A fine-grained semantics for arrays and pointers under weak memory models
From MaRDI portal
Publication:6174541
DOI10.1007/978-3-031-27481-7_18zbMath1529.68177MaRDI QIDQ6174541
Publication date: 17 August 2023
Published in: Formal Methods (Search for Journal in Brave)
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Unnamed Item
- A semantics for concurrent separation logic
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Designing a semantic model for a wide-spectrum language with concurrency
- An algebra of synchronous atomic steps
- A separation logic for a promising semantics
- A formal hierarchy of weak memory models
- Views
- Concurrent Kleene Algebra
- Owicki-Gries Reasoning for Weak Memory Models
- Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems
- Tentative steps toward a development method for interfering programs
- Process algebra for synchronous communication
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- BI as an assertion language for mutable data structures
- Ogre and Pythia: an invariance proof method for weak consistency models
- A promising semantics for relaxed-memory concurrency
- Communicating State Transition Systems for Fine-Grained Concurrent Resources
- An Efficient Algorithm for Exploiting Multiple Arithmetic Units
- An axiomatic basis for computer programming
- On Hoare logic and Kleene algebra with tests
- Parallelized sequential composition and hardware weak memory models
This page was built for publication: A fine-grained semantics for arrays and pointers under weak memory models
