Wait-free linearization with a mechanical proof

DOI10.1007/BF01784240MaRDI QIDQ5137000zbMATH OpenOpenAlexFDO

Authors W. H. Hesselink

Publication date 30 November 2020

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01784240

zbMATH Keywords

Boyer-Moore logicconsensuscorrectnessgrain of atomicitylinearizablemechanical verificationmemory managementshared data objectwait-free

Mathematics Subject Classification ID

Distributed systems (68M14) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)

Recommendations

• Wait-free linearization with an assertional proof
• A sound and complete proof technique for linearizability of concurrent data structures
• Proving Linearizability Via Non-atomic Refinement
• Aspect-oriented linearizability proofs
• Aspect-oriented linearizability proofs

Cites work

• A calculus of communicating systems
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• A verification system for concurrent programs based on the Boyer-Moore prover
• An axiomatic proof technique for parallel programs
• Applications of Process Algebra
• Beyond atomic registers: Bounded wait-free implementations of nontrivial objects
• FM8501: a verified microprocessor
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 50008 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 3415379 (Why is no real title available?)
• Wait-free linearization with an assertional proof

Cited in

(5)

• A simple proof technique for priority-scheduled systems
• Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
• A simple constructive computability theorem for wait-free computation
• Invariants for the construction of a handshake register
• Wait-free linearization with an assertional proof

Describes a project that uses

Uses Software

• HOL
• NQTHM
• UNITY

This page was built for publication: Wait-free linearization with a mechanical proof

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