* Incomplete sentence in commit 405f3f465f7f
@ 2017-11-02 13:32 Akira Yokosawa
2017-11-03 13:59 ` Paul E. McKenney
0 siblings, 1 reply; 6+ messages in thread
From: Akira Yokosawa @ 2017-11-02 13:32 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
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?
Thanks, Akira
^ permalink raw reply [flat|nested] 6+ messages in thread* Re: Incomplete sentence in commit 405f3f465f7f 2017-11-02 13:32 Incomplete sentence in commit 405f3f465f7f Akira Yokosawa @ 2017-11-03 13:59 ` Paul E. McKenney 2017-11-03 14:53 ` Akira Yokosawa 0 siblings, 1 reply; 6+ messages in thread From: Paul E. McKenney @ 2017-11-03 13:59 UTC (permalink / raw) To: Akira Yokosawa; +Cc: perfbook 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? 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}. Although formal verification is finally starting to show some promise, including more-recent L4 verifications involving greater ^ permalink raw reply related [flat|nested] 6+ messages in thread
* Re: Incomplete sentence in commit 405f3f465f7f 2017-11-03 13:59 ` Paul E. McKenney @ 2017-11-03 14:53 ` Akira Yokosawa 2017-11-03 15:45 ` Paul E. McKenney 0 siblings, 1 reply; 6+ messages in thread From: Akira Yokosawa @ 2017-11-03 14:53 UTC (permalink / raw) To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa 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? Thanks, Akira > > Although formal verification is finally starting to show some > promise, including more-recent L4 verifications involving greater > > ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Incomplete sentence in commit 405f3f465f7f 2017-11-03 14:53 ` Akira Yokosawa @ 2017-11-03 15:45 ` Paul E. McKenney 2017-11-03 22:06 ` Akira Yokosawa 0 siblings, 1 reply; 6+ messages in thread From: Paul E. McKenney @ 2017-11-03 15:45 UTC (permalink / raw) To: Akira Yokosawa; +Cc: perfbook 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 ^ permalink raw reply related [flat|nested] 6+ messages in thread
* Re: Incomplete sentence in commit 405f3f465f7f 2017-11-03 15:45 ` Paul E. McKenney @ 2017-11-03 22:06 ` Akira Yokosawa 2017-11-03 22:56 ` Paul E. McKenney 0 siblings, 1 reply; 6+ messages in thread From: Akira Yokosawa @ 2017-11-03 22:06 UTC (permalink / raw) To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa On 2017/11/03 08:45:50 -0700, Paul E. McKenney wrote: > 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. Acked-by: Akira Yokosawa <akiyks@gmail.com> > > 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 > > ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Incomplete sentence in commit 405f3f465f7f 2017-11-03 22:06 ` Akira Yokosawa @ 2017-11-03 22:56 ` Paul E. McKenney 0 siblings, 0 replies; 6+ messages in thread From: Paul E. McKenney @ 2017-11-03 22:56 UTC (permalink / raw) To: Akira Yokosawa; +Cc: perfbook On Sat, Nov 04, 2017 at 07:06:54AM +0900, Akira Yokosawa wrote: > On 2017/11/03 08:45:50 -0700, Paul E. McKenney wrote: > > 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. > > Acked-by: Akira Yokosawa <akiyks@gmail.com> Applied and pushed, thank you! 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 > > > > > ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2017-11-03 22:56 UTC | newest] Thread overview: 6+ messages (download: mbox.gz follow: Atom feed -- links below jump to the message on this page -- 2017-11-02 13:32 Incomplete sentence in commit 405f3f465f7f Akira Yokosawa 2017-11-03 13:59 ` Paul E. McKenney 2017-11-03 14:53 ` Akira Yokosawa 2017-11-03 15:45 ` Paul E. McKenney 2017-11-03 22:06 ` Akira Yokosawa 2017-11-03 22:56 ` Paul E. McKenney
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox