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 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.