The RISC-V Memory Consistency Model

Krste Asanović, Chairman, RISC-V Foundation

Memory consistency models (MCMs) are known to flummox even experienced computer architects, so it is perhaps not surprising that recent news articles had some difficulty portraying the nuances behind recent findings by a team of Princeton researchers led by Professor Margaret Martonosi.  The RISC-V Foundation is publishing this article to help the RISC-V community understand the deeper implications of the Princeton study.

Executive Summary

1. The Princeton team found holes in the original RISC-V MCM specification that might lead designers of future complex RISC-V processors to implement behavior that would violate memory-ordering rules required for the C11 programming language standard.
2. Current simpler RISC-V cores, such as the Rocket core, are not affected.
3. The RISC-V Instruction Set Architecture (ISA) specification does not have “over a 100 errors”, rather some possible implementations of the ISA could fail over a 100 litmus tests, but a single change to the RISC-V ISA specification could eliminate all these errors.
4. The RISC-V Foundation has been working with the Princeton team since December 2015, as well as with other MCM experts, to help tighten up the RISC-V ISA specification to avoid these problems. This work is part of converting the original Berkeley-authored RISC-V specifications into ratified RISC-V Foundation ISA standards, and is expected to complete in 2017.
5. It is intended that the MCM changes would be backwards compatible, such that existing simpler cores would run code written to the new specs correctly.

Memory Consistency Model Background

The Princeton team have been developing tools to help analyze MCMs, and last year began applying them to the original RISC-V ISA specifications produced by UC Berkeley.  An ISA specification describes the contract between hardware and software, so that software written to the specification should run correctly on any processor claiming to obey the specification.  MCMs are a portion of the ISA specification that describe how values produced by one core are made visible to other cores in the system when running multithreaded programs. Programming languages also have MCMs that describe how different threads in a program can communicate through shared-memory variables, and the Princeton project focused on the C11 version of the popular C programming language.  The Princeton tools allow the specification of a complete system including language-level ordering rules, the mapping of language-level constructs to the ISA, and a model of re-orderings possible in a micro-architectural implementation of an ISA.  Given a suite of litmus tests, the tools can analyze a system to see if illegal re-orderings are observable at the language level. Prof. Martonosi elaborates: “Our previous tools, such as PipeCheck, verified an underlying implementation against a specified ISA, whereas TriCheck also looks upwards to assess an ISA’s alignment with language-level memory models. We use axiomatic specifications of the ISA and the hardware implementation, and compiler mappings that translate from language-level code to an ISA implementation of each litmus test. This creates a suite of test instances to be run on a tool similar to PipeCheck.” The Princeton team used their tools to specify language-level axioms for C11, a set of compiler mappings to the RISC-V ISA and also to build a model of the popular Rocket RISC-V core.  The model of the unmodified base Rocket core did not exhibit any illegal behavior because it does not reorder memory accesses aggressively. The problematic behavior occurs after adding additional re-orderings that would be legal under the RISC-V specification as currently written. Though the Princeton paper reported a large number of failing litmus tests when additional re-orderings were added, it is important to note that a failed litmus test does not correspond one-to-one with errors in the MCM as a single change in the MCM could remove all litmus test failures. The Princeton team, via emails on RISC-V public developer lists, communicated their initial MCM concerns in December 2015. As their tools progressed to demonstrate with greater detail that the existing RISC-V MCM specification was too weak to support the C11 MCM, the Princeton team again approached the RISC-V community last September, and presented their findings at the 5th RISC-V workshop at Google in November (a later version of the Princeton work appeared in a paper at the ASPLOS conference in April 2017).  After more discussions, the Foundation formed a memory model task group in early 2017 with the goal of defining the memory model as part of the process of formally ratifying the UC Berkeley-produced RISC-V ISA specifications as the official Foundation RISC-V ISA standard. Task Groups within the RISC-V Foundation are in the process of cleaning up the original RISC-V ISA specifications proposed by UC Berkeley and ratifying them as official RISC-V Foundation standards.  The Memory Model Task Group’s work is part of this effort and will propose a new RISC-V memory model that will be ratified as part of the RISC-V  Foundation ISA standard in 2017. In their paper, the Princeton team also reports on the results of using their tools on the MCMs of some proprietary ISAs and has shown these proprietary ISAs have open unresolved bugs in shipping products.  We note that no proprietary ISA vendor has published a formal memory model that they guarantee their products will obey. Daniel Lustig, a co-author on the paper, who is now at NVIDIA and is chairing the RISC-V Foundation Memory Model Task Group, adds “RISC-V’s open-source approach allows the best experts from academia and industry to collaborate on the instruction set architecture. For example, researchers from NVIDIA, Princeton University, and MIT are together defining the memory model, one of the most complex parts of the ISA. The model is being finalized and will be proven correct using formal verification tools such as TriCheck, a specialized tool flow developed at Princeton.” The RISC-V Foundation was formed with an open and inclusive governance model to allow for contributions from experts across academia and industry.  This work by Princeton is a shining example of the power and benefit of an open, non-proprietary ISA.  Together, we are developing an extensible RISC-V ISA available for all to use across all forms of computing devices. If you have an interest in contributing to the RISC-V Foundation, please contact us at info@riscv.org.[/vc_column_text][/vc_column][/vc_row]]]>