Re: Incomplete sentence in commit 405f3f465f7f

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

On Fri, Nov 03, 2017 at 11:53:00PM +0900, Akira Yokosawa wrote:
> On 2017/11/03 06:59:48 -0700, Paul E. McKenney wrote:
> > On Thu, Nov 02, 2017 at 10:32:30PM +0900, Akira Yokosawa wrote:
> >> Hi Paul,
> >>
> >> In commit 405f3f465f7f ("debugging,formal: Update for increased Linux kernel usage"),
> >> there is an incomplete hunk of formal/formal.tex
> >>
> >> @@ -135,6 +147,7 @@ The larger overarching software construct is of course validated by testing.
> >>         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.
> >> +       In addition, 
> >>
> >>         Although formal verification is finally starting to show some
> >>         promise, including more-recent L4 verifications involving greater
> >>
> >> What was your intention here?
> > 
> > Those two words do leave quite a bit to the imagination, don't they?
> 
> Indeed. ;-)
> 
> > 
> > Good catch, thank you!  Does the patch below help?
> > 
> > 							Thanx, Paul
> > 
> > -----------------------------------------------------------------------
> > 
> > commit 7f417104712459c70117333aa392d680350cae90
> > Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > Date:   Fri Nov 3 06:58:10 2017 -0700
> > 
> >     formal: Complete verification-limitations thought in QQ12.33
> >     
> >     Reported-by: Akira Yokosawa <akiyks@gmail.com>
> >     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > 
> > diff --git a/formal/formal.tex b/formal/formal.tex
> > index 7c1aeac7d112..2fa410252197 100644
> > --- a/formal/formal.tex
> > +++ b/formal/formal.tex
> > @@ -147,7 +147,9 @@ The larger overarching software construct is of course validated by testing.
> >  	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.
> > -	In addition, 
> > +	In addition, this verification did have limits, as the researchers
> > +	freely admit, to their credit:
> > +	\url{https://wiki.sel4.systems/FrequentlyAskedQuestions#What_does_seL4.27s_formal_verification_mean.3F}.
> 
> The next item in the page:
> 
>     https://wiki.sel4.systems/FrequentlyAskedQuestions#Does_seL4_have_zero_bugs.3F
> 
> looks more relevant to the "limits", doesn't it?

Fair enough, please see below.

							Thanx, Paul

------------------------------------------------------------------------

commit 715dff95ec40599a67c6835be78a98de2d45c251
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date:   Fri Nov 3 06:58:10 2017 -0700

    formal: Complete verification-limitations thought in QQ12.33
    
    Reported-by: Akira Yokosawa <akiyks@gmail.com>
    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

diff --git a/formal/formal.tex b/formal/formal.tex
index 7c1aeac7d112..219395354106 100644
--- a/formal/formal.tex
+++ b/formal/formal.tex
@@ -147,7 +147,9 @@ The larger overarching software construct is of course validated by testing.
 	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.
-	In addition, 
+	In addition, this verification did have limits, as the researchers
+	freely admit, to their credit:
+	\url{https://wiki.sel4.systems/FrequentlyAskedQuestions#Does_seL4_have_zero_bugs.3F}.

 	Although formal verification is finally starting to show some
 	promise, including more-recent L4 verifications involving greater