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