Spin & Plan 9

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.

Jim Mckie: mentions the bug

Dave Presotto: explains it in detail

Dave Presotto: explains further

Richard Miller: summarizes

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

Rob Pike: model reply

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

Richard Miller: agrees

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)

Dave Presotto: response

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.

stripped-down C version

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.

current version

revision history


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.

semaphore manual page

rendezvous manual page

current semaphore implementation (bottom)

spin model for semaphores

Russ Cox