vault backup: 2025-04-15 08:45:18

Concurrent Systems/notes/13 -.md

@@ -1,26 +0,0 @@
-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:
-![](../../Pasted%20image%2020250415082906.png)
-
-## Restrictions
-**Proposition:** a.P\a ∼ 0
-*Proof:*
-- S = {(a.P\a , 0)} is a bisimulation
-
-Which challenges can (a.P)\a have?
-- a.P can only perform a (and become P)
-- however, because of restriction, a.P\a is stuck
-
- No challenge from a.P\a, nor from 0 à bisimilar!
-
-**Proposition:**