On Thu, Feb 07, 2019 at 07:42:26AM +0900, Akira Yokosawa wrote:
> On 2019/02/02 09:34:37 -0800, Paul E. McKenney wrote:
> > 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.
>
> Half a terabyte is not prohibitively large these days, and Spin has
> another compaction option "-DMA=N" which aggressively reduces memory
> consumption in exchange of search speed.
>
> It took three days to complete, with the total memory usage of 6.5GB.
> The output looks as follows:
>
> --------
> (Spin Version 6.4.6 -- 2 December 2016)
> + Partial Order Reduction
> + Graph Encoding (-DMA=96)
>
> Full statespace search for:
> never claim - (none specified)
> assertion violations +
> cycle checks - (disabled by -DSAFETY)
> invalid end states +
>
> State-vector 96 byte, depth reached 2055621, errors: 0
> MA stats: -DMA=84 is sufficient
> Minimized Automaton: 56420520 nodes and 1.75128e+08 edges
> 9.6647071e+09 states, stored
> 9.7503813e+09 states, matched
> 1.9415088e+10 transitions (= stored+matched)
> 7.2047951e+09 atomic steps
>
> Stats on memory usage (in Megabytes):
> 1142905.887 equivalent memory usage for states (stored*(State-vector + overhead))
> 5448.879 actual memory usage for states (compression: 0.48%)
> 1068.115 memory used for DFS stack (-m20000000)
> 1.619 memory lost to fragmentation
> 6515.375 total actual memory usage
>
>
> unreached in proctype qrcu_reader
> (0 of 18 states)
> unreached in proctype qrcu_updater
> qrcu.spin:102, state 82, "-end-"
> (1 of 82 states)
> unreached in init
> (0 of 23 states)
>
> pan: elapsed time 2.72e+05 seconds
> pan: rate 35500.523 states/second
> --------
>
> I'm not sure if this result is worthy enough to be mentioned
> in the text.
But of course!
As long as the entire table is generated with the same arguments and
configuration, and those arguments and configuration are called out
somewhere (perhaps in a script somewhere in CodeSamples), please do
send me a patch!
Perhaps even better would be to call out those configurations and
arguments earlier on in the section giving advice on how to use
Promela and spin.
Thanx, Paul
> Thoughts?
>
> Thanks, Akira
>
> > 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
> >>
> >
>
