Proving that non-blocking algorithms don't block

DOI10.1145/1480881.1480886zbMath1315.68093OpenAlexW2124945255MaRDI QIDQ5261502

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

livenessformal verificationterminationconcurrent programming

Mathematics Subject Classification ID

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

Related Items (12)

Developments in concurrent Kleene algebra ⋮ Undecidability of Propositional Separation Logic and Its Neighbours ⋮ Rely-guarantee termination and cost analyses of loops with concurrent interleavings ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Liveness-Preserving Atomicity Abstraction ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Modular Termination Verification for Non-blocking Concurrency ⋮ Verifying Deadlock-Freedom of Communication Fabrics ⋮ 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 ⋮ A Machine-Checked Framework for Relational Separation Logic

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