formal/formal.tex

% formal/formal.tex
% SPDX-License-Identifier: CC-BY-SA-3.0

\QuickQuizChapter{chp:Formal Verification}{Formal Verification}
%
\Epigraph{Beware of bugs in the above code; I have only proved it correct,
	  not tried it.}{\emph{Donald Knuth}}

\OriginallyPublished{Chapter}{chp: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,
Section~\ref{sec:formal:General-Purpose State-Space Search} provides an
introduction to the general-purpose state-space search tools Promela and Spin,
Section~\ref{sec:formal:Special-Purpose State-Space Search}
similarly introduces the special-purpose ppcmem and cppmem tools,
Section~\ref{sec:formal:Axiomatic Approaches}
looks at an example axiomatic approach,
Section~\ref{sec:formal:SAT Solvers}
briefly overviews SAT solvers,
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/ppcmem}
\input{formal/axiomatic}
\input{formal/sat}

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

The formal-verification techniques described in this chapter
are very powerful tools for validating small
parallel algorithms, but they should not be the only tools in your toolbox.
Despite decades of focus on formal verification, testing remains the
validation workhorse for large parallel software
systems~\cite{JonathanCorbet2006lockdep,DaveJones2011Trinity}.

It is nevertheless quite possible that this will not always be the case.
To see this, consider that there are more than one billion instances
of the Linux kernel as of 2013.
Suppose that the Linux kernel has a bug that manifests on average every million
years of runtime.
As noted at the end of the preceding chapter,
this bug will be appearing three times \emph{per day} across the installed
base.
But the fact remains that most formal validation techniques can be used
only on very small code bases.
So what is a concurrency coder to do?

One approach is to think in terms of finding the first bug, the first
relevant bug, the last relevant bug, and the last bug.

The first bug is normally found via inspection or compiler diagnostics.
Although the increasingly sophisticated diagnostics provided by modern
compilers might be considered to be a lightweight sort of formal
verification, it is not common to think of them in those terms.
This is in part due to an odd practitioner prejudice which says
``If I am using it, it cannot be formal verification'' on the one
hand, and the large difference in sophistication between compiler
diagnostics and verification research on the other.

Although the first relevant bug might be located via inspection or
compiler diagnostics, it is not unusual for these two steps to find
only typos and false positives.
Either way, the bulk of the relevant bugs, that is, those bugs that
might actually be encountered in production, will often be found via testing.

When testing is driven by anticipated or real use cases, it is not
uncommon for the last relevant bug to be located by testing.
This situation might motivate a complete rejection of formal verification,
however, irrelevant bugs have a bad habit of suddenly becoming relevant
at the least convenient moment possible, courtesy of black-hat attacks.
For security-critical software, which appears to be a continually
increasing fraction of the total, there can thus be strong motivation
to find and fix the last bug.
Testing is demonstrably unable to find the last bug, so there is a
possible role for formal verification.
That is, there is such a role if and only if formal verification
proves capable of growing into it.
As this chapter has shown, current formal verification systems are
extremely limited.

Another approach is to consider that
formal verification is often much harder to use than is testing.
This is of course in part a cultural statement, and there is every reason
to hope that formal verification will be perceived to be easier as more
people become familiar with it.
That said, very simple test harnesses can find significant bugs in arbitrarily
large software systems.
In contrast, the effort required to apply formal verification seems to
increase dramatically as the system size increases.

I have nevertheless made occasional use of formal verification
for more than 20 years, playing to formal verification's strengths,
namely design-time verification of small complex portions of the overarching
software construct.
The larger overarching software construct is of course validated by testing.

\QuickQuiz{}
	In light of the full verification of the L4 microkernel,
	isn't this limited view of formal verification just a little
	bit obsolete?
\QuickQuizAnswer{
	Unfortunately, no.

	The first full verification of the L4 microkernel was a tour de force,
	with a large number of Ph.D.~students hand-verifying code at a
	very slow per-student rate.
	This level of effort could not be applied to most software projects
	because the rate of change is just too great.
	Furthermore, although the L4 microkernel is a large software
	artifact from the viewpoint of formal verification, it is tiny
	compared to a great number of projects, including LLVM,
	gcc, the Linux kernel, Hadoop, MongoDB, and a great many others.

	Although formal verification is finally starting to show some
	promise, including more-recent L4 verifications involving greater
	levels of automation, it currently has no chance of completely
	displacing testing in the foreseeable future.
	And although I would dearly love to be proven wrong on this point,
	please note that such a proof will be in the form of a real tool
	that verifies real software, not in the form of a large body of
	rousing rhetoric.
} \QuickQuizEnd

One final approach is to consider the following two definitions and the
consequence that they imply:

\begin{description}
\item[Definition:]	Bug-free programs are trivial programs.
\item[Definition:]	Reliable programs have no known bugs.
\item[Consequence:]	Any non-trivial reliable program contains at least
			one as-yet-unknown bug.
\end{description}

From this viewpoint, any advances in validation and verification can
have but two effects: (1)~An increase in the number of trivial programs or
(2)~A decrease in the number of reliable programs.
Of course, the human race's increasing reliance on multicore systems and
software provides extreme motivation for a very sharp increase in the
number of trivial programs!

However, if your code is so complex that you find yourself
relying too heavily on formal-verification
tools, you should carefully rethink your design, especially if your
formal-verification tools require your code to be hand-translated
to a special-purpose language.
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!

And the open challenge to those working on formal verification techniques
and systems is to prove this summary wrong!