Analysing lock-free linearizable datatypes using CSP

DOI10.1007/978-3-319-51046-0_9MaRDI QIDQ1708716zbMATH OpenOpenAlexFDO

Authors Gavin Lowe

Publication date 26 March 2018

Full work available at URL https://doi.org/10.1007/978-3-319-51046-0_9

Mathematics Subject Classification ID

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

• A sound and complete proof technique for linearizability of concurrent data structures
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Proving Linearizability Via Non-atomic Refinement
• Testing and verifying concurrent objects
• Automatically verifying concurrent queue algorithms

Cited in

(6)

• Local linearizability for concurrent container-type data structures
• Static Livelock Analysis in CSP
• Checking opacity and durable opacity with FDR
• View abstraction for systems with component identities
• Local analysis of determinism for CSP
• Compositional and local livelock analysis for CSP

This page was built for publication: Analysing lock-free linearizable datatypes using CSP

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