Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models

DOI10.1007/978-3-319-47958-3_4zbMath1483.68066OpenAlexW2529658871MaRDI QIDQ3179280

Toshiyuki Maeda, Tatsuya Abe

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

observationrelaxed memory consistency modelconcurrent program logicindependent reads independent writesrely/guarantee method

Mathematics Subject Classification ID

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

Related Items (2)

Local Data Race Freedom with Non-multi-copy Atomicity ⋮ Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models

Uses Software

• SPIN
• Oracle

Cites Work

• Unnamed Item
• Unnamed Item
• Concurrent Kleene algebra and its foundations
• The Rely-Guarantee method for verifying shared variable concurrent programs
• On Rely-Guarantee Reasoning
• Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models
• Owicki-Gries Reasoning for Weak Memory Models
• Parameterized Memory Models and Concurrent Separation Logic
• Relaxed memory models
• An axiomatic basis for computer programming

This page was built for publication: Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models