Boost logo

Boost :

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
> others' proofs. Here are some issues:
> 1. Where can I or other reviewers find authoritative references on
> semantics of the POSIX and Windows synchronization primitives,
> 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
> various special symbols. I would suggest that the proofs (and
> commentaries) be converted into PDF after being prepared using
> 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

Boost list run by bdawes at, gregod at, cpdaniel at, john at