Proving that non-blocking algorithms don't block

DOI10.1145/1480881.1480886zbMATH Open1315.68093OpenAlexW2124945255MaRDI QIDQ5261502FDOQ5261502

Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis

Publication date: 3 July 2015

Published in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1480881.1480886

zbMATH Keywords

formal verificationterminationconcurrent programmingliveness

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) General topics in the theory of algorithms (68W01)

Cited In (12)

• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• A Machine-Checked Framework for Relational Separation Logic
• Balancing expressiveness in formal approaches to concurrency
• Liveness-Preserving Atomicity Abstraction
• Developments in concurrent Kleene algebra
• Modular Termination Verification for Non-blocking Concurrency
• Towards a Thread-Local Proof Technique for Starvation Freedom
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Rely-guarantee termination and cost analyses of loops with concurrent interleavings
• Undecidability of Propositional Separation Logic and Its Neighbours
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Verifying Deadlock-Freedom of Communication Fabrics

Recommendations

• Title not available (Why is that?) 👍 👎
• Time and Space Lower Bounds for Nonblocking Implementations 👍 👎
• Nonblocking Algorithms and Backward Simulation 👍 👎
• Efficient Transformations of Obstruction-Free Algorithms into Non-blocking Algorithms 👍 👎
• Distributed Computing 👍 👎
• Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors 👍 👎
• Proving Concurrent Noninterference 👍 👎
• Tasks in modular proofs of concurrent algorithms 👍 👎

This page was built for publication: Proving that non-blocking algorithms don't block

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