Explanation of two non-blocking shared-variable communication algorithms

DOI10.1007/s00165-011-0213-4zbMath1298.68062OpenAlexW2028010419MaRDI QIDQ469352

Hasan Amjad, Richard Bornat

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

zbMATH Keywords

refinementconcurrencyproofseparation logicatomicityrely-guarantee

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Possible values: exploring a concept for concurrency ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Balancing expressiveness in formal approaches to concurrency

Uses Software

• MASCOT

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Explanation of two non-blocking shared-variable communication algorithms