Formal Axiomatic Specification in Herd

The tool herd takes a memory model and a litmus test as input and simulates the execution of the test on top of the memory model. Memory models are written in the domain specific language Cat. This section provides two Cat memory model of RVWMO. The first model, Figure 2, follows the global memory order, Chapter [ch:memorymodel], definition of RVWMO, as much as is possible for a Cat model. The second model, Figure 3, is an equivalent, more efficient, partial order based RVWMO model.

The simulator herd is part of the diy tool suite — see http://diy.inria.fr for software and documentation. The models and more are available online at http://diy.inria.fr/cats7/riscv/.

riscv-defs.cat, a herd definition of preserved program order (1/3)

riscv.cat, a herd version of the RVWMO memory model (2/3)

riscv.cat, an alternative herd presentation of the RVWMO memory model (3/3)