Boost logo

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, gregod at, cpdaniel at, john at