On Tue, Feb 12, 2019 at 12:28:12AM +0900, Akira Yokosawa wrote: > 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? Done! I queued and pushed all three, and also pushed out some minor wordsmithing. Please let me know if I messed anything up. And nice approach showing the strengths and weaknesses of the two approaches, good stuff, thank you! Thanx, Paul > 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 > > > [...] >
