Re: [boost] boost::semaphore

From: Kevin S. Van Horn (kevin.vanhorn_at_[hidden])
Date: 2001-10-22 13:24:31

On Mon, 22 Oct 2001 williamkempf_at_[hidden] wrote:

> 2)  He quotes a classic paper by Hansen which states that semaphores
> are unsafe for general use

Could you summarize the argument?  I imagine it's the same problem that
mutexes have if you don't use something like scoped_lock: you can't guarantee
that everybody plays by the rules.

> process, and, unfortunately, I felt there wasn't enough reasoning for
> removing this "fundamental" concept and didn't do so.  Now I'd like to
> reconsider and simply remove it completely.

I think we should keep the semaphores, if for no other reason than to give
students in OS courses something to play with :-).  It doesn't hurt to have
them, as long as they are implemented correctly, and clearly documented as to
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.  This stuff is tricky enough that I wouldn't trust any of the
code until I've seen and understood a thorough correctness proof, and know
that at least three other people familiar with proofs of concurrent systems
have done the same.  Not that I think correctness proofs are a panacea --
instead, I view them as one more weapon in the bug-fighting arsenal.  That is,
a good way to find bugs is to try to prove your solution correct.  After the
third or fourth unsuccessful proof attempt, you begin to suspect that there's
something wrong with your solution... and the troubles you've had with your
proof will lead you to the bug.

BTW, the claim that putting a maximum count for a semaphore leads to race
conditions is, I believe, only true for "weak" semaphores.  For strong
semaphores with a maximum count value, the increment/up/signal/V and
decrement/down/wait/P operations are symmetric.