On Thu, Nov 02, 2017 at 11:19:45PM +0900, Akira Yokosawa wrote:
> Hi Paul
>
> I couldn't follow the reasoning around the following _artificial_ hunk.
>
> diff --git a/formal/regression.tex b/formal/regression.tex
> index 29cb787..9831b9d 100644
> --- a/formal/regression.tex
> +++ b/formal/regression.tex
> @@ -387,6 +387,7 @@ To see this, keep in mind that on average, every six fixes introduces
> a bug.
> Therefore, fixing the 24 bugs, which had a combine mean time to failure
> of about 40,000 years, will introduce three more bugs.
> +???
> These three bugs most likely fail more often than once per 13,000 years,
> so the reliability of the software has decreased.
>
> Where did the "once per 13,000 years" come from?
> 13,000 was derived from 40,000/3?
>
> But in this argument, original 24 bugs are fixed, and 3 new bugs are introduced.
> We have no idea what failure rate the new bugs would have, don't we???
>
> What am I missing?
You are not missing much, but it looks like I was thinking backwards.
For one thing, I was using an outdated bug-injection rate, more recent
figures are 7%. I updated this, (hopefully) fixed and clarified the
reasoning, and added a citation for the 7%. How does the patch below
look?
Thanx, Paul
------------------------------------------------------------------------
commit b1efdff66eb050317232dd36bd4b1385ed24524d
Author: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
Date: Thu Nov 2 16:50:44 2017 -0700
formal: Update bug-injection rate and clarify reasoning
New data says 7% instead of 1-of-6, and the math was backwards.
Reported-by: Akira Yokosawa <akiyks@xxxxxxxxx>
Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
diff --git a/formal/regression.tex b/formal/regression.tex
index 29cb78709f76..479ae020b518 100644
--- a/formal/regression.tex
+++ b/formal/regression.tex
@@ -374,28 +374,68 @@ type of validation effort.
Clearly, false positives are to be avoided.
But even in the absense of false postives, there are bugs and there are bugs.
-For example, suppose that a software artifact had exactly 24 remaining
+For example, suppose that a software artifact had exactly 100 remaining
bugs, each of which manifested on average once every million years
of runtime.
Suppose further that an omniscient formal-verification tool located
-all 24 bugs, which the developers duly fixed.
+all 100 bugs, which the developers duly fixed.
What happens to the reliability of this software artifact?
-The reliability \emph{decreases}.
+The perhaps surprising answer is that the reliability \emph{decreases}.
-To see this, keep in mind that on average, every six fixes introduces
-a bug.
-Therefore, fixing the 24 bugs, which had a combine mean time to failure
-of about 40,000 years, will introduce three more bugs.
-These three bugs most likely fail more often than once per 13,000 years,
-so the reliability of the software has decreased.
+To see this, keep in mind that historical experience indicates that
+about 7\% of fixes introduce a new bug~\cite{RexBlack2012SQA}.
+Therefore, fixing the 100 bugs, which had a combined mean time to failure
+(MTBF) of about 10,000 years, will introduce seven more bugs.
+Historical statistics indicate that each new bug will have an MTBF
+much less than 70,000 years.
+This in turn suggests that the combined MTBF of these seven new bugs
+will most likely be much less than 10,000 years, which in turn means
+that the well-intentioned fixing of the original 100 bugs actually
+decreased the reliability of the overall software.
+
+\QuickQuiz{}
+ How do we know that the MTBFs of known bugs is a good estimate
+ of the MTBFs of bugs that have not yet been located?
+\QuickQuizAnswer{
+ We don't, but it does not matter.
+
+ To see this, note that the 7\% figure only applies to injected
+ bugs that were subsequently located: It necessarily ignores
+ any injected bugs that were never found.
+ Therefore, the MTBF statistics of known bugs is likely to be
+ a good approximation of that of the injected bugs that are
+ subsequently located.
+
+ A key point in this whole section is that we should be more
+ concerned about bugs that inconvenience users than about
+ other bugs that never actually manifest.
+ This of course is \emph{not} to say that we should completely
+ ignore bugs that have not yet inconvenienced users, just that
+ we should properly prioritize our efforts so as to fix the
+ most important and urgent bugs first.
+} \QuickQuizEnd
+
+\QuickQuiz{}
+ But the formal-verification tools should immediately find all the
+ bugs introduced by the fixes, so why is this a problem?
+\QuickQuizAnswer{
+ It is a problem because real-world formal-verification tools
+ (as opposed to those that exist only in the imaginations of
+ the more vociferous proponents of formal verification) are
+ not omniscient, and thus are only able to locate certain types
+ of bugs.
+ For but one example, formal-verification tools are unlikely to
+ spot a bug corresponding to an omitted assertion or, equivalently,
+ a bug corresponding to an omitted portion of the specification.
+} \QuickQuizEnd
Worse yet, imagine another software artifact with one bug that fails
-once every day on average and 24 more that fail every million years
+once every day on average and 99 more that fail every million years
each.
-Suppose that a formal-verification tool located the 24 million-year
+Suppose that a formal-verification tool located the 99 million-year
bugs, but failed to find the one-day bug.
-Fixing the 24 bugs located will take time and effort, likely slightly
+Fixing the 99 bugs located will take time and effort, likely slightly
decrease reliability, and do nothing at all about the pressing
each-day failure that is likely causing much embarrassment and perhaps
much worse besides.
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
