formal/formal.tex

% formal/formal.tex

\QuickQuizChapter{chp:formal:Formal Verification}{Formal Verification}

\OriginallyPublished{Appendix}{chp:formal:Formal Verification}{Formal Verification}{Linux Weekly News}{PaulEMcKenney2007QRCUspin,PaulEMcKenney2008dynticksRCU,PaulEMcKenney2011ppcmem}

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.
In addition, a proof of correctness cannot be expected to find errors
in your assumptions, shortcomings in the requirements,
misunderstandings of the underlying software or hardware primitives,
or errors that you did not think to construct a proof for.
This means that formal methods can never replace testing, however,
formal methods are nevertheless a valuable addition to your validation toolbox.

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~\ref{sec:formal:What are Promela and Spin?} provide an
introduction to Promela and Spin,
Section~\ref{sec:formal:Promela Example: Non-Atomic Increment}
demonstrates use of Promela and Spin to find a race in a non-atomic increment
example,
Section~\ref{sec:formal:Promela Example: Atomic Increment}
uses Promela and Spin to validate a similar atomic-increment example,
Section~\ref{sec:formal:How to Use Promela}
gives an overview of using Promela and Spin,
Section~\ref{sec:formal:Promela Example: Locking}
demonstrates a Promela model of a spinlock,
Section~\ref{sec:formal:Promela Example: QRCU}
applies Promela and spin to validate a simple RCU implementation,
Section~\ref{sec:formal:Promela Parable: dynticks and Preemptible RCU}
applies Promela to validate an interface between preemptible RCU and
the dyntick-idle energy-conservation feature in the Linux kernel,
Section~\ref{sec:formal:Simplicity Avoids Formal Verification}
presents a simpler interface that does not require formal verification,
Section~\ref{sec:formal:Formal Verification and Memory Ordering}
descripes the PPCMEM tool that understands ARM and Power memory ordering,
and finally
Section~\ref{sec:formal:Summary}
sums up use of formal-verification tools for verifying parallel algorithms.

\input{formal/spinhint}
\input{formal/dyntickrcu}
\input{formal/cppmem}

\section{Summary}
\label{sec:formal:Summary}

Promela and CPPMEM are very powerful tools for validating small
parallel algorithms, but they should not be the only tools in your
toolbox.
The QRCU experience is a case in point: given the Promela validation,
the proof of correctness, and several
rcutorture
% @@@ <A HREF="http://git.kernel.org/?p=linux/kernel/git/torvalds/linux-2.6.git;a=blob;hb=HEAD;f=Documentation/RCU/torture.txt">rcutorture</A>
runs, I now feel
reasonably confident in the QRCU algorithm and its implementation.
But I would certainly not feel so confident given only one of the three!

Nevertheless, if your code is so complex that you find yourself
relying too heavily on validation
tools, you should carefully rethink your design.
For example, a complex implementation of the dynticks interface for
preemptible RCU that was presented in
Section~\ref{sec:formal:Promela Parable: dynticks and Preemptible RCU}
turned out to
have a much simpler alternative implementation, as discussed in
Section~\ref{sec:formal:Simplicity Avoids Formal Verification}.
All else being equal, a simpler implementation is much better than
a mechanical proof for a complex implementation!