Modular Verification of a Non-Blocking Stack

Matthew J. Parkinson, Richard Bornat, and Peter O'Hearn

Abstract

This paper contributes to the development of techniques for the

modular proof of programs that include concurrent algorithms. We

present a proof of a non-blocking concurrent algorithm, which provides

a shared stack. The inter-thread interference, which is essential

to the algorithm, is confined in the proof and the specification to

the modular operations, which perform push and pop on the stack.

This is achieved by the mechanisms of separation logic. The effect

is that inter-thread interference does not pollute specification

or verification of clients of the stack.

Details

Publication typeInproceedings
Published inPOPL
Pages297–302
PublisherAssociation for Computing Machinery, Inc.
> Publications > Modular Verification of a Non-Blocking Stack