On Fri, Nov 03, 2017 at 09:07:43AM +0900, Akira Yokosawa wrote:
> On 2017/11/02 16:53:44 -0700, Paul E. McKenney wrote:
> > 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?
>
> Nice clarification! Now the reasoning is easy to follow.
>
> Acked-by: Akira Yokosawa <akiyks@xxxxxxxxx>
Applied and pushed, thank you!
Thanx, Paul
> Thanks, Akira
>
> >
> > 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
