Weak memory

[Google Scholar]

Distributed Shared Memory, ISA specification, Memory coherence, Total store order (TSO), uSpec

  • Herding cats: Modelling, simulation, testing, and data mining for weak memory [alglave:toplas:2014]
  • Isla: Integrating full-scale ISA semantics and axiomatic concurrency models [armstrong:cav:2021]
  • Reasoning about the ARM weakly consistent memory model [chong:asplos:2008]
  • Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations [hsiao:micro:2021]
  • Memory coherence in shared virtual memory systems [li:tocs:1989]
  • COATCheck: Verifying memory ordering at the hardware-OS interface [lustig:asplos:2016]
  • RTLcheck: Verifying the memory consistency of RTL designs [manerkar:micro:2017]
  • Axiomatic hardware-software contracts for security [mosier:isca:2022]
  • Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8 [pulte:popl:2017]
  • CompCertTSO: A verified compiler for relaxed-memory concurrency [sevcik:jacm:2013]
  • x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors [sewell:cacm:2010]
  • ARMv8-A system semantics: Instruction fetch in relaxed architectures [simner:pls:2020]
  • Processor memory system verification using DOGReL: a language for specifying end-to-end properties [stewart:difts:2014]
  • Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware [tao:sosp:2021]
  • Opening Pandora's box: A systematic study of new ways microarchitecture can leak private data [vicarte:isca:2021]
  • Automatically comparing memory consistency models [wickerson:popl:2017]
  • Integrating memory consistency models with instruction-level abstraction for heterogeneous system-on-chip verification [zhang:fmcad:2018]