Tackling Real-Life Relaxed Concurrency with FSL++

DOI10.1007/978-3-662-54434-1_17zbMath1485.68061OpenAlexW2596443718MaRDI QIDQ2988652

Marko Doko, Viktor Vafeiadis

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54434-1_17

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) 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

Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL, 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

Uses Software

• Coq
• CDSChecker
• Rust

Cites Work

• Unnamed Item
• A Program Logic for C11 Memory Fences
• A Separation Logic for Fictional Sequential Consistency
• A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
• Taming release-acquire consistency
• Fictional Separation Logic
• Library abstraction for C/C++ concurrency
• Views
• Subjective auxiliary state for coarse-grained concurrency
• Deciding Robustness against Total Store Ordering
• Owicki-Gries Reasoning for Weak Memory Models
• Separation and information hiding
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• On Thin Air Reads Towards an Event Structures Model of Relaxed Memory
• Robustness against Power is PSpace-complete
• Permission accounting in separation logic
• CONCUR 2004 - Concurrency Theory
• A promising semantics for relaxed-memory concurrency
• Mathematizing C++ concurrency