Reasoning about optimistic concurrency using a program logic for history

DOI10.1007/978-3-642-15375-4_27MaRDI QIDQ3584944zbMATH OpenOpenAlexFDO

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

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)

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

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 relational shape abstract domain
• A sound and complete proof technique for linearizability of concurrent data structures

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)