xv6

port of xv6 to x86-64
git clone http://frotz.net/git/xv6.git
Log | Files | Refs | README | LICENSE

sleep1.p (1990B)

      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