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.
9 (You may need to install Spin
, available at http
://spinroot.com
/.
)
11 After a successful run spin prints something like
:
13 unreached in proctype consumer
15 unreached in proctype producer
18 After an unsuccessful run
, the spinp script prints
19 an execution trace that causes a deadlock.
21 The safe body of producer reads
:
24 x
= value
; value
= x
+ 1; x
= 0;
29 If this is changed to
:
31 x
= value
; value
= x
+ 1; x
= 0;
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.
45 x
= value
; value
= x
+ 1; x
= 0;
50 then nothing bad happens
: it is okay to wakeup after release
51 instead of before
, although it seems morally wrong.
63 atomic
{ x
== 0; x
= 1 }
72 inline sleep
(cond
, lk
)
74 assert
!sleeping
[_pid
];
79 atomic
{ release
(lk
); sleeping
[_pid
] = 1 };
97 active
[N
] proctype consumer
()
105 sleep
(value
> 0, lk
);
106 x
= value
; value
= x
- 1; x
= 0;
116 active
[N
] proctype producer
()
124 x
= value
; value
= x
+ 1; x
= 0;