// // array lock // // T.E. Anderson, "The Performance of Spin Lock Alternatives for Shared-Money Multiprocessors" // IEEE Transactions on Parallel and Distributed Systems, Jan-90 // // jones@tcd.ie // // 21/10/14 first version // #define N 3 byte slot[N]; byte nextSlot; byte ncs; byte cs[N]; active[N] proctype p() { byte mySlot; // again: atomic { mySlot = nextSlot; // NB: mySlot = nextSlot++ nextSlot = nextSlot + 1; // NB: NOT valid in Promela } mySlot = mySlot % N; // if :: mySlot == N - 1 -> // nextSlot = nextSlot - N; // NB: must be implemented by an atomic instruction :: else -> skip; fi; slot[mySlot]; // wait until slot[mySlot] ncs++; // critical section assert(ncs == 1); // critical section cs[_pid] = 1; // critical section cs[_pid] = 0; // critical section ncs--; // critical section slot[mySlot] = 0; // initialise for next time slot[(mySlot + 1) % N] = 1; // pass lock to next thread goto again; } init { slot[0] = 1; // must initialise } ltl claim { always eventually cs[0] } // cs0 is true infinitely often // eof