E. Formal Verification
Keywords: perfbook_html

#
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

- E.1 What are Promela and Spin?
- E.2 Promela Example: Non-Atomic Increment
- E.3 Promela Example: Atomic Increment
  - E.3.1 Combinatorial Explosion
- E.4 How to Use Promela
  - E.4.1 Promela Peculiarities
  - E.4.2 Promela Coding Tricks
- E.5 Promela Example: Locking
- E.6 Promela Example: QRCU
  - E.6.1 Running the QRCU Example
  - E.6.2 How Many Readers and Updaters Are Really Needed?
  - E.6.3 Alternative Approach: Proof of Correctness
  - E.6.4 Alternative Approach: More Capable Tools
  - E.6.5 Alternative Approach: Divide and Conquer
- E.7 Promela Parable: dynticks and Preemptible RCU
  - E.7.1 Introduction to Preemptible RCU and dynticks
    - E.7.1.1 Task Interface
    - E.7.1.2 Interrupt Interface
    - E.7.1.3 Grace-Period Interface
  - E.7.2 Validating Preemptible RCU and dynticks
    - E.7.2.1 Basic Model
    - E.7.2.2 Validating Safety
    - E.7.2.3 Validating Liveness
    - E.7.2.4 Interrupts
    - E.7.2.5 Validating Interrupt Handlers
    - E.7.2.6 Validating Nested Interrupt Handlers
    - E.7.2.7 Validating NMI Handlers
  - E.7.3 Lessons (Re)Learned
- E.8 Simplicity Avoids Formal Verification
  - E.8.1 State Variables for Simplified Dynticks Interface
  - E.8.2 Entering and Leaving Dynticks-Idle Mode
  - E.8.3 NMIs From Dynticks-Idle Mode
  - E.8.4 Interrupts From Dynticks-Idle Mode
  - E.8.5 Checking For Dynticks Quiescent States
  - E.8.6 Discussion
- E.9 Summary