Explanation of two non-blocking shared-variable communication algorithms

DOI10.1007/S00165-011-0213-4MaRDI QIDQ469352zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

concurrencyrefinementatomicityseparation logicproofrely-guarantee

Mathematics Subject Classification ID

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

Recommendations

• Inter-process buffers in separation logic with rely-guarantee
• Reasoning about nonblocking concurrency
• Elucidating concurrent algorithms via layers of abstraction and reification
• Nonblocking Algorithms and Backward Simulation
• A technique for decomposing algorithms which use a single shared variable

Cites work

• scientific article; zbMATH DE number 3521895 (Why is no real title available?)
• scientific article; zbMATH DE number 1878545 (Why is no real title available?)
• scientific article; zbMATH DE number 2090146 (Why is no real title available?)
• scientific article; zbMATH DE number 3264018 (Why is no real title available?)
• scientific article; zbMATH DE number 3278860 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• Elucidating concurrent algorithms via layers of abstraction and reification
• Inter-process buffers in separation logic with rely-guarantee
• MASCOT
• Modular Safety Checking for Fine-Grained Concurrency
• Process synchronisation in MASCOT
• Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
• Relational separation logic
• Resources, concurrency, and local reasoning
• Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification

Cited in

(7)

• Inter-process buffers in separation logic with rely-guarantee
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
• Possible values: exploring a concept for concurrency
• Elucidating concurrent algorithms via layers of abstraction and reification
• Balancing expressiveness in formal approaches to concurrency
• Specifying and reasoning about shared-variable concurrency
• Reasoning about nonblocking concurrency

Describes a project that uses

Uses Software

• MASCOT

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)