A program logic for C11 memory fences

DOI10.1007/978-3-662-49122-5_20MaRDI QIDQ2796064zbMATH OpenOpenAlexFDO

Authors Marko Doko, Viktor Vafeiadis

Publication date 23 March 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-49122-5_20

Mathematics Subject Classification ID

Logic in computer science (03B70) 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

• Tackling real-life relaxed concurrency with FSL++
• A separation logic for fictional sequential consistency
• Automating deductive verification for weak-memory programs
• Program verification under weak memory consistency using separation logic
• Fences in weak memory models

Cited in

(10)

• Thread-modular analysis of release-acquire concurrency
• Automating deductive verification for weak-memory programs
• A separation logic for fictional sequential consistency
• Taming release-acquire consistency
• Tackling real-life relaxed concurrency with FSL++
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Making Linearizability Compositional for Partially Ordered Executions
• Concise outlines for a complex logic: a proof outline checker for TaDA
• Reasoning about promises in weak memory models with event structures
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A program logic for C11 memory fences

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