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