Fill in details of QRCU-like benchmark
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index eb029ca..87a7040 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -1377,23 +1377,61 @@
says otherwise (see Section~5.1 of the paper at the bottom of page~12).
Which is it?
-I do not know, as I never have been able to track down the code in which
-Algave, Kroening, and Tautschig found a flaw, though the authors did
-point out that the concurrency benchmarks are not necessarily equivalent
-to the real-world examples that they were derived from.
-In some sense, it does not matter, as QRCU never was accepted into the
-Linux kernel, nor to the best of my knowledge was it ever used in any
-other production software.
+It turns out that both are correct!
+When QRCU was added to a suite of formal-verification benchmarks,
+its memory barriers were omitted, thus resulting in a buggy version
+of QRCU.
+So the real news here is that a number of formal-verification tools
+incorrectly proved this buggy QRCU correct.
+And this is why formal-verification tools themselves should be tested
+using bug-injected versions of the code being verified.
+If a given tool cannot find the injected bugs, then that tool is
+clearly untrustworthy.
-However, if you do intend to use QRCU, please take care.
+\QuickQuiz{}
+ But different formal-verification tools are often designed to
+ locate particular classes of bugs.
+ For example, very few formal-verification tools will find
+ an error in the specification.
+ So isn't this ``clearly untrustworthy'' judgment a bit harsh?
+\QuickQuizAnswer{
+ It is certainly true that many formal-verification tools are
+ specialized in some way.
+ For example, Promela does not handle realistic memory models
+ (though they can be programmed into
+ Promela~\cite{Desnoyers:2013:MSM:2506164.2506174}),
+ CBMC~\cite{EdmundClarke2004CBMC} does not detect probabilistic
+ hangs and deadlocks, and
+ Nidhugg~\cite{CarlLeonardsson2014Nidhugg} does not detect
+ bugs involving data nondeterminism.
+ But this means that that these tools cannot be trusted to find
+ bugs that they are not designed to locate.
+
+ And therefore people creating formal-verification tools should
+ ``tell the truth on the label'', clearly calling out what
+ classes of bugs their tools can and cannot detect.
+ Otherwise, the first time a practitioner finds a tool
+ failing to detect a bug, that practitioner is likely to
+ make extremely harsh and extremely public denunciations
+ of that tool.
+ Yes, yes, there is something to be said for putting your
+ best foot forward, but putting it too far forward without
+ appropriate disclaimers can easily trigger a land mine of
+ negative reaction that your tool might or might not be able
+ to recover from.
+
+ You have been warned!
+} \QuickQuizEnd
+
+Therefore, if you do intend to use QRCU, please take care.
Its proofs of correctness might or might not themselves be correct.
Which is one reason why formal verification is unlikely to
-completely replace testing.
+completely replace testing, as Donald Knuth pointed out so long ago.
\QuickQuiz{}
Given that we have two independent proofs of correctness for
the QRCU algorithm described herein, and given that the
- proof of incorrectness covers what is likely a different
+ proof of incorrectness covers what is known to be a different
algorithm, why is there any room for doubt?
\QuickQuizAnswer{
There is always room for doubt.
