15 lines
1,002 B
Markdown
15 lines
1,002 B
Markdown
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)}$$
|
|
|
|
If we consider S(2) as the specification of the expected behavior of a binary semaphore and S(1) | S(1) as its concrete implementation, we can show that $$S^{(1)}|S^{(1)} \space \textasciitilde \space S^{2}$$
|
|
This means that the implementation and the specification do coincide. To show this equivalence, it suffices to show that following relation is a bisimulation:
|
|
|
|
|
|
## Congruence
|