From: Akira Yokosawa <akiyks@gmail.com>
To: "Paul E. McKenney" <paulmck@linux.ibm.com>
Cc: perfbook@vger.kernel.org, Akira Yokosawa <akiyks@gmail.com>
Subject: Re: [PATCH 1/3] formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
Date: Tue, 12 Feb 2019 00:28:12 +0900 [thread overview]
Message-ID: <c5ee9c83-e89a-c3d2-e293-21396acb7db8@gmail.com> (raw)
In-Reply-To: <a83e948f-d241-be30-733b-87975452fd1a@gmail.com>
Paul,
There was a typo in the commit log.
On 2019/02/12 00:11:23 +0900, Akira Yokosawa wrote:
> From fe701731c7296b90deae52747f5f3be556511289 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Sun, 10 Feb 2019 00:02:26 +0900
> Subject: [PATCH 1/3] formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
>
> By using the compiler flag "-DMA=N", run of qrcu.spin with 3 readers
> and 3 updaters can be completed with the memory usage of 6.5GHz.
^^^^
6.5GB.
Can you amend it for me?
Thanks, Akira
>
> This commit adds the result and the command used to run the
> verification. A Quick Quiz is added to present an indirect
> evidence of search completeness.
>
> As the compiler flag "-DCOLLAPSE" generates much faster code,
> memory usage table with "-DCOLLAPSE" is kept. The complete
> table for the runs with the flag "-DMA=N" is added as another
> table.
>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> .../formal/promela/atomicincrement.spin.lst | 2 +-
> CodeSamples/formal/promela/increment.spin.lst | 2 +-
> CodeSamples/formal/promela/lock.spin.lst | 2 +-
> CodeSamples/formal/promela/qrcu.spin.33ma.lst | 37 +++++
> .../formal/promela/qrcu.spin.col-ma.diff.lst | 48 +++++++
> formal/spinhint.tex | 150 ++++++++++++++++++++-
> 6 files changed, 234 insertions(+), 7 deletions(-)
> create mode 100644 CodeSamples/formal/promela/qrcu.spin.33ma.lst
> create mode 100644 CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst
>
[...]
next prev parent reply other threads:[~2019-02-11 15:28 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 ` [PATCH 0/6] formal/spinhint: Update code snippet Paul E. McKenney
2019-02-06 22:42 ` 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 [this message]
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=c5ee9c83-e89a-c3d2-e293-21396acb7db8@gmail.com \
--to=akiyks@gmail.com \
--cc=paulmck@linux.ibm.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