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
>
