> On April 13, 2016, 5:49 p.m., Andreas Hansson wrote: > > Really nice to see more work along these lines. > > > > I am keen to make sure we "finish what we started", and for that reason I > > would like to understand how this relates to the existing MemChecker. Also, > > I'd really like to see the MemChecker more widely deployed (which I think > > requires some further cleverness). Could you shed some light on this Marco? > > Marco Elver wrote: > Sorry, there appears to have been a email-response race condition. I > replied to your other email; the response is (carry the discussion forward > here): > > McVerSi is very different from MemChecker: > > 1) Unlike MemChecker, which is only monitoring the memory system, my > goal was to verify executions of the full memory consistency model, > which can only be achieved by actually executing real instructions of > the target ISA (in this case, the tests even run inside a full system, > with virtual addressing, etc.). > > 2) Unlike MemChecker, McVerSi does not monitor; MemChecker is in fact > what can be referred to as a relaxed scoreboard or operational model (in > limited form). The checker that I use is axiomatic, and only works over > fixed size traces -- this works very well for the test sizes that I want > to generate, and also allows encoding many memory consistency models > succinctly. > > 3) McVerSi aims to generate better tests over time: it a) optimizes > tests for the domain (memory consistency verification) and b) uses > coverage to guide the test search in unexplored directions (since > coverage is highly specific, the patch I provide includes a template > that should be filled in with the user's coverage computation). > > I hope that makes the picture a bit clearer. In the paper we discuss > more related work, and the approach of MemChecker falls somewhere under > the "Memory system verification" section. > > Marco Elver wrote: > I want to clarify point 1) yes, we also run real instructions and monitor > with MemChecker the commands that are generated and sent to the memory > system. However, the actual memory consistency model can only be verified if > we look at the results of each instruction. This implies that with the > approach I take with McVerSi, I am verifying the full system, including the > core pipeline. In fact, the new bugs I found are due to the interaction of > coherence protocol and pipeline (usually missed forwarded invalidations). > > Additionally, with the latest version, I can also generate tests that > actually test aspects of the Virtual Address Memory Consistency (VAMC), by > generating synonyms.
Don't get me wrong, this is all great. All I am saying is: Can we put some energy into fixing the outstanding issues in the MemChecker, and add a regression or two? That would be of tremendous value. Once we are passed that we can make the world an even better place with this new framework. Sounds ok? - Andreas ----------------------------------------------------------- This is an automatically generated e-mail. To reply, visit: http://reviews.gem5.org/r/3449/#review8206 ----------------------------------------------------------- On April 13, 2016, 7:53 p.m., Marco Elver wrote: > > ----------------------------------------------------------- > This is an automatically generated e-mail. To reply, visit: > http://reviews.gem5.org/r/3449/ > ----------------------------------------------------------- > > (Updated April 13, 2016, 7:53 p.m.) > > > Review request for Default. > > > Repository: gem5 > > > Description > ------- > > Add support for McVerSi memory consistency verification framework > > This patch implements the Gem5-specific portion of McVerSi (a framework for > simulation-based memory consistency verification) [1]. > > Currently, only the O3CPU is supported. > > [1] http://ac.marcoelver.com/research/mcversi > > > Diffs > ----- > > src/arch/arm/isa/formats/aarch64.isa df24b9af42c7 > src/arch/arm/isa/formats/m5ops.isa df24b9af42c7 > src/arch/arm/isa/insts/m5ops.isa df24b9af42c7 > src/cpu/o3/commit_impl.hh df24b9af42c7 > src/cpu/o3/dyn_inst.hh df24b9af42c7 > src/cpu/o3/dyn_inst_impl.hh df24b9af42c7 > src/cpu/o3/lsq_unit_impl.hh df24b9af42c7 > src/sim/SConscript df24b9af42c7 > src/sim/mcversi.hh PRE-CREATION > src/sim/mcversi.cc PRE-CREATION > src/sim/pseudo_inst.hh df24b9af42c7 > src/sim/pseudo_inst.cc df24b9af42c7 > util/m5/m5op.h df24b9af42c7 > util/m5/m5op_x86.S df24b9af42c7 > util/m5/m5ops.h df24b9af42c7 > > Diff: http://reviews.gem5.org/r/3449/diff/ > > > Testing > ------- > > Unless explicitly enabled (via loading appropriate workload), this is > component is unused. > > However, bugs have been found elsewhere in Gem5 by McVerSi (which is its > purpose!). (I will not restate them here to keep the discussion on topic.) > > > Thanks, > > Marco Elver > > _______________________________________________ gem5-dev mailing list gem5-dev@gem5.org http://m5sim.org/mailman/listinfo/gem5-dev
