Re: [boost] boost::semaphore

From: Beman Dawes (bdawes_at_[hidden])
Date: 2001-10-23 17:51:39

At 05:15 PM 10/22/01 -0500, Kevin S. Van Horn 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.

Thanks.  I'd guess most Boosters never use formal proofs, and would be 
interested in seeing how they apply to a practical problem.

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

Try http://www.opengroup.org/austin/  It looks like you have to sign up for 
a list, like Boost, before you can access the current draft.

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

PDF is OK, but the file size can become an issue (because we don't like 
blowing up the size of the boost_all download.

 >3. Where do we put the proofs?  In my mind, this is implementation
 >   documentation that should stay with the code somehow.

Yes, they should probably be added to the docs.  A little hard to say 
without seeing them first, of course.

 >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 library has already been accepted, so generally should be fairly 
stable.  But the specific issue of semaphore has come up, and there may 
(will?) be a change there.

--Beman