Mathematizing C++ concurrency

DOI10.1145/1926385.1926394MaRDI QIDQ5408531zbMATH OpenOpenAlexFDO

Authors Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://kar.kent.ac.uk/50265/1/popl085ap-sewell.pdf

zbMATH Keywords

relaxed memory modelssemantics

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A promising semantics for relaxed-memory concurrency
• Relaxed-memory concurrency and verified compilation
• Library abstraction for C/C++ concurrency
• A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
• CompCertTSO

Cited in

(27)

• TSO-to-TSO linearizability is undecidable
• A formal C memory model for separation logic
• A denotational semantics for SPARC TSO
• Thread-modular analysis of release-acquire concurrency
• Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations
• Overhauling SC atomics in C11 and OpenCL
• Library abstraction for C/C++ concurrency
• Aliasing restrictions of C11 formalized in Coq
• Tackling real-life relaxed concurrency with FSL++
• Lem: a lightweight tool for heavyweight semantics
• Owicki-Gries reasoning for weak memory models
• scientific article; zbMATH DE number 5526622 (Why is no real title available?)
• Modular relaxed dependencies in weak memory concurrency
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Dynamic race detection for C++11
• A denotational semantics for SPARC TSO
• Operational semantics of a weak memory model with channel synchronization
• Making Linearizability Compositional for Partially Ordered Executions
• Decidability of liveness for concurrent objects on the TSO memory model
• Reasoning about promises in weak memory models with event structures
• Optimal stateless model checking for causal consistency
• Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
• Compositional reasoning for non-multicopy atomic architectures
• Mechanised operational reasoning for C11 programs with relaxed dependencies
• Verification of the release-acquire semantics
• Linearizability on hardware weak memory models
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Mathematizing C++ concurrency

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