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