Mathematizing C++ concurrency

DOI10.1145/1926385.1926394zbMath1284.68165OpenAlexW4234066571MaRDI QIDQ5408531

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

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

semanticsrelaxed memory models

Mathematics Subject Classification ID

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

Related Items (18)

Modular Relaxed Dependencies in Weak Memory Concurrency ⋮ A denotational semantics for SPARC TSO ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ TSO-to-TSO linearizability is undecidable ⋮ Owicki-Gries Reasoning for Weak Memory Models ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Thread-modular analysis of release-acquire concurrency ⋮ Aliasing Restrictions of C11 Formalized in Coq ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ A formal C memory model for separation logic ⋮ Decidability of liveness for concurrent objects on the TSO memory model ⋮ Reasoning about promises in weak memory models with event structures ⋮ Tackling Real-Life Relaxed Concurrency with FSL++ ⋮ Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ Unnamed Item ⋮ Lem: A Lightweight Tool for Heavyweight Semantics ⋮ Linearizability on hardware weak memory models

Uses Software

• Isabelle/HOL

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