// lamport TSO -> lamport 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 enter0; int enter1; int cs0; int cs1; void thread0() { // var declarations // round ROUND; int sim, roundTSO, roundSC; // mask MASK[2]; // masks for each round int MASK0flag0, MASK0flag1, MASK0enter0, MASK0enter1; int MASK1flag0, MASK1flag1, MASK1enter0, MASK1enter1; // shared VIEW, QUEUE[2]; // view of the thread int VIEWflag0, VIEWflag1, VIEWenter0, VIEWenter1; int QUEUE0flag0, QUEUE0flag1, QUEUE0enter0, QUEUE0enter1; int QUEUE1flag0, QUEUE1flag1, QUEUE1enter0, QUEUE1enter1; //BEGIN init_thread corral_atomic_begin(); sim = 1; roundTSO = roundSC =0; // set the view to the shared vars VIEWflag0 = flag0; VIEWflag1 = flag1; VIEWenter0 = enter0; VIEWenter1 = enter1; // initialize MASK0 and MASK1 MASK0flag0 = MASK1flag0 = 0; MASK0flag1 = MASK1flag1 = 0; MASK0enter0 = MASK1enter0 = 0; MASK0enter1 = MASK1enter1 = 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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END while (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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END //enter0 = 1; // BEGIN memory_update_enter0=1 VIEWenter0 = 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) enter0 = 1; else{ // updating mask + queue if (roundTSO==0) {MASK0enter0 = 1; QUEUE0enter0 = 1;} if (roundTSO==1) {MASK1enter0 = 1; QUEUE1enter0 = 1;} } //END memory_update_enter0=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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END if (VIEWflag0 < VIEWflag1) { // flag0 = flag1+1; //BEGIN memory_update_flag0=flag1+1 VIEWflag0 = 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) flag0 = VIEWflag0; else{ // updating mask + queue if (roundTSO==0) {MASK0flag0 = 1; QUEUE0flag0 = VIEWflag0;} if (roundTSO==1) {MASK1flag0 = 1; QUEUE1flag0 = VIEWflag0;} } //END memory_update_flag0=0 } else { // flag0++; //BEGIN memory_update_flag0=flag0+1 VIEWflag0 = 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 = VIEWflag0; else{ // updating mask + queue if (roundTSO==0) {MASK0flag0 = 1; QUEUE0flag0 = VIEWflag0;} if (roundTSO==1) {MASK1flag0 = 1; QUEUE1flag0 = VIEWflag0;} } //END memory_update_flag0=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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END // enter0 = 0; // BEGIN memory_update_enter0=0 VIEWenter0 = 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) enter0 = 0; else{ // updating mask + queue if (roundTSO==0) {MASK0enter0 = 1; QUEUE0enter0 = 0;} if (roundTSO==1) {MASK1enter0 = 1; QUEUE1enter0 = 0;} } //END memory_update_enter0=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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END __hv_assume(!VIEWenter1); //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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END __hv_assume(!( (VIEWflag1 != 0) && (VIEWflag1 < VIEWflag0) )); //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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // 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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // 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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // 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, MASK0enter0, MASK0enter1; int MASK1flag0, MASK1flag1, MASK1enter0, MASK1enter1; // shared VIEW, QUEUE[2]; // view of the thread int VIEWflag0, VIEWflag1, VIEWenter0, VIEWenter1; int QUEUE0flag0, QUEUE0flag1, QUEUE0enter0, QUEUE0enter1; int QUEUE1flag0, QUEUE1flag1, QUEUE1enter0, QUEUE1enter1; //BEGIN init_thread corral_atomic_begin(); sim = 1; roundTSO = roundSC =0; // set the view to the shared vars VIEWflag0 = flag0; VIEWflag1 = flag1; VIEWenter0 = enter0; VIEWenter1 = enter1; // initialize MASK0 and MASK1 MASK0flag0 = MASK1flag0 = 0; MASK0flag1 = MASK1flag1 = 0; MASK0enter0 = MASK1enter0 = 0; MASK0enter1 = MASK1enter1 = 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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END while (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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END // enter1 = 1; // BEGIN memory_update_enter1=1 VIEWenter1 = 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) enter1 = 1; else{ // updating mask + queue if (roundTSO==0) {MASK0enter1 = 1; QUEUE0enter1 = 1;} if (roundTSO==1) {MASK1enter1 = 1; QUEUE1enter1 = 1;} } //END memory_update_enter1=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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END if (VIEWflag0 < VIEWflag1) { // flag1++; //BEGIN memory_update_flag1=flag1+1 VIEWflag1 = 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 = VIEWflag1; else{ // updating mask + queue if (roundTSO==0) {MASK0flag1 = 1; QUEUE0flag1 = VIEWflag1;} if (roundTSO==1) {MASK1flag1 = 1; QUEUE1flag1 = VIEWflag1;} } //END memory_update_flag1=flag1+1 } else { // flag1 = flag0+1; //BEGIN memory_update_flag1=flag0+1 VIEWflag1 = 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) flag1 = VIEWflag1; else{ // updating mask + queue if (roundTSO==0) {MASK0flag1 = 1; QUEUE0flag1 = VIEWflag1;} if (roundTSO==1) {MASK1flag1 = 1; QUEUE1flag1 = VIEWflag1;} } //END memory_update_flag1=flag0+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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END // enter1 = 0; // BEGIN memory_update_enter1=0 VIEWenter1 = 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) enter1 = 0; else{ // updating mask + queue if (roundTSO==0) {MASK0enter1 = 1; QUEUE0enter1 = 0;} if (roundTSO==1) {MASK1enter1 = 1; QUEUE1enter1 = 0;} } //END memory_update_enter1=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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END __hv_assume(!VIEWenter0); //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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // IS_INIT_ROUND END __hv_assume(!( (VIEWflag0 != 0) && ( VIEWflag0 <= VIEWflag1 ))); //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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // 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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // 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; if (roundSC==0) MASK0enter0 = 0; if (roundSC==1) MASK1enter0 = 0; if (roundSC==0) MASK0enter1 = 0; if (roundSC==1) MASK1enter1 = 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==0) && (MASK0enter0 )) enter0 = QUEUE0enter0; if ((roundSC==0) && (MASK0enter1 )) enter1 = QUEUE0enter1; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1enter0 )) enter0 = QUEUE1enter0; if ((roundSC==1) && (MASK1enter1 )) enter1 = QUEUE1enter1; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0enter0 ) && (!MASK1enter0 ) ) VIEWenter0 = enter0; if ( (!MASK0enter1 ) && (!MASK1enter1 ) ) VIEWenter1 = enter1; } // 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 //} __hv_assume(0); } void poirot_main() { // InitializeSpinLock(lock); int t0, t1; flag0 = flag1 = cs0 = cs1 = enter0 = enter0 = 0; __async_call thread0(); __async_call thread1(); corral_atomic_begin(); t0 = cs0; t1 = cs1; corral_atomic_end(); POIROT_ASSERT( !(t0 && t1) ); } void main() {}