sys/src/9/port/semaphore.p

   1 /*
   2 spin -a semaphore.p
   3 pcc -DSAFETY -DREACH -DMEMLIM'='500 -o pan pan.c
   4 pan -i
   5 rm pan.* pan
   6
   7 */
   8
   9 #define N 3
  10
  11 bit listlock;
  12 byte value;
  13 bit onlist[N];
  14 bit waiting[N];
  15 bit sleeping[N];
  16 bit acquired[N];
  17
  18 inline lock(x)
  19 {
  20         atomic { x == 0; x = 1 }
  21 }
  22
  23 inline unlock(x)
  24 {
  25         assert x==1;
  26         x = 0
  27 }
  28
  29 inline 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
  44 inline wakeup(id)
  45 {
  46         if
  47         :: sleeping[id] == 1 -> sleeping[id] = 0
  48         :: else
  49         fi
  50 }
  51
  52 inline semqueue()
  53 {
  54         lock(listlock);
  55         assert !onlist[_pid];
  56         onlist[_pid] = 1;
  57         unlock(listlock)
  58 }
  59
  60 inline semdequeue()
  61 {
  62         lock(listlock);
  63         assert onlist[_pid];
  64         onlist[_pid] = 0;
  65         waiting[_pid] = 0;
  66         unlock(listlock)
  67 }
  68
  69 inline 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
  95 inline semrelease(n)
  96 {
  97         atomic { value = value+n; printf("release %d\n", n); };
  98         semwakeup(n)
  99 }
 100
 101 inline canacquire()
 102 {
 103         atomic { value > 0 -> value--; };
 104         acquired[_pid] = 1
 105 }
 106
 107 #define semawoke() !waiting[_pid]
 108
 109 inline 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;
 144 out:
 145         assert (!block || interrupted || acquired[_pid]);
 146         assert !(interrupted && acquired[_pid]);
 147         assert !waiting[_pid];
 148         printf("%d done\n", _pid);
 149 }
 150
 151 active[N] proctype acquire()
 152 {
 153         bit interrupted;
 154
 155         semacquire(1);
 156         printf("%d finished\n", _pid);
 157         skip
 158 }
 159
 160 active 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  */
 180 active proctype dummy()
 181 {
 182 end:    0;
 183 }