Elucidating concurrent algorithms via layers of abstraction and reification
From MaRDI portal
Publication:539423
DOI10.1007/s00165-010-0156-1zbMath1216.68074MaRDI QIDQ539423
Publication date: 30 May 2011
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-010-0156-1
formal methods; concurrency; asynchronous communication mechanisms; program proof; rely/guarantee conditions; Simpson's algorithm
68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N99: Theory of software
Related Items
Explanation of two non-blocking shared-variable communication algorithms, 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
- Inter-process buffers in separation logic with rely-guarantee
- Splitting atoms safely
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
- Understanding concurrent systems
- The Role of Auxiliary Variables in the Formal Development of Concurrent Programs
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Modular Safety Checking for Fine-Grained Concurrency
- Tentative steps toward a development method for interfering programs
- Concurrent Reading While Writing
- A New Solution to Lamport's Concurrent Programming Problem Using Small Shared Variables
- The B-Book
- Separation logic and abstraction
- A Structural Proof of the Soundness of Rely/guarantee Rules
- The mutual exclusion problem
