E. Formal Verification

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.



Subsections
Paul E. McKenney 2011-12-16