A load-buffer semantics for total store ordering
From MaRDI portal
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
- The benefits of duality in verifying concurrent programs under TSO
- From total store order to sequential consistency: a practical reduction theorem
- Deciding Robustness against Total Store Ordering
- Reasoning algebraically about refinement on TSO architectures
- Checking and enforcing robustness against TSO
Cites work
- Checking and enforcing robustness against TSO
- Counter-Example Guided Fence Insertion under TSO
- Effective abstractions for verification under relaxed memory models
- Effective Program Verification for Relaxed Memory Models
- Explaining relaxed memory models with program transformations
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- On the verification problem for weak memory models
- Ordering by Divisibility in Abstract Algebras
- Owicki-Gries reasoning for weak memory models
- Robustness against Power is PSpace-complete
- Software verification for weak memory via program transformation
- Stateless model checking for TSO and PSO
- The benefits of duality in verifying concurrent programs under TSO
- Verification of Concurrent Programs on Weak Memory Models
- Well (and better) quasi-ordered transition systems
- Well-structured transition systems everywhere!
- What's decidable about weak memory models?
Cited in
(16)- Parameterized model checking on the TSO weak memory model
- A high-level semantics for program execution under total store order memory
- Reasoning algebraically about refinement on TSO architectures
- Deciding Robustness against Total Store Ordering
- The benefits of duality in verifying concurrent programs under TSO
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- From total store order to sequential consistency: a practical reduction theorem
- Probabilistic total store ordering
- Reconciling preemption bounding with DPOR
- Parameterized verification under TSO with data types
- Rely-guarantee reasoning for causally consistent shared memory
- Compositional reasoning for non-multicopy atomic architectures
- Concurrent stochastic lossy channel games
- TSO games -- on the decidability of safety games under the total store order semantics
- Reachability and safety games under TSO semantics
- TSO games -- on the decidability of safety games under the total store order semantics
This page was built for publication: A load-buffer semantics for total store ordering
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3130550)
