More practice with interleavings (Adapted from Problem 2.19 from Andrews's MPD text)
Semaphores
< await (s > 0) s = s - 1; >
< s = s + 1; >
wait(s)
and signal(s)
work the same for binary and counting (general) semaphores1
or 0
Class exercises
0 <= s1+s2 <= 1