Relaxed memory models
From MaRDI portal
Publication:5261535
DOI10.1145/1480881.1480930zbMATH Open1315.68173OpenAlexW2104245532MaRDI QIDQ5261535FDOQ5261535
Authors: Gérard Boudol, Gustavo Petri 
Publication date: 3 July 2015
Published in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1480881.1480930
Recommendations
- Generative operational semantics for relaxed memory models
- An operational happens-before memory model
- Relationships between memory models
- A calculus for relaxed memory
- A model of memory dynamics
- scientific article; zbMATH DE number 1728265
- On thin air reads towards an event structures model of relaxed memory
- A formal hierarchy of weak memory models
Cited In (24)
- Operational semantics of a weak memory model with channel synchronization
- A denotational semantics for SPARC TSO
- Operational semantics of a weak memory model with channel synchronization
- Parallelized sequential composition and hardware weak memory models
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
- Verification of STM on relaxed memory models
- Operational semantics with semicommutations
- Observation-based concurrent program logic for relaxed memory consistency models
- Brookes is relaxed, almost!
- On thin air reads towards an event structures model of relaxed memory
- Relaxed operational semantics of concurrent programming languages
- Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
- A denotational semantics for SPARC TSO
- Verified software toolchain (invited talk)
- A calculus for relaxed memory
- Programmer-centric memory consistency modelling
- Studying Operational Models of Relaxed Concurrency
- An axiomatic specification for sequential memory models
- A formal hierarchy of weak memory models
- Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
- An operational happens-before memory model
- Generative operational semantics for relaxed memory models
- A promising semantics for relaxed-memory concurrency
- Context-bounded analysis of TSO systems
This page was built for publication: Relaxed memory models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5261535)
