Parallel algorithms can be hard to write, and even harder to debug. Testing, though essential, is insufficient, as fatal race conditions can have extremely low probabilities of occurrence. Proofs of correctness can be valuable, but in the end are just as prone to human error as is the original algorithm.
It would be very helpful to have a tool that could somehow locate
all race conditions.
A number of such tools exist, for example,
the language Promela and its compiler Spin, which are described in
this chapter.
Section provide an
introduction to Promela and Spin,
Section
demonstrates use of Promela and Spin to find a race in a non-atomic increment
example,
Section
uses Promela and Spin to validate a similar atomic-increment example,
Section
gives an overview of using Promela and Spin,
Section
demonstrates a Promela model of a spinlock,
Section
applies Promela and spin to validate a simple RCU implementation,
Section
applies Promela to validate an interface between preemptible RCU and
the dyntick-idle energy-conservation feature in the Linux kernel,
Section
presents a simpler interface that does not require formal verification,
and finally
Section
sums up use of formal-verification tools for verifying parallel algorithms.