Hi Paul,
This patch set adds the result and discussion you suggested in this
thread.
Instead of replacing the existing table of memory usage (with the
flag "-DCOLLAPSE"), I added another table comparing the memory usage
and runtime obtained with "-DCOLLAPSE" and "-DMA=N".
Patch #1 adds the result as a summary table and give some discussion
of the usage of the compiler flag "-DMA=N". It also adds a quick
quiz comparing the result of "-DCOLLAPSE" and "-DMA=N" with 2 readers
and 3 updaters.
Patch #2 adds a column of search depth in the existing Table 12.2 of
memory usage with "-DCOLLAPSE". This helps the extrapolation of
necessary search depth for 3 readers and 3 updaters.
Patch #3 is a minor tweak of a footnote in Table 12.2.
It should be possible to reconstruct the story to reference only the
added summary table, but I took another way to minimize the change
of story. The point is that as long as you have sufficient memory,
there is no need to use "-DMA=N". The search speed can be slower
than that with the flag "-DCOLLAPSE" by nearly one order of magnitude.
Any feedback/update is more than welcome!
Thanks, Akira
--
Akira Yokosawa (3):
formal/spinhint: Add result of 3 readers 3 updaters QRCU Spin run
formal/spinhint: Add column of search depth in Table 12.2
formal/spinhint: Place footnote inside floating table
.../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 | 185 ++++++++++++++++++---
perfbook.tex | 2 +-
7 files changed, 254 insertions(+), 24 deletions(-)
create mode 100644 CodeSamples/formal/promela/qrcu.spin.33ma.lst
create mode 100644 CodeSamples/formal/promela/qrcu.spin.col-ma.diff.lst
--
2.7.4
