From: "Paul E. McKenney" <paulmck@linux.ibm.com>
To: Akira Yokosawa <akiyks@gmail.com>
Cc: perfbook@vger.kernel.org
Subject: Re: [PATCH 0/6] formal/spinhint: Update code snippet
Date: Sat, 2 Feb 2019 09:34:37 -0800 [thread overview]
Message-ID: <20190202173437.GO4240@linux.ibm.com> (raw)
In-Reply-To: <db974b96-dd4f-dce2-44a5-1b33f5ed495e@gmail.com>
On Sun, Feb 03, 2019 at 12:05:32AM +0900, Akira Yokosawa wrote:
> Hi Paul,
>
> Here is another round of code snippet update, with modernization
> of outputs of Spin and tables of state search results.
>
> Patch #1 updates fcvextract.pl so that .spin files are handled
> as the same as C source files.
>
> Patch #2 applies the new scheme to code snippets. It also contains
> minor changes for better typesetting.
>
> Patch #3 replaces captures of Spin outputs with those obtained
> from Spin version 6.4.8. This commit adds outputs as .lst files
> under CodeSamples/formal/promela/. They are added to the dependency
> in the top level Makefile.
>
> Patch #4 updates tables of Spin result. For qrcu.spin, I used
> the compiler flag -DCOLLAPSE to complete the state search for
> updaters=3 readers=2 on a machine with 16GB memory. As far as
> I understand correctly, this compiler flag does not affect the
> completeness of state search. So I added some explanation in the text
> to mention the flag and the argument -mN of ./pan to increase the
> limit of search depth.
>
> Patch #5 tweaks footnote on a cell in a table.
>
> Patch #6 is a nitpick patch to consistently use \co{}.
>
> I'm wondering if Patch #4 is OK from your perspective.
> Any feedback is welcome!
Very good, applied and pushed! I added a small patch on top of Patch #4
updating the extrapolation. It was about a terabyte, and is now about
half that. I agree that -DCOLLAPSE is a pure optimization, so it should
be OK. If we trust the documentation, anyway! ;-)
Thanx, Paul
> Thanks, Akira
> --
> Akira Yokosawa (6):
> fcvextract.pl: Treat '.spin' files as C sources
> formal/spinhint: Employ new scheme for code snippet
> formal/spinhint: Update output lists of spin
> formal/spinhint: Update tables of memory usage of Spin
> formal/spinhint: Put footnote on header in table
> formal/spinhint: Use \co{...} rather than {\tt ...}
>
> CodeSamples/formal/promela/atomicincrement.spin | 2 +
> .../formal/promela/atomicincrement.spin.lst | 28 +
> CodeSamples/formal/promela/increment.spin | 46 +-
> CodeSamples/formal/promela/increment.spin.lst | 28 +
> .../formal/promela/increment.spin.trail.lst | 42 +
> CodeSamples/formal/promela/lock.h | 16 +-
> CodeSamples/formal/promela/lock.spin | 46 +-
> CodeSamples/formal/promela/lock.spin.lst | 29 +
> CodeSamples/formal/promela/qrcu.spin | 95 ++-
> Makefile | 4 +-
> formal/spinhint.tex | 874 ++++++---------------
> perfbook.tex | 1 +
> utilities/fcvextract.pl | 8 +-
> 13 files changed, 502 insertions(+), 717 deletions(-)
> create mode 100644 CodeSamples/formal/promela/atomicincrement.spin.lst
> create mode 100644 CodeSamples/formal/promela/increment.spin.lst
> create mode 100644 CodeSamples/formal/promela/increment.spin.trail.lst
> create mode 100644 CodeSamples/formal/promela/lock.spin.lst
>
> --
> 2.7.4
>
next prev parent reply other threads:[~2019-02-02 17:41 UTC|newest]
Thread overview: 16+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-02-02 15:05 [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
2019-02-02 15:08 ` [PATCH 1/6] fcvextract.pl: Treat '.spin' files as C sources Akira Yokosawa
2019-02-02 15:09 ` [PATCH 2/6] formal/spinhint: Employ new scheme for code snippet Akira Yokosawa
2019-02-02 15:11 ` [PATCH 3/6] formal/spinhint: Update output lists of spin Akira Yokosawa
2019-02-02 15:13 ` [PATCH 4/6] formal/spinhint: Update tables of memory usage of Spin Akira Yokosawa
2019-02-02 15:14 ` [PATCH 5/6] formal/spinhint: Put footnote on header in table Akira Yokosawa
2019-02-02 15:15 ` [PATCH 6/6] formal/spinhint: Use \co{...} rather than {\tt ...} Akira Yokosawa
2019-02-02 17:34 ` Paul E. McKenney [this message]
2019-02-06 22:42 ` [PATCH 0/6] formal/spinhint: Update code snippet Akira Yokosawa
2019-02-07 9:17 ` Paul E. McKenney
2019-02-11 15:08 ` [PATCH 0/3] formal/spinhint: Add result and discussion of 3 readers 3 updaters QRCU Spin run Akira Yokosawa
2019-02-11 15:11 ` [PATCH 1/3] formal/spinhint: Add result " Akira Yokosawa
2019-02-11 15:28 ` Akira Yokosawa
2019-02-11 19:34 ` Paul E. McKenney
2019-02-11 15:12 ` [PATCH 2/3] formal/spinhint: Add column of search depth in Table 12.2 Akira Yokosawa
2019-02-11 15:13 ` [PATCH 3/3] formal/spinhint: Place footnote inside floating table Akira Yokosawa
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=20190202173437.GO4240@linux.ibm.com \
--to=paulmck@linux.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