Modeling LSE2 extension

[Blaisorblade]

IIUC, ARMv8-A LSE2 (Large System Extension 2) enables atomic misaligned reads that "fit in cachelines", and that seems to affect the model in minor ways — it seems the "storage" model reflects properties of caches and not just RAM.

For instance, a LDP instruction can read the the 64-bit value at address range [0x4, 0x12[ atomically — but only if the memory has inner & outer writeback cacheability.

• If your RAM model forbids such a misaligned access, LSE2 requires allowing that, at least sometimes.
• If your RAM model always allows such a misaligned access, no change is needed for LSE2 — that just seems a bit odd, and it means storage behavior accounts for some effects of caches as well.

---

References.

This is documented in prose in DDI0487 I.a, Sec. B2.5.2 Alignment of data accesses.

This is also documented in the DDI0487 I.a pseudocode (but not in DDI0487 G.a): function aarch64/functions/memory/AArch64.MemSingle (in Appendix J-1) will let CheckSingleAccessAttributes decide to split the access.

[fshaked]

Hi Blaisorblade,

• The model doesn't support LSE2 at the moment.
• The storage subsystem is not supposed to be a model of RAM (this is more clear in the Flowing and POP models).
• LDP is not very well supported by the model because it requires ISA level non-determinism that is not needed by any other instruction that we modelled so far, and we didn't get to implement that.

Shaked