123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183 |
- /*
- 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;
- }
|