Elucidating concurrent algorithms via layers of abstraction and reification

DOI10.1007/s00165-010-0156-1zbMath1216.68074OpenAlexW2004321173MaRDI QIDQ539423

Ken Pierce, Cliff B. Jones

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

zbMATH Keywords

formal methodsconcurrencyasynchronous communication mechanismsprogram proofrely/guarantee conditionsSimpson's algorithm

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of software (68N99)

Related Items (4)

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 ⋮ Explanation of two non-blocking shared-variable communication algorithms

Uses Software

• Rodin

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

This page was built for publication: Elucidating concurrent algorithms via layers of abstraction and reification