Matthew J. Parkinson, Richard Bornat, and Peter O'Hearn
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.
Publisher Association for Computing Machinery, Inc.