From: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
To: Akira Yokosawa <akiyks@gmail.com>
Cc: perfbook@vger.kernel.org
Subject: Re: [PATCH] formal/regression: Fix typo
Date: Mon, 30 Oct 2017 10:17:24 -0700 [thread overview]
Message-ID: <20171030171724.GV3659@linux.vnet.ibm.com> (raw)
In-Reply-To: <ea9123a0-7651-72c0-24d5-1b847b6b2efc@gmail.com>
On Tue, Oct 31, 2017 at 12:53:39AM +0900, Akira Yokosawa wrote:
> >From c313894cb1f877b1d8ef5303d59d97b187cf925e Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Tue, 31 Oct 2017 00:48:11 +0900
> Subject: [PATCH] formal/regression: Fix typo
>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> Hi Paul,
>
> Here are fixes of several typos in the new section.
> There are chances I'm guessing wrong in some of the hunks, though.
Good eyes, thank you very much! I applied this, but have not yet pushed
it out as it is blocked behind the patch I sent you, which I do not wish
to push until you are happy with it.
Thanx, Paul
> Thanks, Akira
> --
> formal/regression.tex | 10 +++++-----
> 1 file changed, 5 insertions(+), 5 deletions(-)
>
> diff --git a/formal/regression.tex b/formal/regression.tex
> index 39ca388..09d28e1 100644
> --- a/formal/regression.tex
> +++ b/formal/regression.tex
> @@ -60,7 +60,7 @@ and C++ code, but these tools work only on very small litmus tests,
> which normally means that you must extract the core of your
> mechanism---by hand.
> As with Promela and \co{spin}, both PPCMEM and \co{herd} are
> -extremely useful, but they are well-suited for regression suites.
> +extremely useful, but they are not well-suited for regression suites.
>
> In contrast, \co{cbmc} and Nidhugg can input C programs of reasonable
> (though still quite limited) size, and if their capabilities continue
> @@ -394,7 +394,7 @@ Worse yet, imagine another software artifact with one bug that fails
> once every day on average and 24 more that fail every million years
> each.
> Suppose that a formal-verification tool located the 24 million-year
> -bugs, but failed to fined the one-day bug.
> +bugs, but failed to find the one-day bug.
> Fixing the 24 bugs located will take time and effort, likely slightly
> decrease reliability, and do nothing at all about the pressing
> each-day failure that is likely causing much embarrassment and perhaps
> @@ -479,7 +479,7 @@ Despite requiring hand translation, Promela handles assertions
> in a natural way, so its fifth cell is green.
>
> PPCMEM usually requires hand translation due to the small size of litmus
> -tests that it support, so its first cell is orange.
> +tests that it supports, so its first cell is orange.
> It accurately handles several memory models, so its second cell is green.
> Its overhead is quite high, so its third cell is red.
> It provides a graphical display of relations among operations, which
> @@ -493,7 +493,7 @@ so \co{herd}'s first cell is also orange.
> It supports a wide variety of memory models, so its second cell is blue.
> It has reasonable overhead, so its third cell is yellow.
> Its bug-location and assertion capabilities are quite similar to those
> -of \co{cbmc}, so \co{herd} gets the same color for the next two cells.
> +of PPCMEM, so \co{herd} gets the same color for the next two cells.
>
> The \co{cbmc} tool inputs C code directly, so its first cell is blue.
> It supports a few memory models, so its second cell is yellow.
> @@ -515,7 +515,7 @@ so they are all yellow with question marks.
>
> Once again, please note that this table rates these tools for use in
> regression testing.
> -Just because many of them area poor fit for regression testing does
> +Just because many of them are poor fit for regression testing does
> not at all mean that they are useless, in fact,
> many of them have proven their worth many times over.
> Just not for regression testing.
> --
> 2.7.4
>
prev parent reply other threads:[~2017-10-30 17:22 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-10-30 15:53 [PATCH] formal/regression: Fix typo Akira Yokosawa
2017-10-30 17:17 ` 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=20171030171724.GV3659@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