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 06:59:48 -0700 [thread overview]
Message-ID: <20171103135948.GI3624@linux.vnet.ibm.com> (raw)
In-Reply-To: <765342ad-03aa-180f-308f-010a6d503b5d@gmail.com>
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
next prev parent reply other threads:[~2017-11-03 13:59 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 [this message]
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
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=20171103135948.GI3624@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 a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox