Re: [boost] boost::semaphore

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.