Reasoning about optimistic concurrency using a program logic for history

DOI10.1007/978-3-642-15375-4_27zbMATH Open1287.03071OpenAlexW1824790454MaRDI QIDQ3584944FDOQ3584944

Authors: Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang 

Publication date: 31 August 2010

Published in: CONCUR 2010 - Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-15375-4_27

Recommendations

• Specifying and verifying concurrent algorithms with histories and subjectivity
• Program verification under weak memory consistency using separation logic
• Owicki-Gries reasoning for weak memory models
• Separation logic and concurrency
• Fine-grained concurrency with separation logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (7)

• Preferred history semantics for iterated updates
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Formal verification of a lock-free stack with hazard pointers
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Specifying and verifying concurrent algorithms with histories and subjectivity
• A sound and complete proof technique for linearizability of concurrent data structures
• A relational shape abstract domain

This page was built for publication: Reasoning about optimistic concurrency using a program logic for history

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