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@xxxxxxxxx>
> Date: Tue, 31 Oct 2017 00:48:11 +0900
> Subject: [PATCH] formal/regression: Fix typo
>
> Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
> ---
> 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
>
--
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
