Formal verification of the MCS list-based queueing lock

DOI10.1007/3-540-46674-6_24MaRDI QIDQ4501590zbMATH OpenFDO

Authors Kazuhiro Ogata, Kokichi Futatsugi

Publication date 6 May 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46674-6_24

zbMATH Keywords

queueing lock algorithm

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20)

Recommendations

• Formal verification of a practical lock-free queue algorithm
• Formal verification of concurrent programs with Read-write locks
• Automatically verifying concurrent queue algorithms
• Correct Hardware Design and Verification Methods
• VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES

Cited in

(2)

• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
• Formal verification of a practical lock-free queue algorithm

This page was built for publication: Formal verification of the MCS list-based queueing lock

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