[octalide]

What

Machine fences and ordered atomics state how they order the memory accesses around them, so mirl cannot move an access across an inline dmb, fence rw,rw, mfence or a locked op.

• effect.Order gains by: Orderings. An effect.Ordering{operand, mask, value, before, after} says that when the operand's value meets the bit pattern, its kinds join the order. This is how a row states an order its encoding carries in an operand's field: riscv fence pred/succ, the A extension's aq/rl, aarch64 dmb/dsb's CRm. effect.order(e, values) resolves the orderings against operand values. effect.joined takes the union of two orders.
• footprint.of resolves the row's order into Footprint.order. The inline block footprint (inline.effects) carries the union of its instructions' orders.
• New shared gen/src/order.mach reads order facts ([before=<kinds>] [after=<kinds>] [field=<field> bits=<pattern>], kinds as letters of rwio) and resolves them against a row. Where the row fixes the field's bits the fact holds or not when gen runs. Where an operand holds them it becomes an Ordering. The order is read from the encoding fields wherever they carry it, through the generators, and no code holds a mnemonic list.
• Each set's topic gains order and ordered lines. gen refuses a row an ordered line names that states no order, and an order or ordered line that names no row.
  • riscv (effects.txt): fence, fence.tso and pause from pred/succ, read bit by bit. fence.i orders every access. amo*, lr.*, sc.*, ssamoswap.* and the zalasr l*.aq/s*.rl from aq/rl.
  • aarch64 (effects.txt): an order line keys an instruction, or a model group by its last name. dmb and dsb from CRm<1:0> (LD, ST, full, and reserved values as full). dsb nXS and isb are full. memop, memop_128, memop_unpriv, comswap*, rcwcomswap* from A/R. ldstexclr/ldstexclp/ldstexclr_unpriv from L:o0. ldstord, ldapstl_writeback, ldiappstilp from L. ldapstl_unscaled and ldapstl_simd from opc. LDAP1/STL1 lane forms.
  • x86 (effects.txt): every _LOCK iclass from the lock field (whether f0 is there), xchg with memory, cmpccxadd, mfence, lfence (before=r after=rw), sfence (before=w after=w), serialize, cpuid. Every LOCKED row must state an order.
  • wasm (access.txt): every threads instruction (0xfe 0x00-0x4e: atomics, wait, notify, atomic.fence) is seq_cst, before=rw after=rw.
• Regenerated the riscv, aarch64, x86 and wasm row tables, and moved the four overlays' checksums in gen/src/registry.mach (last commit).

Decisions

• Order contract. An access before the row of a kind in before stays before it, and one after it of a kind in after stays after it. Acquire states after=rw, release before=rw, a full fence both. The effect.Order doc says so.
• Operand-carried orders are Ordering entries, not rules. A masked-value test per operand covers the hardest members: riscv's two 4-bit sets, aq/rl as two bits of one operand, and aarch64 CRm, where xx00 reserved means full and is not a bitwise union. The orderings name operands by index plus one, as the rest of Order does.
• The block union drops operand narrowing. joined ors the kinds and zeroes semantics, failure, scope and execution, since those name another instruction's operands. The result orders at least what each instruction did.
• Which rows must state an order is data. ordered lines name riscv mnemonic patterns, aarch64 groups or instructions, x86 iclasses and wasm ranges. x86 also requires it of every LOCKED row, read from XED's pattern.
• Upper bounds where the order is narrower than the kinds can say. fence.tso reads as rw,rw. TSO's w→r relaxation is not stated. aarch64 LDLAR/STLLR (LOAcquire/LORelease) read as acquire and release. fence.i and isb order every access, since no kind names instruction fetch or context synchronization. lfence is before=r after=rw. aarch64 domain (CRm<3:2>) is not stated as scope, so scope 0 (all agents) stands.
• cmpccxadd is included. It is implicitly locked like xchg with memory. The issue lists lock-prefixed forms and xchg. cmpccxadd has the same semantics and would otherwise be an unordered atomic.

Consumer changes (what mirl reads)

• effect.Effect.order is now filled for machine rows. Read it through footprint.of (Footprint.order), which has already resolved every Ordering against the operand values, or call effect.order(e, values). An order that depends on an operand with no known value makes footprint.of undecided (open).
• inline.effects fills Footprint.order with the union of the block's orders. A non-empty before or after means no access of those kinds may move across the block.
• effect.ordered(o) is true for an order with orderings even before they resolve.

Notes

• Checks were host-only: machd check . and gen run to regenerate. No unit tests, tool comparison, qemu or validator runs, per the v7 rules.
• Not stated, as gaps: riscv sfence.vma, hfence.*, sinval/hinval and sfence.w.inval/sfence.inval.ir (they order implicit page-table accesses, which no kind names). x86 serializing instructions other than serialize and cpuid (iret, wbinvd, mov to cr, and so on). x86 RAO-INT aadd/aand/aor/axor, which are weakly ordered by the SDM. aarch64 sb, ssbb and pssbb as anything beyond dsb's reserved-full reading. wasm 3.0 has no ordering immediates, so nothing reads one.

Closes #547