Boost logo

Boost :

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

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