|
|
Mechanical Proofs of Correctness for DCAS-based Concurrent Deques
Mechanical Proofs of Correctness for DCAS-based Concurrent Deques
David Detlefs and Mark Moir
Introduction
One of the authors of this page (Detlefs) was an author on the paper
DCAS-Based Concurrent Deques, with Ole Agesen, Christine
Flood, Alex Garthwaite, Paul Martin, Nir Shavit, and Guy Steele.
This paper was presented in
SPAA 2000; the
PDF is
available here.
We were invited to submit it for consideration in a "Best Papers of
SPAA" issue of a journal (which eventually, after some confusion,
turned out to be Theory of Computing Systems.) However, this
would require fleshing out of the correctness proofs, which had been
made somewhat sketchily in the conference paper.
During this time, Mark Moir had joined Sun Labs, and immersed himself
in the DCAS-based concurrent data structure work we were doing. Mark
has high standards of proof, and wished to hold us to those
standards. Mark has interest in extending and promoting the proof of
mechanical theorem provers in theoretical CS; Dave had some previous
experience which such theorem provers (and low confidence in his
ability to construct a correct proof without such aid). Therefore we
decided to work together to do a mechanical correctness proof, and
that Mark would join the paper as an author.
We used the Simplify
theorem prover, largely because Dave had been one of the developers of
that system. A description and download is available at the link just
given.
There are two algorithms in the paper. Below are links to two proof
script files, one for each of the algorithms. To run these
successfully through Simplify, one minor tweak is necessary:
you need to set an environment variable, using
setenv PROVER_D1P_MAX_EFFORT 1
or the equivalent in the command shell you use.
(This tells the
prover, on a scale of 0 to 3, how much effort to spend on an internal
proof strategy called "depth-1 plunging." As an implementor of the
prover, I apologize to users that they would ever need to hear of such
a thing. If this system were undergoing further development, this could
probably be fixed, but it isn't :-)
The journal version of the paper has a detailed explanation of the
proof; including (almost) the full text of the proof scripts. When
that is complete and cleared for publication, this page will link to
that version. For now, and for posterity and experimentation, here
are the full input files for the two proofs:
|
