We have to be a little careful to make sure the class invariant's true when a
binary semaphore's initialized. If the semaphore s is initialized to false, then
the invariant
0 <= #s.put() - #s.get() <= 1
holds. However, if s is initialized to true and the first operation is a
get(), then #s.put() - #s.get() is -1 and the invariant doesn't
hold.
One way around this problem is to change the invariant to
0 <= |#s.put() - #s.get()| <= 1
Another way is to assume that, when a semaphore is initialized to true, the
initial value of #s.put() is 1.
Which fix is better is a matter of choice. The first fix is weaker than the second, and so might be harder to use, depending on how it's being used.
This page last modified on 23 June 2003.