Observation-based concurrent program logic for relaxed memory consistency models

DOI10.1007/978-3-319-47958-3_4MaRDI QIDQ3179280zbMATH OpenOpenAlexFDO

Authors Tatsuya Abe, Toshiyuki Maeda

Publication date 21 December 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-47958-3_4

zbMATH Keywords

concurrent program logicindependent reads independent writesobservationrelaxed memory consistency modelrely/guarantee method

Mathematics Subject Classification ID

Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Program verification under weak memory consistency using separation logic
• Effective Program Verification for Relaxed Memory Models
• A separation logic for fictional sequential consistency
• Parameterized Memory Models and Concurrent Separation Logic
• Owicki-Gries reasoning for weak memory models

Cites work

• An axiomatic basis for computer programming
• Concurrent Kleene algebra and its foundations
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• Observation-based concurrent program logic for relaxed memory consistency models
• On rely-guarantee reasoning
• Owicki-Gries reasoning for weak memory models
• Parameterized Memory Models and Concurrent Separation Logic
• Relaxed memory models
• The Rely-Guarantee method for verifying shared variable concurrent programs

Cited in

(6)

• Studying Operational Models of Relaxed Concurrency
• Concurrent Library Correctness on the TSO Memory Model
• Observation-based concurrent program logic for relaxed memory consistency models
• scientific article; zbMATH DE number 1760165 (Why is no real title available?)
• scientific article; zbMATH DE number 1418374 (Why is no real title available?)
• Local Data Race Freedom with Non-multi-copy Atomicity

Describes a project that uses

Uses Software

• SPIN
• Oracle

This page was built for publication: Observation-based concurrent program logic for relaxed memory consistency models

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