571 B
571 B
An n-ary semaphore S(n)(p,v) is a process used to ensure that there are no more than n istances of the same activity concurrently in execution. An activity is started by action p and is terminated by action v.
The specification of a unary semaphore is the following:
S^{(1)} \triangleq p \cdot S_{1}^{(1)}S_{1}^{(1)} \triangleq p \cdot S_{1}^{(1)}The specification of a binary semaphore is the following:
S_{}^{(2)} \triangleq p \cdot S_{1}^{(2)}S_{1}^{(2)} \triangleq p \cdot S_{1}^{(2)}+v\cdot S^{(2)}S_{2}^{(2)} \triangleq v \cdot S_{1}^{(2)}