Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification

DOI10.1007/978-3-540-87603-8_47MaRDI QIDQ3535380zbMATH OpenOpenAlexFDO

Authors Ken Pierce, Cliff B. Jones

Publication date 11 November 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-87603-8_47

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

• Splitting atoms in relational algebras
• A criterion for atomicity revisited
• A Marriage of Rely/Guarantee and Separation Logic
• Robustness against consistency models with atomic visibility
• An assertional criterion for atomicity
• Distributed Computing
• Concurrency and availability as dual properties of replicated atomic data

Cites work

• Concurrency verification. Introduction to compositional and noncompositional methods
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 3999266 (Why is no real title available?)
• scientific article; zbMATH DE number 2090146 (Why is no real title available?)
• Inter-process buffers in separation logic with rely-guarantee
• Modular Safety Checking for Fine-Grained Concurrency
• Non-deterministic data types: Models and implementations
• Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
• Splitting atoms safely
• Tentative steps toward a development method for interfering programs
• The B-Book

Cited in

(7)

• Possible values: exploring a concept for concurrency
• An approach to splitting atoms safely (extended abstract)
• Explanation of two non-blocking shared-variable communication algorithms
• Elucidating concurrent algorithms via layers of abstraction and reification
• Inter-process buffers in separation logic with rely-guarantee
• Splitting atoms safely
• Balancing expressiveness in formal approaches to concurrency

This page was built for publication: Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3535380)