Tackling real-life relaxed concurrency with FSL++

DOI10.1007/978-3-662-54434-1_17zbMATH Open1485.68061OpenAlexW2596443718MaRDI QIDQ2988652FDOQ2988652

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

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

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)

Cites Work

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

Cited In (7)

• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• 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
• Mechanised operational reasoning for C11 programs with relaxed dependencies
• Making Linearizability Compositional for Partially Ordered Executions

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)