|
Boost : |
From: Kevin S. Van Horn (kevin.vanhorn_at_[hidden])
Date: 2001-10-22 17:15:35
On Tue, 23 Oct 2001, Beman Dawes wrote:
> At 01:24 PM 10/22/01 -0500, Kevin S. Van Horn wrote:
> >weak/strong/fair. But I think an important part of the review process for
>
> >this
> >and any other synchronization primitive has got to include proofs of
> >correctness.
>
> Are you volunteering to organize such an effort?
I'm willing to attempt proofs for the POSIX implementation and review
others' proofs. Here are some issues:
1. Where can I or other reviewers find authoritative references on the
semantics of the POSIX and Windows synchronization primitives, without
having to shell out $100+ bucks?
2. Proofs in plain old ASCII text are usually unreadable, as one lacks
various special symbols. I would suggest that the proofs (and perhaps
commentaries) be converted into PDF after being prepared using the
reviewer's favorite word processing / typesetting program.
3. Where do we put the proofs? In my mind, this is implementation
documentation that should stay with the code somehow.
Since this discussion was provoked by a proposal to make a major change to the
threads library interface, a final question is: how far have things
stabilized? There's no point attempting a proof of code that is going to be
rewritten next week.
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk