ref: 4a120a381652668b7eb9313d9b8ca1835ddccb91
dir: /sys/src/9/port/semaphore.p/
/* spin -a semaphore.p pcc -DSAFETY -DREACH -DMEMLIM'='500 -o pan pan.c pan -i rm pan.* pan */ #define N 3 bit listlock; byte value; bit onlist[N]; bit waiting[N]; bit sleeping[N]; bit acquired[N]; inline lock(x) { atomic { x == 0; x = 1 } } inline unlock(x) { assert x==1; x = 0 } inline sleep(cond) { assert !sleeping[_pid]; assert !interrupted; if :: cond :: atomic { else -> sleeping[_pid] = 1 } -> !sleeping[_pid] fi; if :: skip :: interrupted = 1 fi } inline wakeup(id) { if :: sleeping[id] == 1 -> sleeping[id] = 0 :: else fi } inline semqueue() { lock(listlock); assert !onlist[_pid]; onlist[_pid] = 1; unlock(listlock) } inline semdequeue() { lock(listlock); assert onlist[_pid]; onlist[_pid] = 0; waiting[_pid] = 0; unlock(listlock) } inline semwakeup(n) { byte i, j; lock(listlock); i = 0; j = n; do :: (i < N && j > 0) -> if :: onlist[i] && waiting[i] -> atomic { printf("kicked %d\n", i); waiting[i] = 0 }; wakeup(i); j-- :: else fi; i++ :: else -> break od; /* reset i and j to reduce state space */ i = 0; j = 0; unlock(listlock) } inline semrelease(n) { atomic { value = value+n; printf("release %d\n", n); }; semwakeup(n) } inline canacquire() { atomic { value > 0 -> value--; }; acquired[_pid] = 1 } #define semawoke() !waiting[_pid] inline semacquire(block) { if :: atomic { canacquire() -> printf("easy acquire\n"); } -> goto out :: else fi; if :: !block -> goto out :: else fi; semqueue(); do :: skip -> waiting[_pid] = 1; if :: atomic { canacquire() -> printf("hard acquire\n"); } -> break :: else fi; sleep(semawoke()) if :: interrupted -> printf("%d interrupted\n", _pid); break :: !interrupted fi od; semdequeue(); if :: !waiting[_pid] -> semwakeup(1) :: else fi; out: assert (!block || interrupted || acquired[_pid]); assert !(interrupted && acquired[_pid]); assert !waiting[_pid]; printf("%d done\n", _pid); } active[N] proctype acquire() { bit interrupted; semacquire(1); printf("%d finished\n", _pid); skip } active proctype release() { byte k; k = 0; do :: k < N -> semrelease(1); k++; :: else -> break od; skip } /* * If this guy, the highest-numbered proc, sticks * around, then everyone else sticks around. * This makes sure that we get a state line for * everyone in a proc dump. */ active proctype dummy() { end: 0; }