"Risc V total order model" (*****************************************) (* The RISCV Instruction set manual v2.3 *) (*****************************************) (* Notice that herd has defined its own rf relation *) (* Define ppo *) include "riscv-defs.cat" (********************************) (* Generate global memory order *) (********************************) let gmo0 = (* precursor: ie build gmo as an total order that include gmo0 *) loc & (W\FW) * FW | # Final write after any write to the same location ppo | # ppo compatible rfe # extends rf external (* Walk over all linear extensions of gmo0 *) with gmo from linearisations(M\IW,gmo0) (* Add initial writes upfront -- convenient for computing rfGMO *) let gmo = gmo | loc & IW * (M\IW) (**********) (* Axioms *) (**********) (* Compute rf according to the load value axiom, aka rfGMO *) let WR = loc & ([W];(gmo|po);[R]) let rfGMO = WR \ (loc&([W];gmo);WR) (* Check equality of herd rf and of rfGMO *) empty (rf\rfGMO)|(rfGMO\rf) as RfCons (* Atomicity axion *) let infloc = (gmo & loc)^-1 let inflocext = infloc & ext let winside = (infloc;rmw;inflocext) & (infloc;rf;rmw;inflocext) & [W] empty winside as Atomic