Formal verification of a lock-free stack with hazard pointers

DOI10.1007/978-3-642-23283-1_16MaRDI QIDQ3105753zbMATH OpenOpenAlexFDO

Authors Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif

Publication date 6 January 2012

Published in Theoretical Aspects of Computing – ICTAC 2011 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-23283-1_16

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Verifying Lock-Freedom Using Well-Founded Orders
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Quantitative reasoning for proving lock-freedom
• An integrated specification and verification technique for highly concurrent data structures
• Modular verification of a non-blocking stack

Cites work

• scientific article; zbMATH DE number 3901996 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)
• Concurrency verification. Introduction to compositional and noncompositional methods
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Formal verification of a lock-free stack with hazard pointers
• Interactive verification of concurrent systems using symbolic execution
• Modular verification of a non-blocking stack
• Proving linearizability with temporal logic
• Reasoning about optimistic concurrency using a program logic for history
• Temporal Logic Verification of Lock-Freedom

Cited in

(11)

• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Lock-free parallel and concurrent garbage collection by mark\&sweep
• Quantitative reasoning for proving lock-freedom
• Trace-based derivation of a scalable lock-free stack algorithm
• Formal verification of a lock-free stack with hazard pointers
• A sound and complete proof technique for linearizability of concurrent data structures
• Safe deferred memory reclamation with types
• Verifying a concurrent garbage collector using a rely-guarantee methodology
• Verifying Lock-Freedom Using Well-Founded Orders
• Verifying concurrent memory reclamation algorithms with grace
• Lock Free Data Structures Using STM in Haskell

Describes a project that uses

Uses Software

• KIV

This page was built for publication: Formal verification of a lock-free stack with hazard pointers

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