Tackling real-life relaxed concurrency with FSL++

DOI10.1007/978-3-662-54434-1_17MaRDI QIDQ2988652zbMATH OpenOpenAlexFDO

Authors 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

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A program logic for C11 memory fences
• A separation logic for fictional sequential consistency
• Parameterized Memory Models and Concurrent Separation Logic
• Effective abstractions for verification under relaxed memory models
• Effective Abstractions for Verification under Relaxed Memory Models

Cites work

• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
• A program logic for C11 memory fences
• A promising semantics for relaxed-memory concurrency
• A separation logic for fictional sequential consistency
• CONCUR 2004 - Concurrency Theory
• Deciding Robustness against Total Store Ordering
• Fictional separation logic
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Library abstraction for C/C++ concurrency
• Mathematizing C++ concurrency
• Owicki-Gries reasoning for weak memory models
• Permission accounting in separation logic
• Robustness against Power is PSpace-complete
• Separation and information hiding
• Subjective auxiliary state for coarse-grained concurrency
• Taming release-acquire consistency
• Views, compositional reasoning for concurrent programs

Cited in

(7)

• Mechanised operational reasoning for C11 programs with relaxed dependencies
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• Making Linearizability Compositional for Partially Ordered Executions
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Concise outlines for a complex logic: a proof outline checker for TaDA
• A separation logic for fictional sequential consistency
• A program logic for C11 memory fences

Describes a project that uses

Uses Software

• Coq
• CDSChecker
• Rust

This page was built for publication: Tackling real-life relaxed concurrency with FSL++

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