You don't need to prove theorems — you need to know what your CPU + fabric + devices guarantee. ARM: Device, Normal Non-cacheable, Normal Cacheable with inner/outer shareable. RISC-V: RVWMO with fence instructions. x86: TSO (stronger). Mismatch between what software assumes and what hardware provides causes 'impossible' bugs.
Consider the Store Buffering test with distinct locations A=B=0 initially, one atomic aligned access per operation, no fences, no other writes and no compiler transformation. Core 0 stores A=1 then loads B into r0; core 1 stores B=1 then loads A into r1. Under sequential consistency (SC), (0,0) is forbidden: each zero read would have to precede the other core's store, creating a cycle when combined with the two program orders. The other three binary outcomes are allowed.
Under the x86-TSO store-buffer model for ordinary cacheable memory, (0,0) is allowed: each store can remain buffered while its core loads the other location's initial zero. The stores can drain afterwards without changing those read results. This distinguishes cross-location consistency from per-location coherence. Use assembly-level or explicitly defined model operations; ordinary racy non-atomic C/C++ is not a valid translation. See Sewell et al., x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Passing sampled executions does not prove a forbidden result can never occur.
SB LITMUS (atomic model operations; initially A=B=0)
Core 0: store A=1; r0=load B
Core 1: store B=1; r1=load A
SC allowed: (0,1), (1,0), (1,1)
x86-TSO allowed: all four binary outcomes, including (0,0)
TSO witness for (0,0):
buffer A=1; buffer B=1; load B=0; load A=0; drain stores
No fences, no other writes, ordinary cacheable memory.For supported PCIe request types, Relaxed Ordering and ID-Based Ordering affect specific ordering permissions under the selected revision and capabilities. No Snoop concerns cache-snooping treatment, not a general completion fence. Do not assume every TLP supports every attribute, or that clearing RO establishes all CPU-to-device publication and completion requirements.
Check transaction-type-specific ordering rather than one global strong/relaxed label.
Enable relaxed ordering only where the requester, completer and software contract permit it.
A readback or completion wait has the guarantees of its documented path; it is not interchangeable with any barrier instruction.