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
>> >and any other synchronization primitive has got to include proofs of
>> Are you volunteering to organize such an effort?
>I'm willing to attempt proofs for the POSIX implementation and review
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
>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.
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk