1/* 2spin -a semaphore.p 3pcc -DSAFETY -DREACH -DMEMLIM'='500 -o pan pan.c 4pan -i 5rm pan.* pan 6 7*/ 8 9#define N 3 10 11bit listlock; 12byte value; 13bit onlist[N]; 14bit waiting[N]; 15bit sleeping[N]; 16bit acquired[N]; 17 18inline lock(x) 19{ 20 atomic { x == 0; x = 1 } 21} 22 23inline unlock(x) 24{ 25 assert x==1; 26 x = 0 27} 28 29inline sleep(cond) 30{ 31 assert !sleeping[_pid]; 32 assert !interrupted; 33 if 34 :: cond 35 :: atomic { else -> sleeping[_pid] = 1 } -> 36 !sleeping[_pid] 37 fi; 38 if 39 :: skip 40 :: interrupted = 1 41 fi 42} 43 44inline wakeup(id) 45{ 46 if 47 :: sleeping[id] == 1 -> sleeping[id] = 0 48 :: else 49 fi 50} 51 52inline semqueue() 53{ 54 lock(listlock); 55 assert !onlist[_pid]; 56 onlist[_pid] = 1; 57 unlock(listlock) 58} 59 60inline semdequeue() 61{ 62 lock(listlock); 63 assert onlist[_pid]; 64 onlist[_pid] = 0; 65 waiting[_pid] = 0; 66 unlock(listlock) 67} 68 69inline semwakeup(n) 70{ 71 byte i, j; 72 73 lock(listlock); 74 i = 0; 75 j = n; 76 do 77 :: (i < N && j > 0) -> 78 if 79 :: onlist[i] && waiting[i] -> 80 atomic { printf("kicked %d\n", i); 81 waiting[i] = 0 }; 82 wakeup(i); 83 j-- 84 :: else 85 fi; 86 i++ 87 :: else -> break 88 od; 89 /* reset i and j to reduce state space */ 90 i = 0; 91 j = 0; 92 unlock(listlock) 93} 94 95inline semrelease(n) 96{ 97 atomic { value = value+n; printf("release %d\n", n); }; 98 semwakeup(n) 99} 100 101inline canacquire() 102{ 103 atomic { value > 0 -> value--; }; 104 acquired[_pid] = 1 105} 106 107#define semawoke() !waiting[_pid] 108 109inline semacquire(block) 110{ 111 if 112 :: atomic { canacquire() -> printf("easy acquire\n"); } -> 113 goto out 114 :: else 115 fi; 116 if 117 :: !block -> goto out 118 :: else 119 fi; 120 121 semqueue(); 122 do 123 :: skip -> 124 waiting[_pid] = 1; 125 if 126 :: atomic { canacquire() -> printf("hard acquire\n"); } -> 127 break 128 :: else 129 fi; 130 sleep(semawoke()) 131 if 132 :: interrupted -> 133 printf("%d interrupted\n", _pid); 134 break 135 :: !interrupted 136 fi 137 od; 138 semdequeue(); 139 if 140 :: !waiting[_pid] -> 141 semwakeup(1) 142 :: else 143 fi; 144out: 145 assert (!block || interrupted || acquired[_pid]); 146 assert !(interrupted && acquired[_pid]); 147 assert !waiting[_pid]; 148 printf("%d done\n", _pid); 149} 150 151active[N] proctype acquire() 152{ 153 bit interrupted; 154 155 semacquire(1); 156 printf("%d finished\n", _pid); 157 skip 158} 159 160active proctype release() 161{ 162 byte k; 163 164 k = 0; 165 do 166 :: k < N -> 167 semrelease(1); 168 k++; 169 :: else -> break 170 od; 171 skip 172} 173 174/* 175 * If this guy, the highest-numbered proc, sticks 176 * around, then everyone else sticks around. 177 * This makes sure that we get a state line for 178 * everyone in a proc dump. 179 */ 180active proctype dummy() 181{ 182end: 0; 183} 184