semaphore.p

Version: - FREEBSD - FREEBSD-13-STABLE - FREEBSD-13-0 - FREEBSD-12-STABLE - FREEBSD-12-0 - FREEBSD-11-STABLE - FREEBSD-11-0 - FREEBSD-10-STABLE - FREEBSD-10-0 - FREEBSD-9-STABLE - FREEBSD-9-0 - FREEBSD-8-STABLE - FREEBSD-8-0 - FREEBSD-7-STABLE - FREEBSD-7-0 - FREEBSD-6-STABLE - FREEBSD-6-0 - FREEBSD-5-STABLE - FREEBSD-5-0 - FREEBSD-4-STABLE - FREEBSD-3-STABLE - FREEBSD22 - l41 - OPENBSD - linux-2.6 - MK84 - PLAN9 - xnu-8792
SearchContext: - none - 3 - 10

    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 }

Cache object: 0458db0c62e401c37f3fcf75b3487e35

[ source navigation ] [ diff markup ] [ identifier search ] [ freetext search ] [ file search ] [ list types ] [ track identifier ]

This page is part of the FreeBSD/Linux Linux Kernel Cross-Reference, and was automatically generated using a modified version of the LXR engine.

FreeBSD/Linux Kernel Cross Reference sys/port/semaphore.p

FreeBSD/Linux Kernel Cross Reference
sys/port/semaphore.p