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@xxxxxxxxx>
> 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@xxxxxxxxx>
> ---
> .../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
>
[...]
