i386/MIT/src.xv6/sleep1.p

   1 /*
   2 This file defines a Promela model for xv6's
   3 acquire, release, sleep, and wakeup, along with
   4 a model of a simple producer/consumer queue.
   5
   6 To run:
   7         spinp sleep1.p
   8
   9 (You may need to install Spin, available at http://spinroot.com/.)
  10
  11 After a successful run spin prints something like:
  12
  13         unreached in proctype consumer
  14                 (0 of 37 states)
  15         unreached in proctype producer
  16                 (0 of 23 states)
  17
  18 After an unsuccessful run, the spinp script prints
  19 an execution trace that causes a deadlock.
  20
  21 The safe body of producer reads:
  22
  23                 acquire(lk);
  24                 x = value; value = x + 1; x = 0;
  25                 wakeup(0);
  26                 release(lk);
  27                 i = i + 1;
  28
  29 If this is changed to:
  30
  31                 x = value; value = x + 1; x = 0;
  32                 acquire(lk);
  33                 wakeup(0);
  34                 release(lk);
  35                 i = i + 1;
  36
  37 then a deadlock can happen, because the non-atomic
  38 increment of value conflicts with the non-atomic
  39 decrement in consumer, causing value to have a bad value.
  40 Try this.
  41
  42 If it is changed to:
  43
  44                 acquire(lk);
  45                 x = value; value = x + 1; x = 0;
  46                 release(lk);
  47                 wakeup(0);
  48                 i = i + 1;
  49
  50 then nothing bad happens: it is okay to wakeup after release
  51 instead of before, although it seems morally wrong.
  52 */
  53
  54 #define ITER 4
  55 #define N 2
  56
  57 bit lk;
  58 byte value;
  59 bit sleeping[N];
  60
  61 inline acquire(x)
  62 {
  63         atomic { x == 0; x = 1 }
  64 }
  65
  66 inline release(x)
  67 {
  68         assert x==1;
  69         x = 0
  70 }
  71
  72 inline sleep(cond, lk)
  73 {
  74         assert !sleeping[_pid];
  75         if
  76         :: cond ->
  77                 skip
  78         :: else ->
  79                 atomic { release(lk); sleeping[_pid] = 1 };
  80                 sleeping[_pid] == 0;
  81                 acquire(lk)
  82         fi
  83 }
  84
  85 inline wakeup()
  86 {
  87         w = 0;
  88         do
  89         :: w < N ->
  90                 sleeping[w] = 0;
  91                 w = w + 1
  92         :: else ->
  93                 break
  94         od
  95 }
  96
  97 active[N] proctype consumer()
  98 {
  99         byte i, x;
 100
 101         i = 0;
 102         do
 103         :: i < ITER ->
 104                 acquire(lk);
 105                 sleep(value > 0, lk);
 106                 x = value; value = x - 1; x = 0;
 107                 release(lk);
 108                 i = i + 1;
 109         :: else ->
 110                 break
 111         od;
 112         i = 0;
 113         skip
 114 }
 115
 116 active[N] proctype producer()
 117 {
 118         byte i, x, w;
 119
 120         i = 0;
 121         do
 122         :: i < ITER ->
 123                 acquire(lk);
 124                 x = value; value = x + 1; x = 0;
 125                 release(lk);
 126                 wakeup();
 127                 i = i + 1;
 128         :: else ->
 129                 break
 130         od;
 131         i = 0;
 132         skip
 133 }
 134