This page documents the history of the use of the protocol verifier Spin in Plan 9.
Sleep and wakeup
The canonical use has been the verification of the kernel’s sleep and wakeup primitives.
The implementation of sleep and wakeup was done by Rob Pike, Dave Presotto, and Ken Thompson. Gerard Holzmann verified the implementation using Spin. They published a paper about this experience in 1991.
- Process Sleep and Wakeup on a Shared-memory Multiprocessor
(The paper describing the early verification.)
- Promela model for sleep and wakeup
This model verifies not just sleep and wakeup, as discussed in the paper, but also postnote, which complicates the implementation considerably.
- Sleep/wakeup from February 1990. Earliest on record
This version, the earliest version available, matches the 1991 paper.
The earlier, buggy versions are lost to history.
- Inferno manual page for sleep and wakeup
A good description of their semantics. Applies to Plan 9 versions too.
The sleep and wakeup routines were rewritten for Brazil, the internal successor to Plan 9.
In April 1997, Jim McKie posted a note to the Plan 9 mailing list 9fans about finding a bug in that new sleep and wakeup code, sparking a discussion of memory ordering on the Pentium Pro.
- Dave Presotto: explains it in detail
- Dave Presotto: explains further
- Dave Presotto: details from Mike Haertel about Pentium Pro
- Sleep/wakeup from May 1998. Final version used in response to this bug.
In December 1999, a post to 9fans asked for the Promela model used for the paper. In response Rob Pike posted the model linked above.
- Gergo Fodemesi: model request
In July 2000, the topic came up again in response to an off-hand comment I made about not using lock-free data structures. At that time Jim McKie and Dave Presotto were tracking down further problems related to the queued writes.
- Richard Miller: sleep/wakeup are lock-free
- Jim McKie: sleep/wakeup were broken even with locks
- Richard Miller: further explanation of comment
- Dave Presotto: why unlocked access is okay here
- Dave Presotto: explains why unlocked access at all
- Richard Miller: suggestion how to reintroduce locks
- Dave Presotto: possible problem with suggestion
- Richard Miller: acknowledges problem
- Dave Presotto: points out that postnote is the real issue
- Richard Miller: further discussion of problem
- Dave Presotto: points out that postnote is the real issue (2)
- Richard Miller: new suggestion
In September 2000, someone’s mailer burped, resending the December 1999 post asking about a Promela model. In response, Dave Presotto posted saying that he was still working on sleep/wakeup/postnote, based on Richard Miller’s suggestion, and that Gerard Holzmann was verifying the new solution.
- Gergo Fodemesi: model request (repeated)
- Sleep/wakeup from September 2000. Final verified version still in use.
In March 2006, Gerard Holzmann dug up his models from September 2000 and mailed them to me with permission to post them here. The model was generated from a standalone version of the actual C code using the program that became modex.
- model generated from C version
The file /sys/src/9/port/proc.c in the Plan 9 kernel contains the implementation of sleep and wakeup. The current version as well as all previous versions back to February 1990 are available.
Semaphores
In March 2006, Sape Mullender and Russ Cox added semaphores to the Plan 9 kernel, to provide a guaranteed-non-blocking way for real-time processes to wake other processes. (Using rendezvous would block the real-time process if the other process was not waiting at the rendezvous point.)
The implementation is subtle because it manipulates a semaphore kept in user space, and user memory cannot be accessed while holding locks. The full implementation is at the bottom of /sys/src/9/port/sysproc.c.
The implementation was verified using spin, which found two subtle bugs. The spin model is also part of the distribution.
- current semaphore implementation (bottom)
Russ Cox
rsc@swtch.com