Hi Andreas, Can you elaborate on the "rough edges" that need to be addressed in MemChecker, other than adding a regression that uses it? Forcing Marco to deal with our regression system seems a bit out of scope.
Steve On Thu, Apr 14, 2016 at 10:03 AM Andreas Hansson <[email protected]> wrote: > > > > 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. > > > > Andreas Hansson wrote: > > 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? > > > > Marco Elver wrote: > > There may be a misunderstanding: the MemChecker and this (McVerSi) > are not directly competing. Rather, they are complementary verification > tools, in the way that one (MemChecker) targets *checking* a focussed part > of the system (but might miss bugs that only manifest due to interaction of > some components), with the benefit of being able to monitor arbitrary > system excutions for a very long time; and the other (McVerSi) focusses on > *test generation* (at ISA level, for full system) and checks that these > test executions are correct by relying on a completely different style of > checker (that does not allow monitoring). You could even use MemChecker to > monitor the memory system side during execution of tests generated with > McVerSi (which might, e.g. help with debugging). > > > > Indeed, our emphasis with McVerSi is on test generation; the checker > is of course a neccessary dependency. Without good tests, regardless of > checker, little can be done to find the really hard to find bugs, > especially in simulation. > > > > I find this comparison also somewhat misleading (apples vs. > oranges): as MemChecker (the name) implies, is a checker; McVerSi tackles > test generation (at ISA level) together with an efficient integrated > checker for the full system. > > > > Andreas Hansson wrote: > > I am not disputing what you are saying in any way, and I fully > appreciate that these tools are not competing. I merely want to make sure > we finish one thing before immersing ourselves in the next one. > > > > I would like to see: 1) A broader use of the MemChecker (which does > introduce some challenges and cleverness is needed to enhance it), and 2) A > few regressions using the MemChecker. > > > > Once we are past that we can delve in to all the new bits. Ok? > > > > Brad Beckmann wrote: > > Andreas, I completely dissagree in the precedent you are trying to > set here. Essentially you are saying we do not allow Marco to make new > contributions unless he does what you want first? When MemChecker was > added, did Marco have to commit to integrating a broad use of the tool and > adding regression tests? If not, why are you forcing him to do that now? > If we want broad set of contributors, we cannot expect them to climb a > mountain before they can check in. > > I am not asking Marco to climb a mountain, just polish the rough edges. I > am worried that we end up with two half-baked solutions...and I don't think > that benefits anyone. > > > - 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 > [email protected] > http://m5sim.org/mailman/listinfo/gem5-dev > _______________________________________________ gem5-dev mailing list [email protected] http://m5sim.org/mailman/listinfo/gem5-dev
