New Memory Consistency Model Committee

[Daniel Lustig]

Hi all,

 

The RISC-V Technical Committee has formed a new committee tasked with formally defining the memory consistency model for the RISC-V architecture.  I, Dan Lustig (NVIDIA), will be the chair of this committee, and Arvind (MIT) will be the vice-chair.

 

Our tentative charter is as follows:

 - The primary goal is to develop a rigorous and sound memory consistency model to incorporate into the RISC-V ISA specification, and to provide explanatory material as necessary.

 - The RISC-V memory model should follow the best modern practices of the field, from academia and from industry.

 - Ideally, the RISC-V memory model will remain compatible with existing RISC-V implementations, specifications, compiler mappings, and software toolchains.  However, backwards compatibility is not an absolute requirement, and the benefits of backwards compatibility may in some places be outweighed by the need for a sound memory model.

 - The memory model should be compatible with and impose minimal design and/or performance burden onto RISC-V implementations.  This includes small stand-alone RISC-V cores, large complex RISC-V cores, RISC-V cores deeply-embedded as controllers into an SoC, or otherwise.

 

Items on the agenda currently include, in rough priority order:

 - Ensure everybody understands and agrees with the goals laid out in the charter

 - Decide whether global store (multi-copy) atomicity is beneficial/acceptable/unacceptable.  This fundamentally affects the design of the rest of the model, and hence will be the top technical priority to start

 - Options for forbidding out-of-thin-air executions, and in particular: should load-store reordering be forbidden?

 - The legality of same-address load-load reordering, whether memory ordering needs to respect (address/data/control) dependencies, and other details of a similar vein

 - Longer-term: ensure compatibility with the virtual memory subsystem (e.g., FENCE.I), and take other potential risk factors (e.g., mixing accesses of different sizes) into consideration

 

We hope to arrive at a consensus as soon as possible.  The process is not meant to become an extended research endeavor.  If all goes well, we would even like to have a tentative working proposal as soon as the next RISC-V workshop in May.

 

Logistically: we expect to have regular weekly phone and/or video meetings, to be scheduled after we get a sense for the interested participants.  We also expect to have regular ongoing discussion by email between meetings.  All interested RISC-V members are welcome to participate.

 

If you are interested in participating actively, please reach out to me and Arvind, and please join the newly-formed RISC-V memory model working group inside the technical committee workspace.  We will work out the scheduling and logistics for the weekly meetings once we get a sense for who is interested.  Feel free to also reach out to us or reply to this message if you have any questions.

 

Thanks,

Dan Lustig

[Jonas Oberhauser]

Hi all,

I understand I'm late but I have only now been made aware of this project. If it's still possible at all I'd like to get involved.

I'm currently working at the Computer Architecture and Parallel Systems group of Wolfgang J Paul (the former Verisoft project). I did some research on formalizing operational semantics for a realistic ISAs with a weak memory model, and by realistic I mean: has operating system support (address virtualization, user/OS modes, interrupts, IPIs), IO devices, mixed accesses of different sizes and no alignment restrictions, instruction buffers, store buffers. Note that such an ISA no longer is TSO because MMUs can trigger memory events that bypass the store buffer and thus break W->W ordering and W->R forwarding.

I have also proved a non-trivial DRF-theorem (based on the Cohen-Schirmer theorem) for such an ISA, and by non-trivial I mean: shared data can be accessed without locks, and fences are only required between a store to shared data and a later read from shared data on the same hart, and in some edge cases involving mixed-size or misaligned accesses (you correctly identified these as "potential risk factors"... Note that mixed-size accesses can arise in a machine that only allows same-size aligned load/store/RMW because of instruction fetch, in case one processor "step" reads both from the instruction address and an effective address).

I am also working on hardware construction and correctness proofs (i.e., simulation proofs between hardware computations and ISA computations) for hardware implementing such an ISA.

I'm very interested in having an ISA with an extremely weak but still useful and simple memory model, especially ones for which individual implementations can offer additional guarantees and/or hardware support for DRF-like theorems (such as explicit shared instructions (instructions that will access shared state), which if used correctly will bring you back to SC or Rel/Acq by, e.g., enforcing enough order between shared instructions). 

We hope to arrive at a consensus as soon as possible.  The process is not meant to become an extended research endeavor.  If all goes well, we would even like to have a tentative working proposal as soon as the next RISC-V workshop in May.

If God forbid it didn't all go well ; ) and I can still get involved, please let me know,

Jonas