1. Replace system() with a function that responds to SIGINT. 2. Add functions to cleanup temporary files on SIGINT. 3. Fix bugs related to signal handling.

9 files changed, 1016 insertions, 48 deletions

diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 47b031bc..15cbdda5 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -27,6 +27,7 @@
 #include "abc.h"
 #include "mainInt.h"
 #include "cmdInt.h"
+#include "utilSignal.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1557,7 +1558,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     strcat( Command, "\"" );
 
     // call SIS
-    if ( system( Command ) )
+    if ( Util_SignalSystem( Command ) )
     {
         fprintf( pErr, "The following command has returned non-zero exit status:\n" );
         fprintf( pErr, "\"%s\"\n", Command );
@@ -1700,7 +1701,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     strcat( Command, "\"" );
 
     // call MVSIS
-    if ( system( Command ) )
+    if ( Util_SignalSystem( Command ) )
     {
         fprintf( pErr, "The following command has returned non-zero exit status:\n" );
         fprintf( pErr, "\"%s\"\n", Command );
@@ -1912,7 +1913,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // call Capo
-    if ( system( Command ) )
+    if ( Util_SignalSystem( Command ) )
     {
         fprintf( pErr, "The following command has returned non-zero exit status:\n" );
         fprintf( pErr, "\"%s\"\n", Command );
@@ -1964,7 +1965,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
 #else
     {
         sprintf( Command, "%s %s ", pProgNameGnuplot, pPlotFileName );
-        if ( system( Command ) == -1 )
+        if ( Util_SignalSystem( Command ) == -1 )
         {
             fprintf( stdout, "Cannot execute \"%s\".\n", Command );
             goto usage;
diff --git a/src/base/cmd/cmdLoad.c b/src/base/cmd/cmdLoad.c
index 7a83385c..8ff03282 100644
--- a/src/base/cmd/cmdLoad.c
+++ b/src/base/cmd/cmdLoad.c
@@ -22,6 +22,7 @@
 #include "mainInt.h"
 #include "cmd.h"
 #include "cmdInt.h"
+#include "utilSignal.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -72,7 +73,7 @@ int CmdCommandLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     Vec_StrPush( vCommand, 0 );
     // run the command line
-    if ( system( Vec_StrArray(vCommand) ) )
+    if ( Util_SignalSystem( Vec_StrArray(vCommand) ) )
     {
         Abc_Print( -1, "The following command has returned non-zero exit status:\n" );
         Abc_Print( -1, "\"%s\"\n", Vec_StrArray(vCommand) );
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index 7375eb42..116687c7 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -29,6 +29,7 @@
 #include "mainInt.h"
 #include "cmd.h"
 #include "cmdInt.h"
+#include "utilSignal.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -111,8 +112,6 @@ command, then we add a new object for the new action.
 
 */
 
-extern int tmpFile(const char* prefix, const char* suffix, char** out_name);
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -366,7 +365,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // create temp file
-    fd = tmpFile( "__abctmp_", ".aig", &pFileIn );
+    fd = Util_SignalTmpFile( "__abctmp_", ".aig", &pFileIn );
     if ( fd == -1 )
     {
         Abc_Print( -1, "Cannot create a temporary file.\n" );
@@ -379,7 +378,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
 #endif
 
     // create temp file
-    fd = tmpFile( "__abctmp_", ".out", &pFileOut );
+    fd = Util_SignalTmpFile( "__abctmp_", ".out", &pFileOut );
     if ( fd == -1 )
     {
         ABC_FREE( pFileIn );
@@ -437,7 +436,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
 //printf( "Running command line: %s\n", Vec_StrArray(vCommand) ); 
 
     clk = clock();
-    if ( system( Vec_StrArray(vCommand) ) )
+    if ( Util_SignalSystem( Vec_StrArray(vCommand) ) )
     {
         Abc_Print( -1, "The following command has returned non-zero exit status:\n" );
         Abc_Print( -1, "\"%s\"\n", Vec_StrArray(vCommand) );
@@ -516,11 +515,9 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
     
 
     // clean up
-    if ( !fLeaveFiles )
-    {
-        remove( pFileIn );
-        remove( pFileOut );
-    }
+    Util_SignalTmpFileRemove( pFileIn, fLeaveFiles );
+    Util_SignalTmpFileRemove( pFileOut, fLeaveFiles );
+    
     ABC_FREE( pFileIn );
     ABC_FREE( pFileOut );
     return 0;
@@ -565,7 +562,7 @@ int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // create temp file
-    fd = tmpFile( "__abctmp_", ".txt", &pTempFile );
+    fd = Util_SignalTmpFile( "__abctmp_", ".txt", &pTempFile );
     if ( fd == -1 )
     {
         Abc_Print( -1, "Cannot create a temporary file.\n" );
@@ -581,7 +578,7 @@ int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
     pCommandLine = ABC_ALLOC( char, 100 + strlen(pStrDirBin) + strlen(pTempFile) );
 //    sprintf( pCommandLine, "%s -abc -list-commands > %s", pStrDirBin, pTempFile );
     sprintf( pCommandLine, "%s -abc -list-commands > %s", pStrDirBin, pTempFile );
-    RetValue = system( pCommandLine );
+    RetValue = Util_SignalSystem( pCommandLine );
     if ( RetValue == -1 )
     {
         Abc_Print( -1, "Command \"%s\" did not succeed.\n", pCommandLine );
@@ -610,7 +607,7 @@ int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Creating command %s with binary %s\n", pBuffer, pStrDirBin );
     }
     fclose( pFile );
-    remove( pTempFile );
+    Util_SignalTmpFileRemove( pTempFile, 0 );
     ABC_FREE( pTempFile );
     return 0;
 usage:
diff --git a/src/misc/hash/hashGen.h b/src/misc/hash/hashGen.h
new file mode 100644
index 00000000..33359e89
--- /dev/null
+++ b/src/misc/hash/hashGen.h
@@ -0,0 +1,365 @@
+/**CFile****************************************************************
+
+  FileName    [vecGen.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hash maps.]
+
+  Synopsis    [Hash maps.]
+
+  Author      [Aaron P. Hurst, Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Jan 26, 2011.]
+
+  Revision    [$Id: vecGen.h,v 1.00 2005/06/20 00:00:00 ahurst Exp $]
+
+***********************************************************************/
+ 
+#ifndef __HASH_GEN_H__
+#define __HASH_GEN_H__
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Hash_Gen_t_       Hash_Gen_t;
+typedef struct Hash_Gen_Entry_t_ Hash_Gen_Entry_t;
+
+struct Hash_Gen_Entry_t_
+{
+  char *                          key;
+  void *                          data;
+  struct Hash_Gen_Entry_t_ *     pNext;
+};
+
+struct Hash_Gen_t_ 
+{
+  int                             nSize;
+  int                             nBins;
+  int (* fHash)(void *key, int nBins);
+  int (* fComp)(void *key, void *data);
+  int                             fFreeKey;
+  Hash_Gen_Entry_t **            pArray;
+};
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define Hash_GenForEachEntry( pHash, pEntry, bin )   \
+  for(bin=-1, pEntry=NULL; bin < pHash->nBins; (!pEntry)?(pEntry=pHash->pArray[++bin]):(pEntry=pEntry->pNext)) \
+    if (pEntry)
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Default hash function for strings.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Hash_DefaultHashFuncStr( void * key, int nBins )
+{
+    char* p = (const char*)key;
+    int h=0;
+
+    for( ; *p ; ++p )
+        h += h*5 + *p;
+  
+    return (unsigned)h % nBins; 
+}
+
+static int Hash_DefaultCmpFuncStr( void * key1, void * key2 )
+{
+    return strcmp((const char*)key1, (const char*) key2);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Default hash function for (long) integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Hash_DefaultHashFuncInt( void * key, int nBins )
+{
+    return (long)key % nBins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Default comparison function for (long) integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Hash_DefaultCmpFuncInt( void * key1, void* key2 )
+{
+    return (long)key1 - (long)key2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a hash map with the given number of bins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hash_Gen_t * Hash_GenAlloc( 
+  int nBins, 
+  int (*Hash_FuncHash)(void *, int),
+  int (*Hash_FuncComp)(void *, void *),
+  int fFreeKey)
+{
+  Hash_Gen_t * p;
+  int i;
+  assert(nBins > 0);
+  p = ABC_CALLOC( Hash_Gen_t, 1 );
+  p->nBins  = nBins;
+  p->fHash  = Hash_FuncHash? Hash_FuncHash : (int (*)(void *, int))Hash_DefaultHashFuncStr;
+  p->fComp  = Hash_FuncComp? Hash_FuncComp : (int (*)(void *, void *))Hash_DefaultCmpFuncStr;
+  p->fFreeKey = fFreeKey;
+  p->nSize  = 0;
+  p->pArray = ABC_CALLOC( Hash_Gen_Entry_t *, nBins );
+  return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if a key already exists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Hash_GenExists( Hash_Gen_t *p, void * key )
+{
+  int bin;
+  Hash_Gen_Entry_t *pEntry;
+
+  // find the bin where this key would live
+  bin = (*(p->fHash))(key, p->nBins);
+
+  // search for key
+  pEntry = p->pArray[bin];
+  while(pEntry) {
+    if ( !p->fComp(pEntry->key,key) ) {
+      return 1;
+    }
+    pEntry = pEntry->pNext;
+  }
+
+  return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates an entry with a key and writes value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Hash_GenWriteEntry( Hash_Gen_t *p, void * key, void * data )
+{
+  int bin;
+  Hash_Gen_Entry_t *pEntry, **pLast;
+
+  // find the bin where this key would live
+  bin = (*(p->fHash))(key, p->nBins);
+
+  // search for key
+  pLast = &(p->pArray[bin]);
+  pEntry = p->pArray[bin];
+  while(pEntry) {
+    if ( !p->fComp(pEntry->key,key) ) {
+      pEntry->data = data;
+      return;
+    }
+    pLast = &(pEntry->pNext);
+    pEntry = pEntry->pNext;
+  }
+
+  // this key does not currently exist
+  // create a new entry and add to bin
+  p->nSize++;
+  (*pLast) = pEntry = ABC_ALLOC( Hash_Gen_Entry_t, 1 );
+  pEntry->pNext = NULL;
+  pEntry->key  = key;
+  pEntry->data = data;
+
+  return;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates an entry with a key.]
+
+  Description [fCreate specifies whether a new entry should be created.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hash_Gen_Entry_t * Hash_GenEntry( Hash_Gen_t *p, void * key, int fCreate )
+{
+  int bin;
+  Hash_Gen_Entry_t *pEntry, **pLast;
+
+  // find the bin where this key would live
+  bin = (*(p->fHash))(key, p->nBins);
+
+  // search for key
+  pLast = &(p->pArray[bin]);
+  pEntry = p->pArray[bin];
+  while(pEntry) {
+    if ( !p->fComp(pEntry->key,key) )
+      return pEntry;
+    pLast = &(pEntry->pNext);
+    pEntry = pEntry->pNext;
+  }
+
+  // this key does not currently exist
+  if (fCreate) {
+    // create a new entry and add to bin
+    p->nSize++;
+    (*pLast) = pEntry = ABC_ALLOC( Hash_Gen_Entry_t, 1 );
+    pEntry->pNext = NULL;
+    pEntry->key  = key;
+    pEntry->data = NULL;
+    return pEntry;
+  }
+
+  return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes an entry.]
+
+  Description [Returns data, if there was any.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void* Hash_GenRemove( Hash_Gen_t *p, void * key )
+{
+  int    bin;
+  void * data;
+  Hash_Gen_Entry_t *pEntry, **pLast;
+
+  // find the bin where this key would live
+  bin = (*(p->fHash))(key, p->nBins);
+
+  // search for key
+  pLast = &(p->pArray[bin]);
+  pEntry = p->pArray[bin];
+  while(pEntry) {
+    if ( !p->fComp(pEntry->key,key) ) {
+      p->nSize--;
+      data = pEntry->data;
+      *pLast = pEntry->pNext;
+      if (p->fFreeKey)
+        ABC_FREE(pEntry->key);
+      ABC_FREE(pEntry);
+      return data;
+    }
+    pLast = &(pEntry->pNext);
+    pEntry = pEntry->pNext;
+  }
+    
+  // could not find key
+  return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the hash.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Hash_GenFree( Hash_Gen_t *p ) 
+{
+  int bin;
+  Hash_Gen_Entry_t *pEntry, *pTemp;
+
+  // free bins
+  for(bin = 0; bin < p->nBins; bin++) {
+    pEntry = p->pArray[bin];
+    while(pEntry) {
+      pTemp = pEntry;
+      if( p->fFreeKey )
+        ABC_FREE(pTemp->key);
+      pEntry = pEntry->pNext;
+      ABC_FREE( pTemp );
+    }
+  }
+ 
+  // free hash
+  ABC_FREE( p->pArray );
+  ABC_FREE( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/misc/util/module.make b/src/misc/util/module.make
index 54fb8291..c70d582a 100644
--- a/src/misc/util/module.make
+++ b/src/misc/util/module.make
@@ -1 +1 @@
-SRC += src/misc/util/utilFile.c
+SRC += src/misc/util/utilFile.c src/misc/util/utilSignal.c
diff --git a/src/misc/util/utilSignal.c b/src/misc/util/utilSignal.c
new file mode 100644
index 00000000..698ba6d6
--- /dev/null
+++ b/src/misc/util/utilSignal.c
@@ -0,0 +1,520 @@
+/**CFile****************************************************************
+
+  FileName    [utilSignal.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      []
+  
+  Affiliation [UC Berkeley]
+
+  Date        []
+
+  Revision    []
+
+***********************************************************************/
+
+#ifndef _MSC_VER
+
+#include <main.h>
+#include <stdlib.h>
+#include <unistd.h>
+#include <signal.h>
+#include <hashGen.h>
+#include <errno.h>
+#include <pthread.h>
+
+#include "abc_global.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Hash_Gen_t* watched_pid_hash = NULL;
+static Hash_Gen_t* watched_tmp_files_hash = NULL;
+
+static sigset_t* old_procmask;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Kills all watched child processes and remove all watched termporary files.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void Util_SignalCleanup()
+{
+    int i;
+    Hash_Gen_Entry_t* pEntry;
+    
+    // kill all watched child processes
+    Hash_GenForEachEntry(watched_pid_hash, pEntry, i)
+    {
+        pid_t pid = (pid_t)pEntry->key;
+        pid_t ppid = (pid_t)pEntry->data;
+        
+        if (getpid() == ppid)
+        {
+            kill(pid, SIGINT);
+        }
+    }
+
+    // remove watched temporary files
+    Hash_GenForEachEntry(watched_tmp_files_hash, pEntry, i)
+    {
+        int fname = (const char*)pEntry->key;
+        pid_t ppid = (pid_t)pEntry->data;
+        
+        if( getpid() == ppid )
+        {
+            remove(fname);
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Sets up data structures needed for cleanup in signal handler.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void Util_SignalStartHandler()
+{
+    watched_pid_hash = Hash_GenAlloc(100, Hash_DefaultHashFuncInt, Hash_DefaultCmpFuncInt, 0);
+    watched_tmp_files_hash = Hash_GenAlloc(100, Hash_DefaultHashFuncStr, strcmp, 1);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Frees data structures used for clean up in signal handler.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void Util_SignalResetHandler()
+{
+    int i;
+    Hash_Gen_Entry_t* pEntry;
+    
+    sigset_t procmask, old_procmask;
+    
+    sigemptyset(&procmask);
+    sigaddset(&procmask, SIGINT);
+    
+    sigprocmask(SIG_BLOCK, &procmask, &old_procmask);
+    
+    Hash_GenFree(watched_pid_hash);
+    watched_pid_hash = Hash_GenAlloc(100, Hash_DefaultHashFuncInt, Hash_DefaultCmpFuncInt, 0);
+    
+    Hash_GenFree(watched_tmp_files_hash);
+    watched_tmp_files_hash = Hash_GenAlloc(100, Hash_DefaultHashFuncStr, strcmp, 1);
+    
+    sigprocmask(SIG_SETMASK, &old_procmask, NULL);
+}
+
+void Util_SignalStopHandler()
+{
+    int i;
+    Hash_Gen_Entry_t* pEntry;
+    
+    Hash_GenFree(watched_pid_hash);
+    watched_pid_hash = NULL;
+    
+    Hash_GenFree(watched_tmp_files_hash);
+    watched_tmp_files_hash = NULL;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Blocks SIGINT. For use when updating watched processes and temporary files to prevent race conditions with the signal handler.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+static int nblocks = 0;
+
+void Util_SignalBlockSignals()
+{
+    sigset_t procmask;
+
+    assert(nblocks==0);
+    nblocks ++ ;
+    
+    sigemptyset(&procmask);
+    sigaddset(&procmask, SIGINT);
+    
+    sigprocmask(SIG_BLOCK, &procmask, &old_procmask);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Unblocks SIGINT after a call to Util_SignalBlockSignals.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void Util_SignalUnblockSignals()
+{
+    assert( nblocks==1);
+    nblocks--;
+    
+    sigprocmask(SIG_SETMASK, &old_procmask, NULL);
+}
+
+
+static void watch_tmp_file(const char* fname)
+{
+    if( watched_tmp_files_hash != NULL )
+    {
+        Hash_GenWriteEntry(watched_tmp_files_hash, Extra_UtilStrsav(fname), (void*)getpid() );
+    }
+}
+
+static void unwatch_tmp_file(const char* fname)
+{
+    if ( watched_tmp_files_hash )
+    {
+        assert( Hash_GenExists(watched_tmp_files_hash, fname) );
+        Hash_GenRemove(watched_tmp_files_hash, fname);
+        assert( !Hash_GenExists(watched_tmp_files_hash, fname) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Adds a process id to the list of processes that should be killed in a signal handler.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void Util_SignalAddChildPid(int pid)
+{
+    if ( watched_pid_hash )
+    {
+        Hash_GenWriteEntry(watched_pid_hash, (void*)pid,  (void*)getpid());
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Removes a process id from the list of processes that should be killed in a signal handler.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void Util_SignalRemoveChildPid(int pid)
+{
+    if ( watched_pid_hash )
+    {
+        Hash_GenRemove(watched_pid_hash, (void*)pid);
+    }
+}
+
+// a dummy signal hanlder to make sure that SIGCHLD and SIGINT will cause sigsuspend() to return
+static int null_sig_handler(int signum)
+{
+    return 0;
+}
+
+
+// enusre that sigsuspend() returns when signal signum occurs -- sigsuspend() does not return if a signal is ignored
+static void replace_sighandler(int signum, struct sigaction* old_sa, int replace_dfl)
+{
+    sigaction(signum, NULL, old_sa);
+
+    if( old_sa->sa_handler == SIG_IGN || old_sa->sa_handler==SIG_DFL && replace_dfl)
+    {
+        struct sigaction sa;
+        memset(&sa, 0, sizeof(sa));
+        
+        sa.sa_handler = null_sig_handler;
+        
+        sigaction(signum, &sa, &old_sa);
+    }
+}
+
+// 
+static int do_waitpid(pid_t pid, sigset_t* old_procmask)
+{
+    int status;
+
+    struct sigaction sigint_sa;
+    struct sigaction sigchld_sa;
+    sigset_t waitmask;
+    
+    // ensure SIGINT and SIGCHLD are not blocked during sigsuspend()
+    memcpy(&waitmask, old_procmask, sizeof(sigset_t));
+    
+    sigdelset(&waitmask, SIGINT);
+    sigdelset(&waitmask, SIGCHLD);
+
+    // ensure sigsuspend() returns if SIGINT or SIGCHLD occur, and save the current settings for SIGCHLD and SIGINT
+    
+    replace_sighandler(SIGINT, &sigint_sa, 0);
+    replace_sighandler(SIGCHLD, &sigchld_sa, 1);
+    
+    for(;;)
+    {
+        int rc;
+
+        // wait for a signal -- returns if SIGINT or SIGCHLD (or any other signal that is unblocked and not ignored) occur
+        sigsuspend(&waitmask);
+        
+        // check if pid has terminated
+        rc = waitpid(pid, &status, WNOHANG);
+        
+        // stop if terminated or some other error occurs
+        if( rc > 0 || rc == -1 && errno!=EINTR )
+        {
+            break;
+        }
+    }
+    
+    // process is dead, should no longer be watched
+    Util_SignalRemoveChildPid(pid);
+    
+    // restore original behavior of SIGINT and SIGCHLD
+    sigaction(SIGINT, &sigint_sa, NULL);
+    sigaction(SIGCHLD, &sigchld_sa, NULL);
+    
+    return status;
+}
+
+static int do_system(const char* cmd, sigset_t* old_procmask)
+{
+    int pid;
+
+    pid = fork();
+    
+    if (pid == -1)
+    {
+        // fork failed
+        return -1;
+    }
+    else if( pid == 0)
+    {
+        // child process
+        sigprocmask(SIG_SETMASK, old_procmask, NULL);
+        execl("/bin/sh", "sh", "-c", cmd, NULL);
+        _exit(127);
+    }
+
+    Util_SignalAddChildPid(pid);
+    
+    return do_waitpid(pid, old_procmask);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Replaces system() with a function that allows SIGINT to interrupt.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+int Util_SignalSystem(const char* cmd)
+{
+    int status;
+    
+    sigset_t procmask;
+    sigset_t old_procmask;
+ 
+    // if signal handler is not installed, run the original system()
+    if ( ! watched_pid_hash && ! watched_tmp_files_hash )
+        return system(cmd);
+    
+    // block SIGINT and SIGCHLD
+    sigemptyset(&procmask);
+
+    sigaddset(&procmask, SIGINT);
+    sigaddset(&procmask, SIGCHLD);
+    
+    sigprocmask(SIG_BLOCK, &procmask, &old_procmask);
+
+    // call the actual function    
+    status = do_system(cmd, &old_procmask);
+    
+    // restore signal block mask
+    sigprocmask(SIG_SETMASK, &old_procmask, NULL);
+    return status;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#else /* #ifndef _MSC_VER */
+
+#include "abc_global.h"
+
+ABC_NAMESPACE_IMPL_START
+
+void Util_SignalCleanup()
+{
+}
+
+void Util_SignalStartHandler()
+{
+}
+
+void Util_SignalResetHandler()
+{
+}
+
+void Util_SignalStopHandler()
+{
+}
+
+void Util_SignalBlockSignals()
+{
+}
+
+void Util_SignalUnblockSignals()
+{
+}
+
+void watch_tmp_file(const char* fname)
+{
+}
+
+void unwatch_tmp_file(const char* fname)
+{
+}
+
+void Util_SignalAddChildPid(int pid)
+{
+}
+
+void Util_SignalRemoveChildPid(int pid)
+{
+}
+
+int Util_SignalSystem(const char* cmd)
+{
+    return system(cmd);
+}
+
+#endif  /* #ifdef _MSC_VER */
+
+int tmpFile(const char* prefix, const char* suffix, char** out_name);
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Create a temporary file and add it to the list of files to be cleaned up in the signal handler.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
+{
+    int fd;
+    
+    Util_SignalBlockSignals();
+    
+    fd  = tmpFile(prefix, suffix, out_name);
+    
+    if ( fd != -1 )
+    {
+        watch_tmp_file( *out_name );
+    }
+    
+    Util_SignalUnblockSignals();
+    
+    return fd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Remove a temporary file (and remove it from the watched files list.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void Util_SignalTmpFileRemove(const char* fname, int fLeave)
+{
+    Util_SignalBlockSignals();
+    
+    unwatch_tmp_file(fname);
+    
+    if (! fLeave)
+    {
+        remove(fname);
+    }
+    
+    Util_SignalUnblockSignals();
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/misc/util/utilSignal.h b/src/misc/util/utilSignal.h
new file mode 100644
index 00000000..d9802aa0
--- /dev/null
+++ b/src/misc/util/utilSignal.h
@@ -0,0 +1,71 @@
+/**CFile****************************************************************
+
+  FileName    [utilSignal.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      []
+  
+  Affiliation [UC Berkeley]
+
+  Date        []
+
+  Revision    []
+
+***********************************************************************/
+ 
+#ifndef __UTIL_SIGNAL_H__
+#define __UTIL_SIGNAL_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== utilSignal.c ==========================================================*/
+
+void Util_SignalCleanup();
+
+void Util_SignalStartHandler();
+void Util_SignalResetHandler();
+void Util_SignalStopHandler();
+
+void Util_SignalBlockSignals();
+void Util_SignalUnblockSignals();
+
+void Util_SignalAddChildPid(int pid);
+void Util_SignalRemoveChildPid(int pid);
+
+int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name);
+void Util_SignalTmpFileRemove(const char* fname, int fLeave);
+
+int Util_SignalSystem(const char* cmd);
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/python/pyabc.i b/src/python/pyabc.i
index 56ef5cb0..0bf58288 100644
--- a/src/python/pyabc.i
+++ b/src/python/pyabc.i
@@ -25,8 +25,7 @@
 #include <main.h>
 #include <stdlib.h>
 #include <signal.h>
-#include <hash.h>
-#include <hashPtr.h>
+#include "utilSignal.h"
     
 int n_ands()
 {
@@ -219,56 +218,44 @@ void pyabc_internal_register_command( char * sGroup, char * sName, int fChanges
     Cmd_CommandAdd( pAbc, sGroup, sName, (void*)pyabc_internal_abc_command_callback, fChanges);
 }
 
-static Hash_Ptr_t* active_pid_hash = NULL;
-
-void sigint_handler(int signum)
+static void sigint_handler(int signum)
 {
-    int i;
-    Hash_Ptr_Entry_t* pEntry;
-    
-    assert( signum == SIGINT );
-    
-    Hash_PtrForEachEntry(active_pid_hash, pEntry, i)
-    {
-        int pid = pEntry->key;
-        kill(pid, SIGINT);
-    }
-
+    Util_SignalCleanup();
     _exit(1);
 }
 
 void add_child_pid(int pid)
 {
-    Hash_PtrWriteEntry(active_pid_hash, pid, NULL);
+    Util_SignalAddChildPid(pid);
 }
 
 void remove_child_pid(int pid)
 {
-    Hash_PtrRemove(active_pid_hash, pid);
+    Util_SignalRemoveChildPid(pid);
 }
 
-static sigset_t old_procmask;
-
 void block_sigint()
 {
-    sigset_t set;
-    sigemptyset(&set);
-    sigaddset(&set, SIGINT);
-    
-    sigprocmask(SIG_BLOCK, &set, &old_procmask);
+    Util_SignalBlockSignals();
 }
 
 void restore_sigint_block()
 {
-    sigprocmask(SIG_SETMASK, &old_procmask, NULL);
+    Util_SignalUnblockSignals();
+}
+
+void reset_sigint_handler()
+{
+    Util_SignalResetHandler();
 }
 
+
 %}
 
 %init 
 %{
     Abc_Start();
-    active_pid_hash = Hash_PtrAlloc(1);
+    Util_SignalStartHandler();
     signal(SIGINT, sigint_handler);
 %}
 
@@ -301,6 +288,7 @@ void block_sigint();
 void restore_sigint_block();
 void add_child_pid(int pid);
 void remove_child_pid(int pid);
+void reset_sigint_handler();
 
 %pythoncode 
 %{
diff --git a/src/python/pyabc_split.py b/src/python/pyabc_split.py
index b52288c2..431a87a8 100644
--- a/src/python/pyabc_split.py
+++ b/src/python/pyabc_split.py
@@ -83,6 +83,7 @@ Author: Baruch Sterin <sterin@berkeley.edu>
 """
 
 import os
+import errno
 import sys
 import pickle
 import signal
@@ -90,6 +91,26 @@ from contextlib import contextmanager
 
 import pyabc
 
+def _waitpid(pid, flags):
+    while True:
+        try:
+            res =  os.waitpid(pid, flags)
+            return res
+        except OSError as e:
+            if e.errno != errno.EINTR:
+                raise
+
+def _wait():
+    while True:
+        try:
+            pid,rc = os.wait()
+            return pid, rc
+        except OSError as e:
+            if e.errno != errno.EINTR:
+                raise
+        except Exceptions as e:
+            raise
+
 class _sigint_critical_section(object):
     def __init__(self):
         self.blocked = False
@@ -132,7 +153,7 @@ class _splitter(object):
         with _sigint_critical_section() as cs:
             # wait for termination and update result
             for pid, _ in self.fds.iteritems():
-                os.waitpid( pid, 0 )
+                _waitpid( pid, 0 )
                 pyabc.remove_child_pid(pid)
                 self.results[pid] = None
             
@@ -164,6 +185,7 @@ class _splitter(object):
         
                 if pid == 0:
                     # child process:
+                    pyabc.reset_sigint_handler()
                     cs.release()
                     os.close(pr)
                     rc = self.child( pw, f)
@@ -187,9 +209,12 @@ class _splitter(object):
     def get_next_result(self):
     
         # wait for the next child process to terminate
-        pid, rc = os.wait()
+        pid, rc = _wait()
         assert pid in self.fds
         
+        with _sigint_critical_section() as cs:
+            pyabc.remove_child_pid(pid)
+        
         # retrieve the pipe file descriptor1
         i, fd = self.fds[pid]
         del self.fds[pid]