// dekker TSO -> dekker 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; if (roundSC==0) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // flag[0] := true //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 //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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END //fence __hv_assume(roundTSO == roundSC); // while flag[1] = true { while (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; if (roundSC==0) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // if turn != 0 { if (VIEWturn != 0) { //BEGIN END_ROUND if ( poirot_nondet()) {sim = FALSE; corral_atomic_end();} //is_end_round //BEGIN 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // flag[0] := false //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 // 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // while turn != 0 { __hv_assume(VIEWturn == 0); // GENNARO /* while (VIEWturn != 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END } */ //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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // flag[0] := true //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 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round } //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round } //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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // turn := 1 // BEGIN memory_update_turn=1 VIEWturn = 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) turn = 1; else{ // updating mask + queue if (roundTSO==0) {MASK0turn = 1; QUEUE0turn = 1;} if (roundTSO==1) {MASK1turn = 1; QUEUE1turn = 1;} } //END memory_update_turn=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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // flag[0] := false //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; if (roundSC==0) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // flag[1] := true //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 //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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END //fence __hv_assume(roundTSO == roundSC); // while flag[0] = true { while (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; if (roundSC==0) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // if turn != 1 { if (VIEWturn != 1) { //BEGIN END_ROUND if ( poirot_nondet()) {sim = FALSE; corral_atomic_end();} //is_end_round //BEGIN 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // flag[1] := false //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 // 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // while turn != 1 { __hv_assume(VIEWturn == 1); // GENNARO /* while (VIEWturn != 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END } */ //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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // flag[1] := true //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 //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round } //BEGIN is_end_round if ( poirot_nondet()) {sim = 0; corral_atomic_end();} //is_end_round //END is_end_round } //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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // 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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // turn := 0 // BEGIN memory_update_turn=0 VIEWturn = 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) turn = 0; else{ // updating mask + queue if (roundTSO==0) {MASK0turn = 1; QUEUE0turn = 0;} if (roundTSO==1) {MASK1turn = 1; QUEUE1turn = 0;} } //END memory_update_turn=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) MASK0turn = 0; if (roundSC==1) MASK1turn = 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) && (MASK0turn )) turn = QUEUE0turn; if ((roundSC==1) && (MASK1flag0)) flag0 = QUEUE1flag0; if ((roundSC==1) && (MASK1flag1)) flag1 = QUEUE1flag1; if ((roundSC==1) && (MASK1turn )) turn = QUEUE1turn; // rebuild the view if ( (!MASK0flag0) && (!MASK1flag0) ) VIEWflag0 = flag0; if ( (!MASK0flag1) && (!MASK1flag1) ) VIEWflag1 = flag1; if ( (!MASK0turn ) && (!MASK1turn ) ) VIEWturn = turn; } // IS_INIT_ROUND END // flag[1] := false //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() {}