Semaphore invariant
Given that:
S_initial >= 0
Invariant:
S_current = S_initial + #signal(S) - #wait(S)
#signal(S)
-> no of signal()
operations executed on S
#wait(S)
-> no of wait()
operations completed on S
This is because each signal
call always increments S by 1, wait
call always decrements by 1.