Reasoning about nonblocking concurrency

MaRDI QIDQ3639041zbMATH OpenFDO

Authors Lindsay Groves

Publication date 28 October 2009

Full work available at URL http://www.jucs.org/jucs_15_1/reasoning_about_nonblocking_concurrency

zbMATH Keywords

atomicityconcurrencylinearisabilitylock-free algorithmsnonblocking algorithmsreductionshared memorysimulation relationverification

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Modular verification of a non-blocking stack
• Nonblocking Algorithms and Backward Simulation
• Verifying concurrent data structures by simulation
• Proving that non-blocking algorithms don't block
• Explanation of two non-blocking shared-variable communication algorithms

Cited in

(6)

• Using refinement calculus techniques to prove linearizability
• Modular termination verification for non-blocking concurrency
• Modular verification of a non-blocking stack
• Nonblocking Algorithms and Backward Simulation
• Explanation of two non-blocking shared-variable communication algorithms
• Proving that non-blocking algorithms don't block

This page was built for publication: Reasoning about nonblocking concurrency

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