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@xxxxxxxxxxxxxxxxxx>
>>> Date: Fri Nov 3 06:58:10 2017 -0700
>>>
>>> formal: Complete verification-limitations thought in QQ12.33
>>>
>>> Reported-by: Akira Yokosawa <akiyks@xxxxxxxxx>
>>> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
>>>
>>> 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@xxxxxxxxx>
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit 715dff95ec40599a67c6835be78a98de2d45c251
> Author: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
> Date: Fri Nov 3 06:58:10 2017 -0700
>
> formal: Complete verification-limitations thought in QQ12.33
>
> Reported-by: Akira Yokosawa <akiyks@xxxxxxxxx>
> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
>
> 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
>
>
--
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
