From: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
To: Akira Yokosawa <akiyks@gmail.com>
Cc: perfbook@vger.kernel.org
Subject: Re: Incomplete sentence in commit 405f3f465f7f
Date: Fri, 3 Nov 2017 15:56:17 -0700 [thread overview]
Message-ID: <20171103225617.GS3624@linux.vnet.ibm.com> (raw)
In-Reply-To: <713ec1c9-1733-9132-f2bb-629f2b1f04dc@gmail.com>
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
> >
> >
>
prev parent reply other threads:[~2017-11-03 22:56 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
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 message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20171103225617.GS3624@linux.vnet.ibm.com \
--to=paulmck@linux.vnet.ibm.com \
--cc=akiyks@gmail.com \
--cc=perfbook@vger.kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.