// ------------------------------------------------------------------- // Dekker's mutual exclusion algorithm // ------------------------------------------------------------------- // The idea is that the competing threads write their id to a variable // "last" when they leave the critical section. This determines a dynamic // priority that breaks the symmetry. It is also possible to extend // the algorithm to an arbitrary number of processes. // ------------------------------------------------------------------- module Dekker(event ?start1,?start2,crit1,crit2) { bool req1,req2; nat{4} last; last = 1; // to break the symmetry, the threads write their // index to this variable when leaving the crit. sec. { loop { await(start1); next(req1) = true; pause; while(req2) { if(last==2) { next(req1) = false; await(last==1); next(req1) = true; } } // critical section starts here emit(crit1); pause; // critical section ends here next(last) = 2; next(req1) = false; } || loop { await(start2); next(req2) = true; pause; while(req1) { if(last==1) { next(req2) = false; await(last==2); next(req2) = true; } } // critical section starts here emit(crit2); pause; // critical section ends here next(last) = 1; next(req2) = false; } } }satisfies { Mutex : assert A G !(crit1 & crit2); Fair : assert A ((G F start1 -> G F crit1) & (G F start2 -> G F crit2) ); }