> 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?
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 ----------------------------------------------------------- This is an automatically generated e-mail. To reply, visit: http://reviews.gem5.org/r/3449/#review8206 ----------------------------------------------------------- On April 13, 2016, 5:45 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, 5:45 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 48b1f224eddc > src/arch/arm/isa/formats/m5ops.isa 48b1f224eddc > src/arch/arm/isa/insts/m5ops.isa 48b1f224eddc > src/cpu/o3/commit_impl.hh 48b1f224eddc > src/cpu/o3/dyn_inst.hh 48b1f224eddc > src/cpu/o3/dyn_inst_impl.hh 48b1f224eddc > src/cpu/o3/lsq_unit_impl.hh 48b1f224eddc > src/sim/SConscript 48b1f224eddc > src/sim/mcversi.hh PRE-CREATION > src/sim/mcversi.cc PRE-CREATION > src/sim/pseudo_inst.hh 48b1f224eddc > src/sim/pseudo_inst.cc 48b1f224eddc > util/m5/m5op.h 48b1f224eddc > util/m5/m5op_x86.S 48b1f224eddc > util/m5/m5ops.h 48b1f224eddc > > 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 [email protected] http://m5sim.org/mailman/listinfo/gem5-dev
