include "ctrl.cat" let new-data = [R]; dd-restrict; [DATA]; intrinsic; [W] let new-addr = [R]; dd-restrict; [NDATA]; intrinsic; [M] let pom = po & (M*M) let sim = (same-instr & ((EXEC*SPEC) | (SPEC*EXEC))) \ id (* Original computation of equiv, by exclusion of differences in dependencies *) #let ddp = dd-restrict^-1; (po | po^-1); dd-restrict #let equiv = sim & (M*M) \ ddp (* Alternative computation of equiv-spec, by intersection with equivalent histories *) let instances = classes(same-instance) let depi = lift(instances,(rf-reg|rfi)^-1) #pairs of memory reads that read from different writes, one of which being external let diffw =(loc & (W * W)) \ id let diff = ((rfe^-1;diffw;rf)|(rf^-1;diffw;rfe)) let diffi = lift(instances,diff) let bisim = fulldelift(bisimulation(depi,lift(instances,same-instr)\diffi))\id let equiv = sim & (M*M) & bisim let new-ctrl = ctrlequiv equiv let AE = always-exec equiv let DW = zyva equiv Dmins let rf-mem = rf \ rf-reg show rf-reg show rf-mem as rf show co|fr as ca