Suggested changes to improve thread safety.

berkeley-abc · Aug 1, 2024 · 3491773 · 3491773
1 parent a06dde4
commit 3491773
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 20 deletions.
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
@@ -1169,8 +1169,8 @@ void Aig_ManRandomTest1()
 ***********************************************************************/
 unsigned Aig_ManRandom( int fReset )
 {
-    static unsigned int m_z = NUMBER1;
-    static unsigned int m_w = NUMBER2;
+    static __thread unsigned int m_z = NUMBER1;
+    static __thread unsigned int m_w = NUMBER2;
     if ( fReset )
     {
         m_z = NUMBER1;

diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
@@ -48,8 +48,8 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 unsigned Gia_ManRandom( int fReset )
 {
-    static unsigned int m_z = NUMBER1;
-    static unsigned int m_w = NUMBER2;
+    static __thread unsigned int m_z = NUMBER1;
+    static __thread unsigned int m_w = NUMBER2;
     if ( fReset )
     {
         m_z = NUMBER1;

diff --git a/src/misc/util/utilSort.c b/src/misc/util/utilSort.c
@@ -1003,8 +1003,8 @@ void Abc_QuickSortTest()
 
 unsigned Abc_Random( int fReset )
 {
-    static unsigned int m_z = NUMBER1;
-    static unsigned int m_w = NUMBER2;
+    static __thread unsigned int m_z = NUMBER1;
+    static __thread unsigned int m_w = NUMBER2;
     if ( fReset )
     {
         m_z = NUMBER1;

diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
@@ -31,6 +31,7 @@
 #include <pthread.h>
 #include <unistd.h>
 #endif
+#include <stdatomic.h>
 
 #endif
 
@@ -98,25 +99,28 @@ typedef struct Par_ScorrThData_t_
     int *        pMap;
     int          iThread;
     int          nTimeOut;
-    int          fWorking;
+    atomic_bool  fWorking;
 } Par_ScorrThData_t;
 
 void * Ssw_GiaWorkerThread( void * pArg )
 {
+    struct timespec pause_duration;
+    pause_duration.tv_sec = 0;
+    pause_duration.tv_nsec = 10000000L; // 10 milliseconds
+
     Par_ScorrThData_t * pThData = (Par_ScorrThData_t *)pArg;
-    volatile int * pPlace = &pThData->fWorking;
     while ( 1 )
     {
-        while ( *pPlace == 0 );
-        assert( pThData->fWorking );
+        while ( !atomic_load_explicit(&pThData->fWorking, memory_order_acquire) )
+            nanosleep(&pause_duration, NULL);
         if ( pThData->p == NULL )
         {
             pthread_exit( NULL );
             assert( 0 );
             return NULL;
         }
         Cec_ManLSCorrespondenceClasses( pThData->p, &pThData->CorPars );
-        pThData->fWorking = 0;
+        atomic_store_explicit(&pThData->fWorking, 0, memory_order_release);
     }
     assert( 0 );
     return NULL;
@@ -144,37 +148,46 @@ void Ssw_SignalCorrespondenceArray( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
     {
         ThData[i].CorPars  = *pCorPars;
         ThData[i].iThread  = i;
-        //ThData[i].nTimeOut = pPars->nTimeOut;
-        ThData[i].fWorking = 0;
+        atomic_store_explicit(&ThData[i].fWorking, 0, memory_order_release);
         status = pthread_create( WorkerThread + i, NULL, Ssw_GiaWorkerThread, (void *)(ThData + i) );  assert( status == 0 );
     }
+
+    struct timespec pause_duration;
+    pause_duration.tv_sec = 0;
+    pause_duration.tv_nsec = 10000000L; // 10 milliseconds
+
     // look at the threads
     vStack = Vec_PtrDup( vGias );
     while ( Vec_PtrSize(vStack) > 0 )
     {
         for ( i = 0; i < nProcs; i++ )
         {
-            if ( ThData[i].fWorking )
+            if ( atomic_load_explicit(&ThData[i].fWorking, memory_order_acquire) )
                 continue;
             ThData[i].p = (Gia_Man_t*)Vec_PtrPop( vStack );
-            ThData[i].fWorking = 1;   
+            atomic_store_explicit(&ThData[i].fWorking, 1, memory_order_release);
             break;
         }
     }
     Vec_PtrFree( vStack );    
     // wait till threads finish
     for ( i = 0; i < nProcs; i++ )
-        if ( ThData[i].fWorking )
-            i = -1;
+    {
+        if ( atomic_load_explicit(&ThData[i].fWorking, memory_order_acquire) )
+            i = -1; // Start from the beginning again
+        nanosleep(&pause_duration, NULL);
+    }
+
     // stop threads
     for ( i = 0; i < nProcs; i++ )
     {
-        assert( !ThData[i].fWorking );
-        // stop
         ThData[i].p = NULL;
-        ThData[i].fWorking = 1;
+        atomic_store_explicit(&ThData[i].fWorking, 1, memory_order_release);
     }
 
+    // Join threads
+    for ( i = 0; i < nProcs; i++ )
+        pthread_join( WorkerThread[i], NULL );
 }
 
 #endif // pthreads are used