A fine-grained semantics for arrays and pointers under weak memory models

DOI10.1007/978-3-031-27481-7_18MaRDI QIDQ6174541zbMATH OpenFDO

Authors Robert Colvin

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-27481-7_18

Mathematics Subject Classification ID

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)

Recommendations

• Program verification under weak memory consistency using separation logic
• A wide-spectrum language for verification of programs on weak memory models
• Verification of Concurrent Programs on Weak Memory Models
• On the verification problem for weak memory models
• A formal hierarchy of weak memory models

Cites work

• A formal hierarchy of weak memory models
• A promising semantics for relaxed-memory concurrency
• A semantics for concurrent separation logic
• A separation logic for a promising semantics
• An algebra of synchronous atomic steps
• An axiomatic basis for computer programming
• An Efficient Algorithm for Exploiting Multiple Arithmetic Units
• BI as an assertion language for mutable data structures
• Communicating state transition systems for fine-grained concurrent resources
• Concurrent Kleene Algebra
• Designing a semantic model for a wide-spectrum language with concurrency
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Ogre and Pythia: an invariance proof method for weak consistency models
• On Hoare logic and Kleene algebra with tests
• Owicki-Gries reasoning for weak memory models
• Parallelized sequential composition and hardware weak memory models
• Process algebra for synchronous communication
• Tentative steps toward a development method for interfering programs
• Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Verifying concurrent data structures by simulation
• Views, compositional reasoning for concurrent programs

Cited in

(1)

• Mathematics of Program Construction

This page was built for publication: A fine-grained semantics for arrays and pointers under weak memory models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174541)