* 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