70 lines
No EOL
3.2 KiB
Markdown
70 lines
No EOL
3.2 KiB
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)}$$
|
||
The specification of a binary semaphore is the following:
|
||
$$S_{}^{(2)} \triangleq p \cdot S_{1}^{(2)}$$
|
||
$$S_{1}^{(2)} \triangleq p \cdot S_{2}^{(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:
|
||
|
||
|
||
## Restrictions
|
||
**Proposition:** $a.P \textbackslash 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:** $\bar{a}.P \textbackslash a ∼ 0$
|
||
*Proof is similar.*
|
||
|
||
## Idempotency of Sum
|
||
**Proposition:** $α.P+α.P+M ∼ α.P+M$
|
||
*Proof:*
|
||
$$S = \{ (α.P+α.P+M , α.P+M) \}$$
|
||
Is it a bisimulation?
|
||
NO: the problem is that, for example:
|
||
- α.P+α.P+M –α–> P
|
||
- α.P+M –α–> P
|
||
- BUT (P,P) in general does NOT belong to S!
|
||
|
||
So we can try with $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ \{(P,P)\}$$
|
||
But it is not yet a bisimulation.
|
||
P –β–> P’ (challenge and reply), but we don't have (P', P') in S.
|
||
(Questo per garantire che funzioni in qualsiasi caso, con qualsiasi P che eventualmente evolve in P')
|
||
|
||
So let's try with: $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ Id$$
|
||
Let's go!
|
||
|
||
## Congruence
|
||
One of the main aims of an equivalence notion between processes is to make equational reasonings of the kind: “if P and Q are equivalent, then they can be interchangeably used in any execution context”.
|
||
|
||
**This feature on an equivalence makes it a *congruence***
|
||
Not all equivalences are necessarily congruences (even though most of them are).
|
||
To properly define a congruence, we first need to define an execution context, and then what it means to run a process in a context. Intuitively:
|
||
|
||
|
||
where C is a context (i.e., a process with a hole ☐), P is a process, and $C[P]$ denotes filling the hole with P
|
||
|
||
Example: $$if \space C = (☐ | Q) \textbackslash a, \space then \space C[P] = (P | Q) \textbackslash a$$
|
||
The set C of CCS contexts is given by the following grammar:
|
||
$$C ::= ☐ \space | \space C|P \space | \space C \textbackslash a \space | \space a.C + M$$
|
||
where M denotes a sum.
|
||
|
||
An equivalence relation $R$ is a congruence if and only if
|
||
$$\forall (P, Q) \in R, \forall C.(C[P], C[Q]) \in R$$
|
||
**Is bisimilarity a congruence? Yes.**
|
||
**Theorem:**
|
||
$$if \space P ∼ Q \space then \space \forall C.C[P] ∼ C[Q]$$
|
||
|
||
Proof on the slides.
|
||
|
||
So today we learned that bisimulation is a good equivalence. |