Explanation of two non-blocking shared-variable communication algorithms
DOI10.1007/S00165-011-0213-4zbMATH Open1298.68062OpenAlexW2028010419MaRDI QIDQ469352FDOQ469352
Authors: Richard Bornat, Hasan Amjad 
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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- MASCOT
- Elucidating concurrent algorithms via layers of abstraction and reification
- Resources, concurrency, and local reasoning
- A Marriage of Rely/Guarantee and Separation Logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Modular Safety Checking for Fine-Grained Concurrency
- Process synchronisation in MASCOT
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Inter-process buffers in separation logic with rely-guarantee
- Relational separation logic
Cited In (7)
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Balancing expressiveness in formal approaches to concurrency
- Elucidating concurrent algorithms via layers of abstraction and reification
- Possible values: exploring a concept for concurrency
- Inter-process buffers in separation logic with rely-guarantee
- Reasoning about nonblocking concurrency
- Specifying and reasoning about shared-variable concurrency
Uses Software
This page was built for publication: Explanation of two non-blocking shared-variable communication algorithms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q469352)
