Add support for McVerSi memory consistency verification framework

Information
Submitter:	Marco Elver
Repository:	gem5
Branch:	default
Bugs:
Depends On:	3448
Reviewers
Groups:	Default
People:

Description

This patch implements the Gem5-specific portion of McVerSi (a framework for simulation-based memory consistency verification) [1].

Architectures supported are:
- ARM (current mc2lib code generation only supports ARMv7).
- X86 (pseudo ops available via mmapped IPR interface).

Currently, only the O3CPU is supported.

[1] http://ac.marcoelver.com/research/mcversi

Testing Done

Unless explicitly enabled (via loading appropriate workload), this component is unused.

Tested with ARM+Classic and X86+Ruby. Precompiled workloads that were used for testing available here: http://ac.marcoelver.com/res/mcversi_guest_workload_gem5.tar.gz

However, bugs have been found elsewhere in Gem5 while testing McVerSi (see http://www.mail-archive.com/gem5-dev@gem5.org/msg18940.html , and 1 of 2 bugs from paper http://reviews.gem5.org/r/2842/ ). (I will not restate them here to keep the discussion on topic.)

Issue Summary

Description	From	Last Updated	Status
remove trailing whitespace	Brad Beckmann	May 5, 2016, 5:52 a.m.	Resolved
align with the beginning '('	Brad Beckmann	May 5, 2016, 5:52 a.m.	Resolved
align with the beginning '('	Brad Beckmann	May 5, 2016, 5:52 a.m.	Resolved
Please add comments to explain what these do.	Andreas Hansson	May 18, 2016, 2:41 a.m.	Resolved
Same here	Andreas Hansson	May 18, 2016, 2:41 a.m.	Resolved
As above, it would be good if these could be grouped with a comment around what they do and highighting ...	Andreas Hansson	May 18, 2016, 2:41 a.m.	Resolved
Should this perhaps be a probe point?	Andreas Hansson	May 19, 2016, 12:10 p.m.	Resolved
Comments please	Andreas Hansson	May 18, 2016, 3:54 a.m.	Resolved
Why this->?	Andreas Hansson	May 18, 2016, 2:44 a.m.	Resolved
This is intruiging. Every write operation is turned into a SWAP? This seems like it could potentially have a whole ...	Andreas Hansson	May 18, 2016, 2:56 a.m.	Resolved
again, should this be a probe point?	Andreas Hansson	May 19, 2016, 12:10 p.m.	Resolved
I don't think we do this anywhere else in the codebase. Just the author and title should be enough imho.	Andreas Hansson	May 18, 2016, 3:18 a.m.	Resolved
odd indentation, and no comments	Andreas Hansson	May 19, 2016, 11:15 a.m.	Resolved
void*? Please use C++11 STL data structures	Andreas Hansson	May 19, 2016, 12:09 p.m.	Resolved
naming convention	Andreas Hansson	May 18, 2016, 3:21 a.m.	Resolved
really? that seems dodgy	Andreas Hansson	May 18, 2016, 3:21 a.m.	Resolved
Could we make these part of a class instead of making them global?	Andreas Hansson	May 19, 2016, 10:20 a.m.	Resolved
Surely this should not be hardcoded here. Why not use the cache-line size from the System?	Andreas Hansson	May 19, 2016, 10:20 a.m.	Resolved
seems the isValid operations should be const	Andreas Hansson	May 18, 2016, 3:38 a.m.	Resolved
Is there any chance we could use the random_mt used throughout the rest of gem5 rather? We have had a ...	Andreas Hansson	May 18, 2016, 4:04 a.m.	Resolved
Should these not just be removed rather?	Andreas Hansson	May 18, 2016, 4 a.m.	Resolved
void*? Why not use vectors?	Andreas Hansson	May 19, 2016, 11:19 a.m.	Resolved
Please double check that this works with gcc 4.8 and clang 3.1	Andreas Hansson	May 7, 2016, 7:34 a.m.	Open
style	Andreas Hansson	May 18, 2016, 3:39 a.m.	Resolved

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 April 13, 2016, 11:03 a.m. (April 13, 2016, 11:03 a.m.)

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 April 13, 2016, 11:14 a.m. (April 13, 2016, 11:14 a.m.)

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 April 13, 2016, 2:28 p.m. (April 13, 2016, 2:28 p.m.)

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 April 13, 2016, 3:41 p.m. (April 13, 2016, 3:41 p.m.)

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 April 14, 2016, 1:43 a.m. (April 14, 2016, 1:43 a.m.)

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 April 14, 2016, 10 a.m. (April 14, 2016, 10 a.m.)

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.

Andreas Hansson April 14, 2016, 10:03 a.m. (April 14, 2016, 10:03 a.m.)

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 Hansson April 25, 2016, 12:52 a.m. (April 25, 2016, 12:52 a.m.)

As my weekend project I've added a very simple regression for the MemChecker: http://repo.gem5.org/gem5/rev/91834ba4b16d

We may want to extend this further, and possibly also add a Ruby version.

Thank you Marco for posting the patch. Unfortunately most of your patch does not display correctly. Did you post it from a Mecrurail repo using the "hg postreview -o" command? I know your patch applies to an earlier version of the repo, but I believe it should still display correclty if you use the '-o' option.

Thanks.

Change Summary:

Set correct base. (Apologies, missed the -o flag.)

Diff:

Revision 2 (+1234 -1)

Show changes

	src/arch/arm/isa/formats/aarch64.isa
	src/arch/arm/isa/formats/m5ops.isa
	src/arch/arm/isa/insts/m5ops.isa
	src/cpu/o3/commit_impl.hh
	src/cpu/o3/dyn_inst.hh
	src/cpu/o3/dyn_inst_impl.hh
	src/cpu/o3/lsq_unit_impl.hh
	src/sim/SConscript
	7 more

Overall this patch looks great to me. Sorry it took me so long to review it. Could you update the patch description to indicate that only ARM is currently supported. I believe that is true, correct? Other than that, just a few minor style changes below.

src/cpu/o3/commit_impl.hh (Diff revision 2)

remove trailing whitespace

Show all issues

src/sim/pseudo_inst.hh (Diff revision 2)

align with the beginning '('

Show all issues

src/sim/pseudo_inst.hh (Diff revision 2)

align with the beginning '('

Show all issues

Change Summary:

Many thanks for the review.

This change
- addresses the style issues.
- and clarifies supported architectures.

When I started this, X86 was the first supported architecture (together with Ruby, as this was used in the paper). However, I think there are limits to adding new pseudo ops via arch/x86/isa, and it seemed cleaner to just rely on the mmapped IPR interface (ARM does not seem to support this, so had to add this in arch/arm/isa).

Note that, to support Ruby, the patch http://reviews.gem5.org/r/3398/ is required (is marked as a dependency).

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].

	+	Architectures supported are:
	+	- ARM (current mc2lib code generation only supports ARMv7).
	+	- X86 (pseudo ops available via mmapped IPR interface).
	+
		Currently, only the O3CPU is supported.

		[1] http://ac.marcoelver.com/research/mcversi

Testing Done:

~		Unless explicitly enabled (via loading appropriate workload), this is component is unused.
	~	Unless explicitly enabled (via loading appropriate workload), this 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.)
	~	Tested with ARM+Classic and X86+Ruby. Precompiled workloads that were used for testing available here: http://ac.marcoelver.com/res/mcversi_guest_workload_gem5.tar.gz
	+
	+	However, bugs have been found elsewhere in Gem5 while testing McVerSi (see http://www.mail-archive.com/gem5-dev@gem5.org/msg18940.html , and 1 of 2 bugs from paper http://reviews.gem5.org/r/2842/ ). (I will not restate them here to keep the discussion on topic.)

Diff:

Revision 3 (+1234 -1)

Show changes

	src/arch/arm/isa/formats/aarch64.isa
	src/arch/arm/isa/formats/m5ops.isa
	src/arch/arm/isa/insts/m5ops.isa
	src/cpu/o3/commit_impl.hh
	src/cpu/o3/dyn_inst.hh
	src/cpu/o3/dyn_inst_impl.hh
	src/cpu/o3/lsq_unit_impl.hh
	src/sim/SConscript
	7 more

Looks good to me.  Please check this one in with http://reviews.m5sim.org/r/3398/.  Thanks!

Marco Elver May 6, 2016, 9:15 a.m. (May 6, 2016, 9:15 a.m.)

Thank you! Just to let you know, I do not have commit access, so someone else would have to check these in.

Brad Beckmann May 6, 2016, 9:28 a.m. (May 6, 2016, 9:28 a.m.)

Have you ran the regression tester with these patches applied?

Marco Elver May 6, 2016, 4:14 p.m. (May 6, 2016, 4:14 p.m.)

Quick regressions (SE mode) with ALPHA, ARM, X86 look fine to me.

Marco Elver May 7, 2016, 12:05 p.m. (May 7, 2016, 12:05 p.m.)

Thank you for your comments! As I want to avoid making changes hastily, I expect to be able to start addressing these in about 1-2 weeks time earliest.

src/arch/arm/isa/formats/aarch64.isa (Diff revision 3)

Please add comments to explain what these do.

Show all issues

src/arch/arm/isa/formats/m5ops.isa (Diff revision 3)

Same here

Show all issues

src/arch/arm/isa/insts/m5ops.isa (Diff revision 3)

As above, it would be good if these could be grouped with a comment around what they do and highighting that these all belong to McVersi functionality

Show all issues

src/cpu/o3/commit_impl.hh (Diff revision 3)

Should this perhaps be a probe point?

Show all issues

Marco Elver May 20, 2016, 4:45 a.m. (May 20, 2016, 4:45 a.m.)

This is a bigger, and IMHO unnecessary change. Since it would turn into a SimObject, it would need to be instantiated in some Python config.

I see the provided interface an extension of the PseudoInst interface, just that it didn't seem clean to embed the functionality in pseudo_inst.cc.

The reason is that it makes usage simpler, as all that is needed is to invoke the pseudo insts. by some guest-workload (the guest workload decides the configuration, e.g. setting memory size, iterations, etc.).

src/cpu/o3/dyn_inst.hh (Diff revision 3)

Comments please

Show all issues

src/cpu/o3/dyn_inst_impl.hh (Diff revision 3)

Why this->?

Show all issues

Marco Elver May 20, 2016, 4:45 a.m. (May 20, 2016, 4:45 a.m.)

Same as in rest of file: accessing member of base class of template class.

src/cpu/o3/dyn_inst_impl.hh (Diff revision 3)

This is intruiging. Every write operation is turned into a SWAP? This seems like it could potentially have a whole range of unintended side effects.

Show all issues

Marco Elver May 20, 2016, 4:45 a.m. (May 20, 2016, 4:45 a.m.)

As said in the comment above this line: "Prerequisite for using MEM_SWAP is, that it should not be treated any differently than a regular write, with the only difference being that the data being overwritten is returned with the response. AFAIK, this holds for classic and Ruby."

If you trace the usage of MEM_SWAP/isSwap throughout the codebase, it is used like a write, with the only difference being that the overwritten value is returned in the response packet.

I further verified this by running a normal benchmark with unconditionally turning every write into a MEM_SWAP and the results are identical.

src/cpu/o3/lsq_unit_impl.hh (Diff revision 3)

again, should this be a probe point?

Show all issues

src/sim/mcversi.hh (Diff revision 3)

I don't think we do this anywhere else in the codebase. Just the author and title should be enough imho.

Show all issues

src/sim/mcversi.hh (Diff revision 3)

odd indentation, and no comments

Show all issues

Marco Elver May 20, 2016, 4:45 a.m. (May 20, 2016, 4:45 a.m.)

It's aligned with the opening brace '(', using spaces. What is the problem here?

src/sim/mcversi.hh (Diff revision 3)

void*? Please use C++11 STL data structures

Show all issues

src/sim/mcversi.hh (Diff revision 3)

naming convention

Show all issues

src/sim/mcversi.cc (Diff revision 3)

really? that seems dodgy

Show all issues

src/sim/mcversi.cc (Diff revision 3)

Could we make these part of a class instead of making them global?

Show all issues

src/sim/mcversi.cc (Diff revision 3)

Surely this should not be hardcoded here. Why not use the cache-line size from the System?

Show all issues

src/sim/mcversi.cc (Diff revision 3)

seems the isValid operations should be const

Show all issues

src/sim/mcversi.cc (Diff revision 3)

Is there any chance we could use the random_mt used throughout the rest of gem5 rather? We have had a number of cleanups to remove sporadic use of other forms of random number generation, and it would be good to not introduce new ones

Show all issues

Marco Elver May 20, 2016, 4:45 a.m. (May 20, 2016, 4:45 a.m.)

This is intentional, as using a global RNG would mean that test generation is not predictable if the system changes. At least this way, I know that my initial population is always going to be the same, even if the system has changed (e.g. when fixing a bug).

src/sim/mcversi.cc (Diff revision 3)

Should these not just be removed rather?

Show all issues

Marco Elver May 20, 2016, 4:45 a.m. (May 20, 2016, 4:45 a.m.)

They have intentionally been left, so as to make it easier for whoever wants to use this. They are called in other parts of the code, and the call-sites cannot be changed: leaving them here ensures whoever adds coverage computation for their design updates coverage at the right points.

src/sim/mcversi.cc (Diff revision 3)

void*?

Why not use vectors?

Show all issues

src/sim/mcversi.cc (Diff revision 3)

Please double check that this works with gcc 4.8 and clang 3.1

Show all issues

Marco Elver May 20, 2016, 4:45 a.m. (May 20, 2016, 4:45 a.m.)

GCC 4.8 is fine. Clang 3.1 I can't get my hands on, but if it supports C++11 there shouldn't be any problems.

src/sim/pseudo_inst.cc (Diff revision 3)

style

Show all issues

Diff:

Revision 4 (+1324 -1)

Show changes

	src/arch/arm/isa/formats/aarch64.isa
	src/arch/arm/isa/formats/m5ops.isa
	src/arch/arm/isa/insts/m5ops.isa
	src/cpu/o3/commit_impl.hh
	src/cpu/o3/dyn_inst.hh
	src/cpu/o3/dyn_inst_impl.hh
	src/cpu/o3/lsq_unit_impl.hh
	src/sim/SConscript
	7 more

Change Summary:

Rebase against latest gem5 and against latest mc2lib.

Depends On:

-	~~3398 - ruby: Implement SwapReq support~~

Diff:

Revision 5 (+1324 -1)

Show changes

	src/arch/arm/isa/formats/aarch64.isa
	src/arch/arm/isa/formats/m5ops.isa
	src/arch/arm/isa/insts/m5ops.isa
	src/cpu/o3/commit_impl.hh
	src/cpu/o3/dyn_inst.hh
	src/cpu/o3/dyn_inst_impl.hh
	src/cpu/o3/lsq_unit_impl.hh
	src/sim/SConscript
	7 more

You have a pending review.

Review Board 2.0.15

Screenshots

Files

Issue Summary

Change Summary:

Diff:

Change Summary:

Description:

Testing Done:

Diff:

Diff:

Change Summary:

Depends On:

Diff: