Explanation of two non-blocking shared-variable communication algorithms
From MaRDI portal
Publication:469352
DOI10.1007/s00165-011-0213-4zbMath1298.68062MaRDI QIDQ469352
Publication date: 10 November 2014
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-011-0213-4
68Q60: Specification and verification (program logics, model checking, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Balancing expressiveness in formal approaches to concurrency, Possible values: exploring a concept for concurrency, Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MASCOT
- Elucidating concurrent algorithms via layers of abstraction and reification
- Inter-process buffers in separation logic with rely-guarantee
- Resources, concurrency, and local reasoning
- Relational separation logic
- Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
- A Marriage of Rely/Guarantee and Separation Logic
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Modular Safety Checking for Fine-Grained Concurrency
- Process synchronisation in MASCOT