ARCH20.md (1689B)
1 # ARCH20: AArch64 Acquire/Release and Exclusive Memory Ops 2 3 ## Goal 4 5 Extend the parser, instruction set, and checker to recognize AArch64 6 load/store variants that carry acquire/release or exclusive semantics, 7 so they are not silently ignored during auditing. 8 9 ## Context 10 11 The current parser only handles basic `ldr/str` families. Instructions 12 like `ldar`, `stlr`, `ldaxr`, `stlxr` appear in GHC output and represent 13 memory accesses that should be taint-checked. Missing them results in 14 false negatives. 15 16 ## Approach 17 18 Treat these as normal memory accesses for the purposes of taint 19 propagation and violation checks: 20 21 - Acquire loads: `ldar`, `ldarb`, `ldarh` 22 - Release stores: `stlr`, `stlrb`, `stlrh` 23 - Exclusive loads: `ldxr`, `ldxrb`, `ldxrh` 24 - Exclusive stores: `stxr`, `stxrb`, `stxrh` 25 - Acquire-exclusive loads: `ldaxr`, `ldaxrb`, `ldaxrh` 26 - Release-exclusive stores: `stlxr`, `stlxrb`, `stlxrh` 27 28 Semantics: 29 30 - Load variants update taint of destination register using the same 31 rules as `ldr` / `ldrb` / `ldrh`. 32 - Store variants update stack/heap tracking using the same rules as 33 `str` / `strb` / `strh`. 34 - The exclusive result register (e.g., `stxr wX, wY, [xZ]`) does not 35 carry taint from the store; it is a scalar status. Treat it as 36 Public/ProvPublic/KindScalar. 37 38 ## Scope 39 40 - Update `Instr` constructors, parser, and checker. 41 - Update taint transfer for new instructions. 42 - Update memory access extraction for `checkLineStrict`. 43 44 ## Risks 45 46 - Slightly increased parser/transfer surface area. 47 - If we miss an opcode in the family, it will remain untracked. 48 49 ## Out of Scope 50 51 - Atomic RMW instructions (`ldadd`, `swp`, `cas`, etc.). 52 Consider in a later iteration if needed.