AArch64Fences
(* Protection against running tests of other architecture *)
let DMB.ISH = try DMB.ISH with emptyset
let DMB.ISHLD = try DMB.ISHLD with emptyset
let DMB.ISHST = try DMB.ISHST with emptyset
let DSB.ISH = try DSB.ISH with emptyset
let DSB.ISHLD = try DSB.ISHLD with emptyset
let DSB.ISHST = try DSB.ISHST with emptyset
let DMB.SY = try DMB.SY with emptyset
let DMB.ST = try DMB.ST with emptyset
let DMB.LD = try DMB.LD with emptyset
let DSB.SY = try DSB.SY with emptyset
let DSB.ST = try DSB.ST with emptyset
let DSB.LD = try DSB.LD with emptyset
let DMB.OSH = try DMB.OSH with emptyset
let DSB.OSH = try DSB.OSH with emptyset
let DMB.OSHLD = try DMB.OSHLD with emptyset
let DSB.OSHLD = try DSB.OSH with emptyset
let DMB.OSHST = try DMB.OSHST with emptyset
let DSB.OSHST = try DSB.OSHST with emptyset
let ISB = try ISB with emptyset
let A = try A with emptyset
and L = try L with emptyset
and Q = try Q with emptyset
and NoRet = try NoRet with emptyset
(* Fences, for showing *)
let dmb.ish = fencerel(DMB.ISH)
let dmb.ishld = fencerel(DMB.ISHLD)
let dmb.ishst = fencerel(DMB.ISHST)
let dmb.fullsy = fencerel(DMB.SY)
let dmb.fullst = fencerel(DMB.ST)
let dmb.fullld = fencerel(DMB.LD)
let dmb.sy = dmb.fullsy | dmb.ish
let dmb.st = dmb.fullst | dmb.ishst
let dmb.ld = dmb.fullld | dmb.ishld
let dsb.sy = fencerel(DSB.SY)
let dsb.st = fencerel(DSB.ST)
let dsb.ld = fencerel(DSB.LD)
let isb = fencerel(ISB)
show dmb.sy,dmb.st,dmb.ld,dsb.sy,sb.st,dsb.ld,dmb,dsb
(*
* As a restriction of the model, all observers are limited to the same
* inner-shareable domain. Consequently, the ISH, OSH and SY barrier
* options are all equivalent to each other.
*)
let dsb.full = DSB.ISH | DSB.OSH | DSB.SY
let dsb.ld = DSB.ISHLD | DSB.OSHLD | DSB.LD
let dsb.st = DSB.ISHST | DSB.OSHST | DSB.ST
(*
* A further restriction is that standard litmus tests are unable to
* distinguish between DMB and DSB instructions, so the model treats
* them as equivalent to each other.
*)
let dmb.full = DMB.ISH | DMB.OSH | DMB.SY | dsb.full
let dmb.ld = DMB.ISHLD | DMB.OSHLD | DMB.LD | dsb.ld
let dmb.st = DMB.ISHST | DMB.OSHST | DMB.ST | dsb.st
(* Flag any use of shareability options, due to the restrictions above. *)
flag ~empty (dmb.full | dmb.ld | dmb.st) \
(DMB.SY | DMB.LD | DMB.ST | DSB.SY | DSB.LD | DSB.ST)
as Assuming-common-inner-shareable-domain