diff options
Diffstat (limited to 'src/aig/gia/giaAbsPth.c')
-rw-r--r-- | src/aig/gia/giaAbsPth.c | 119 |
1 files changed, 68 insertions, 51 deletions
diff --git a/src/aig/gia/giaAbsPth.c b/src/aig/gia/giaAbsPth.c index 12abf1d4..e0069132 100644 --- a/src/aig/gia/giaAbsPth.c +++ b/src/aig/gia/giaAbsPth.c @@ -22,7 +22,7 @@ #include "proof/pdr/pdr.h" // comment this out to disable pthreads -//#define ABC_USE_PTHREADS +#define ABC_USE_PTHREADS #ifdef ABC_USE_PTHREADS @@ -41,43 +41,31 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Start and stop proving abstracted model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ #ifndef ABC_USE_PTHREADS void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) {} void Gia_Ga2ProveCancel( int fVerbose ) {} -void Gia_Ga2ProveFinish( int fVerbose ) {} int Gia_Ga2ProveCheck( int fVerbose ) { return 0; } #else // pthreads are used // information given to the thread -typedef struct Abs_Pair_t_ +typedef struct Abs_ThData_t_ { char * pFileName; int fVerbose; int RunId; -} Abs_Pair_t; +} Abs_ThData_t; -// the last valid thread -static int g_nRunIds = 0; -int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } +// mutext to control access to shared variables +pthread_mutex_t g_mutex = PTHREAD_MUTEX_INITIALIZER; +static volatile int g_nRunIds = 0; // the number of the last prover instance +static volatile int g_fAbstractionProved = 0; // set to 1 when prover successed to prove +// call back procedure for PDR +int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } +// test procedure to replace PDR int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) { char * p = ABC_ALLOC( char, 111 ); @@ -90,16 +78,30 @@ int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) return -1; } -static int g_fAbstractionProved = 0; +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create one thread] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void * Abs_ProverThread( void * pArg ) { - Abs_Pair_t * pPair = (Abs_Pair_t *)pArg; + Abs_ThData_t * pThData = (Abs_ThData_t *)pArg; Pdr_Par_t Pars, * pPars = &Pars; Aig_Man_t * pAig, * pTemp; - int RetValue; - pAig = Ioa_ReadAiger( pPair->pFileName, 0 ); + int RetValue, status; + pAig = Ioa_ReadAiger( pThData->pFileName, 0 ); if ( pAig == NULL ) - Abc_Print( 1, "\nCannot open file \"%s\".\n", pPair->pFileName ); + Abc_Print( 1, "\nCannot open file \"%s\".\n", pThData->pFileName ); else { // synthesize abstraction @@ -108,28 +110,33 @@ void * Abs_ProverThread( void * pArg ) // call PDR Pdr_ManSetDefaultParams( pPars ); pPars->fSilent = 1; - pPars->RunId = pPair->RunId; + pPars->RunId = pThData->RunId; pPars->pFuncStop = Abs_CallBackToStop; RetValue = Pdr_ManSolve( pAig, pPars, NULL ); // RetValue = Pdr_ManSolve_test( pAig, pPars, NULL ); // update the result - g_fAbstractionProved = (RetValue == 1); + if ( RetValue == 1 ) + { + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + g_fAbstractionProved = 1; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + } // free memory Aig_ManStop( pAig ); // quit this thread - if ( pPair->fVerbose ) + if ( pThData->fVerbose ) { if ( RetValue == 1 ) - Abc_Print( 1, "\nProved abstraction %d.\n", pPair->RunId ); + Abc_Print( 1, "\nProved abstraction %d.\n", pThData->RunId ); else if ( RetValue == 0 ) - Abc_Print( 1, "\nDisproved abstraction %d.\n", pPair->RunId ); + Abc_Print( 1, "\nDisproved abstraction %d.\n", pThData->RunId ); else if ( RetValue == -1 ) - Abc_Print( 1, "\nCancelled abstraction %d.\n", pPair->RunId ); + Abc_Print( 1, "\nCancelled abstraction %d.\n", pThData->RunId ); else assert( 0 ); } } - ABC_FREE( pPair->pFileName ); - ABC_FREE( pPair ); + ABC_FREE( pThData->pFileName ); + ABC_FREE( pThData ); // quit this thread pthread_exit( NULL ); assert(0); @@ -137,38 +144,48 @@ void * Abs_ProverThread( void * pArg ) } void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) { - Abs_Pair_t * pPair; + Abs_ThData_t * pThData; pthread_t ProverThread; - int RetValue; + int status; assert( pFileName != NULL ); - g_fAbstractionProved = 0; // disable verbosity fVerbose = 0; + // reset the proof + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + g_fAbstractionProved = 0; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + // collect thread data + pThData = ABC_CALLOC( Abs_ThData_t, 1 ); + pThData->pFileName = Abc_UtilStrsav( (void *)pFileName ); + pThData->fVerbose = fVerbose; + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + pThData->RunId = ++g_nRunIds; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); // create thread - pPair = ABC_CALLOC( Abs_Pair_t, 1 ); - pPair->pFileName = Abc_UtilStrsav( (void *)pFileName ); - pPair->fVerbose = fVerbose; - pPair->RunId = ++g_nRunIds; - if ( fVerbose ) Abc_Print( 1, "\nTrying to prove abstraction %d.\n", pPair->RunId ); - RetValue = pthread_create( &ProverThread, NULL, Abs_ProverThread, pPair ); - assert( RetValue == 0 ); + if ( fVerbose ) Abc_Print( 1, "\nTrying to prove abstraction %d.\n", pThData->RunId ); + status = pthread_create( &ProverThread, NULL, Abs_ProverThread, pThData ); + assert( status == 0 ); } void Gia_Ga2ProveCancel( int fVerbose ) { + int status; + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); g_nRunIds++; -} -void Gia_Ga2ProveFinish( int fVerbose ) -{ - g_fAbstractionProved = 0; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); } int Gia_Ga2ProveCheck( int fVerbose ) { - return g_fAbstractionProved; + int status; + if ( g_fAbstractionProved == 0 ) + return 0; + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + g_fAbstractionProved = 0; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + return 1; } #endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |