Proving that non-blocking algorithms don't block

DOI10.1145/1480881.1480886MaRDI QIDQ5261502zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Reasoning about nonblocking concurrency
• Proving concurrent noninterference
• Efficient Transformations of Obstruction-Free Algorithms into Non-blocking Algorithms
• Nonblocking Algorithms and Backward Simulation
• Distributed Computing
• Time and Space Lower Bounds for Nonblocking Implementations
• Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors
• Tasks in modular proofs of concurrent algorithms

Cited in

(15)

• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Modular verification of a non-blocking stack
• Balancing expressiveness in formal approaches to concurrency
• Nonblocking Algorithms and Backward Simulation
• Liveness-Preserving Atomicity Abstraction
• Modular termination verification for non-blocking concurrency
• Developments in concurrent Kleene algebra
• Towards a thread-local proof technique for starvation freedom
• Undecidability of propositional separation logic and its neighbours
• Reasoning about nonblocking concurrency
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Verifying deadlock-freedom of communication fabrics
• Rely-guarantee termination and cost analyses of loops with concurrent interleavings
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• A machine-checked framework for relational separation logic

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)