Re: boost::semaphore

From: williamkempf_at_[hidden]
Date: 2001-10-22 17:21:28

--- In boost_at_y..., "Kevin S. Van Horn" <kevin.vanhorn_at_n...> wrote:
> 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?

The most authoritative reference for Windows primitives is the MSDN.  
Which is to say, there is none.  The POSIX standard can be found on 
the web.  I don't have the URL handy on this computer, but I know you 
can find it with a Google search.

> 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.

I'm sure we can figure something out along these lines.
 
> 3. Where do we put the proofs?  In my mind, this is implementation
>    documentation that should stay with the code somehow.

I'd be glad to add it to the Boost.Threads doc directory.
 
> 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.

The only concept likely to undergo changes that will effect such 
proofs happens to be the semaphore.  That said, however, 
Boost.Threads may well undergo some changes as it matures, 
particularly if the C++ standards committee considers the library 
seriously for acceptance.  However, such proofs are precisely what 
will help Boost.Threads to be considered, so it won't be a waste of 
effort even if the proofs have to be re-done because of changes.

Bill Kempf