|
<< Click to Display Table of Contents >> Navigation: ASA-EMulatR Reference Guide > Introduction > Architecture Overview > Chapter 22 – Testing, Validation, and Architectural Compliance > 22.5 Memory Ordering and LL/SC Validation |
Memory model validation focuses on: visibility ordering (stores become visible to other CPUs in the correct order after barriers), store buffering behavior (write buffer drains at correct serialization points), barrier enforcement (MB produces global visibility, WMB produces local write ordering, EXCB resolves pending exceptions before continuation), and cross-CPU ordering (stores committed by CPU A are visible to CPU B after the appropriate barrier sequence completes).
Tests include: store-load reordering scenarios (verify that loads after MB see stores from before MB on another CPU), barrier release edge cases (verify that barriers release only when all conditions are met), DMA vs CPU ordering (verify that DMA completions are visible after the device signals completion), and false sharing scenarios (verify that stores to adjacent-but-distinct cache lines do not interfere with reservations on non-overlapping addresses).
Failures in memory ordering validation are considered critical correctness violations — they indicate that the memory model contract is broken, which invalidates all higher-level assumptions about SMP correctness.
LL/SC validation verifies: reservation granularity (cache-line level, 64 bytes on EV6), reservation invalidation rules (any store to the same cache line from any CPU breaks the reservation), failure semantics (STx_C returns 0 in Ra and does not write memory), and SMP contention behavior (multiple CPUs contending on the same cache line produce correct forward progress guarantees).
Specific tests: multiple CPUs performing concurrent LL/SC to the same cache line (exactly one succeeds per round), false sharing on adjacent addresses within the same cache line (reservation broken even though different bytes are targeted), exception-induced reservation clearing (LL followed by fault → STx_C must fail), barrier-induced clearing (LL followed by MB → STx_C must fail), and PAL boundary clearing (LL followed by CALL_PAL → STx_C must fail).
LL/SC correctness is mandatory for OS-level correctness — operating systems rely on atomic sequences for lock acquisition, reference counting, and concurrent data structure manipulation.
See Also: 5.11 Load-Locked / Store-Conditional (LL/SC) ; Chapter 6 - Serialization and Stall Model (barrier validation targets).