Exploring the Interplay of Software, Hardware, and ISA in Memory Model Design

The ISA is a multi-part specification of hardware behavior as seen by software. One significant, yet often under-appreciated, aspect of this specification is the memory consistency model (MCM) which governs inter-module interactions in a shared memory system. MCM design choices are complicated and involve reasoning about the subtle interplay between many diverse features. Simply defining an ISA specification in light of the evaluation of a single microarchitecture is not sufficient, as future designs may expose inefficiencies or inaccuracies within the specification.
I will make a case for MCM-aware ISA design, and present a toolflow we have developed. In particular, we have developed a methodology for evaluating and refining an ISA's MCM to ensure a correct and complete specification. I will also discuss how we apply our framework to the open source RISC-V ISA, focusing on the goal of accurate, efficient, and legal compilations from C/C++. I will present under-specifications and potential inefficiencies we have uncovered in the current RISC-V ISA documentation and identify possible solutions for each. As an example, we find that a RISC-V-compliant microachitecture allows 144 outcomes forbidden by C/C++ to be observed out of 1,701 litmus tests examined. I will show that using our framework, ISA designers can iteratively refine and evaluate ISA specifications in a microarchitecture-aware manner based on the ISA's ability to serve as a target for compiled C/C++ programs.