// szymanski TSO -> szymanski SC (POIROT) #include "locks.h" #include //#define TRUE 1 //#define FALSE 0 typedef enum boolean {FALSE,TRUE} bool; //KSPIN_LOCK lock; // shared vars int flag0; int flag1; //int turn; int cs0; int cs1; void thread0() { // var declarations // round ROUND; int sim, roundTSO, roundSC; // mask MASK[2]; // masks for each round int MASK0flag0, MASK0flag1 /*, MASK0turn*/; int MASK1flag0, MASK1flag1 /*, MASK1turn*/; // shared VIEW, QUEUE[2]; // view of the thread int VIEWflag0, VIEWflag1 /*, VIEWturn*/; int QUEUE0flag0, QUEUE0flag1 /*, QUEUE0turn*/; int QUEUE1flag0, QUEUE1flag1 /*, QUEUE1turn*/; //BEGIN init_thread corral_atomic_begin(); // AcquireSpinLock(lock); sim = 1; roundTSO = roundSC =0; // set the view to the shared vars VIEWflag0 = flag0; VIEWflag1 = flag1; // VIEWturn = turn; // initialize MASK0 and MASK1 MASK0flag0 = MASK1flag0 = 0; MASK0flag1 = MASK1flag1 = 0; // MASK0turn = MASK1turn = 0; //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round //END init_thread //NEVER CHANGE // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //flag0=1; //BEGIN memory_update_flag0=1 VIEWflag0 = 1; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag0 = 1; else{ // updating mask + queue if (roundTSO==0) {MASK0flag0 = 1; QUEUE0flag0 = 1;} if (roundTSO==1) {MASK1flag0 = 1; QUEUE1flag0 = 1;} } //END memory_update_flag0=1 //fence __hv_assume(roundTSO == roundSC); //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //assume(flag1 < 3); __hv_assume(VIEWflag1 < 3); //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //flag0 = 3; //BEGIN memory_update_flag0=3 VIEWflag0 = 3; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag0 = 3; else{ // updating mask + queue if (roundTSO==0) {MASK0flag0 = 1; QUEUE0flag0 = 3;} if (roundTSO==1) {MASK1flag0 = 1; QUEUE1flag0 = 3;} } //END memory_update_flag0=3 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //if (flag1 == 1){ if (VIEWflag1 == 1){ //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END // flag0=2; //BEGIN memory_update_flag0=2 VIEWflag0 = 2; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag0 = 2; else{ // updating mask + queue if (roundTSO==0) {MASK0flag0 = 1; QUEUE0flag0 = 2;} if (roundTSO==1) {MASK1flag0 = 1; QUEUE1flag0 = 2;} } //END memory_update_flag0=2 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END // assume(flag1 == 4); __hv_assume(VIEWflag1 == 4); } //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //flag0 = 4; //BEGIN memory_update_flag0=4 VIEWflag0 = 4; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag0 = 4; else{ // updating mask + queue if (roundTSO==0) {MASK0flag0 = 1; QUEUE0flag0 = 4;} if (roundTSO==1) {MASK1flag0 = 1; QUEUE1flag0 = 4;} } //END memory_update_flag0=4 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round //CRITICAL SECTION // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END cs0 = 1; //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END cs0 = 0; //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END // assume( (flag1== 0) || (flag1 == 1) || (flag1 == 4) ); __hv_assume( (VIEWflag1 == 0) || (VIEWflag1 == 1) || (VIEWflag1 == 4) ); //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //flag0=0; //BEGIN memory_update_flag0=0 VIEWflag0 = 0; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag0 = 0; else{ // updating mask + queue if (roundTSO==0) {MASK0flag0 = 1; QUEUE0flag0 = 0;} if (roundTSO==1) {MASK1flag0 = 1; QUEUE1flag0 = 0;} } //END memory_update_flag0=0 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round //ASSUME FALSE __hv_assume ( 0 ); } void thread1() { // var declarations // round ROUND; int sim, roundTSO, roundSC; // mask MASK[2]; // masks for each round int MASK0flag0, MASK0flag1 /*, MASK0turn*/; int MASK1flag0, MASK1flag1 /*, MASK1turn*/; // shared VIEW, QUEUE[2]; // view of the thread int VIEWflag0, VIEWflag1 /*, VIEWturn*/; int QUEUE0flag0, QUEUE0flag1 /*, QUEUE0turn*/; int QUEUE1flag0, QUEUE1flag1 /*, QUEUE1turn*/; //BEGIN init_thread corral_atomic_begin(); // AcquireSpinLock(lock); sim = 1; roundTSO = roundSC =0; // set the view to the shared vars VIEWflag0 = flag0; VIEWflag1 = flag1; // VIEWturn = turn; // initialize MASK0 and MASK1 MASK0flag0 = MASK1flag0 = 0; MASK0flag1 = MASK1flag1 = 0; // MASK0turn = MASK1turn = 0; //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round //END init_thread //NEVER CHANGE // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //flag1=1; //BEGIN memory_update_flag1=1 VIEWflag1 = 1; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag1 = 1; else{ // updating mask + queue if (roundTSO==0) {MASK0flag1 = 1; QUEUE0flag1 = 1;} if (roundTSO==1) {MASK1flag1 = 1; QUEUE1flag1 = 1;} } //END memory_update_flag1=1 //fence __hv_assume(roundTSO == roundSC); //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //assume(flag0 < 3); __hv_assume(VIEWflag0 < 3); //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //flag1 = 3; //BEGIN memory_update_flag1=3 VIEWflag1 = 3; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag1 = 3; else{ // updating mask + queue if (roundTSO==0) {MASK0flag1 = 1; QUEUE0flag1 = 3;} if (roundTSO==1) {MASK1flag1 = 1; QUEUE1flag1 = 3;} } //END memory_update_flag1=3 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //if (flag0 == 1){ if (VIEWflag0 == 1){ //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END // flag1=2; //BEGIN memory_update_flag1=2 VIEWflag1 = 2; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag1 = 2; else{ // updating mask + queue if (roundTSO==0) {MASK0flag1 = 1; QUEUE0flag1 = 2;} if (roundTSO==1) {MASK1flag1 = 1; QUEUE1flag1 = 2;} } //END memory_update_flag1=2 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END // assume(flag0 == 4); __hv_assume(VIEWflag0 == 4); } //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //flag1 = 4; //BEGIN memory_update_flag1=4 VIEWflag1 = 4; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag1 = 4; else{ // updating mask + queue if (roundTSO==0) {MASK0flag1 = 1; QUEUE0flag1 = 4;} if (roundTSO==1) {MASK1flag1 = 1; QUEUE1flag1 = 4;} } //END memory_update_flag1=4 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END // assume( flag0 < 2 ); __hv_assume( VIEWflag0 <2 ); //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round //CRITICAL SECTION // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END cs1 = 1; //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END cs1 = 0; //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round // IS_INIT_ROUND BEGIN if ( !sim ) { corral_atomic_begin(); //AcquireSpinLock(lock); sim = 1; // increment roundTSO if needed if ( roundTSO == roundSC ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } // reset the mask for the current round (roundSC) if (roundSC==0) MASK0flag0 = 0; if (roundSC==1) MASK1flag0 = 0; if (roundSC==0) MASK0flag1 = 0; if (roundSC==1) MASK1flag1 = 0; // increment roundSC if (roundSC == 1) roundSC=0; else roundSC++; // updating the shared memory if ((roundSC==0) && (MASK0flag0)) flag0 = QUEUE0flag0; if ((roundSC==0) && (MASK0flag1)) flag1 = QUEUE0flag1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; } // IS_INIT_ROUND END //flag1=0; //BEGIN memory_update_flag1=0 VIEWflag1 = 0; while ( poirot_nondet() ){ //non-deterministically increase roundTSO if (!( ( (roundTSO == 1) && (roundSC == 0) ) || ( (roundTSO+1) == roundSC ) ) ) {if (roundTSO == 1) roundTSO=0; else roundTSO++; } } if (roundSC == roundTSO) flag1 = 0; else{ // updating mask + queue if (roundTSO==0) {MASK0flag1 = 1; QUEUE0flag1 = 0;} if (roundTSO==1) {MASK1flag1 = 1; QUEUE1flag1 = 0;} } //END memory_update_flag1=0 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round //ASSUME FALSE __hv_assume ( 0 ); } void poirot_main() { // InitializeSpinLock(lock); int t0, t1; flag0 = flag1 = cs0 = cs1 = /*turn =*/ 0; __async_call thread0(); __async_call thread1(); corral_atomic_begin(); t0 = cs0; t1 = cs1; corral_atomic_end(); POIROT_ASSERT( !(t0 && t1) ); } void main() {}