Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_lecture_18 [2007/05/28 19:34] vasu.singh |
sav07_lecture_18 [2007/05/29 00:37] vasu.singh |
||
---|---|---|---|
Line 27: | Line 27: | ||
This suggests that the two programs above are not equivalent for the purpose of reasoning | This suggests that the two programs above are not equivalent for the purpose of reasoning | ||
in concurrently executing programs. | in concurrently executing programs. | ||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
==== A semantics of the language with concurrency ==== | ==== A semantics of the language with concurrency ==== | ||
Line 32: | Line 45: | ||
What would be the semantics of || as a composition of relations? | What would be the semantics of || as a composition of relations? | ||
+ | c ::= [r] | c[]c | c;c | c* | c||c | atomic(c) | ||
+ | |||
+ | We express the semantics of c, $[[c]] \subseteq 2^{R^*}$ as the set of all possible sequences of relations of c. | ||
+ | $[[c]] = { r_1^1 r_2^1 \ldots r_{n1}^1, r_1^2 r_2^2 \ldots r_{n2}^2, \ldots, r_1^l r_2^2 \ldots r_{nk}^k}$. | ||
+ | |||
+ | $[[\, [r]\, ]] = \{ r \}$ | ||
+ | |||
+ | $[[C_1; C_2]] = [[C_1]] [[C_2]] = \{r_1 \ldots r_n s_1 \ldots s_m | r_i \in [[C_1]] and s_j \in [[C_2]] \}$ | ||
+ | (This is similar to a language theoretic approach, where we express the concatenation of two languages $L_1$ and $L_2$ as | ||
+ | $L1.L2 = \{w_1 w_2 \mid w_1 \in L_1$ and $w_2 \in L_2 \}$. | ||
+ | |||
+ | $[[C_1 [] C_2 ]] = [[C_1]] \cup [[C_2]]$. | ||
+ | |||
+ | Let $A = \{bar, rab\}$ and $B = \{bara\}$. Then $A.B = \{barbara, rabbara\}$ and $A \cup B = \{bar, rab, bara\}$. | ||
+ | |||
+ | $[[ C_1 || C_2 ]] = \bigcup {\{I(S_1,S_2)\}}$ where $S_1 = [[C_1]]$ and $S_2 = [[C_2]]$, where | ||
+ | |||
+ | $I(S_1,S_2) = \{S_1^1, S_2^1, \ldots, S_1^n, S_2^n \mid S_1 = S_1^1 S_1^2 \ldots S_1^n$ and $S_2 = S_2^1 S_2^2 \ldots S_2^n \}$. | ||
+ | |||
+ | $[[ C^* ]] = \cup_{n \ge 0} [[C^n]]$ where $[[C^0]] = \emptyset$ and $[[C^{n+1}]] = [[ C^n ; C]]$. | ||
+ | |||
+ | $[[ $atomic$(C) ]] = $eval$([[C]])$ where eval is a function $eval: 2^{R^*} \rightarrow R$ such that | ||
+ | eval$(\{r_1^1 \ldots r_{n1}^1, r_1^2 \ldots r_{n2}^2, \ldots, r_1^k \ldots r_{nk}^k \}) = (r_1^1 \circ r_1^2 \ldots \circ r_{n1}^1) \cup \ldots \cup (r_1^k \circ | ||
+ | r_2^k \ldots \circ r_{nk}^k)$. | ||
+ | |||
+ | An example | ||
+ | { b = x + y } | ||
+ | while (*) do | ||
+ | if (*) then | ||
+ | x++; | ||
+ | y--; | ||
+ | else | ||
+ | y++; | ||
+ | x--; | ||
+ | endif | ||
+ | end | ||
+ | || | ||
+ | while (*) do | ||
+ | if (*) then | ||
+ | atomic{ | ||
+ | x++; | ||
+ | y--; | ||
+ | } | ||
+ | else | ||
+ | atomic{ | ||
+ | y++; | ||
+ | x--; | ||
+ | } | ||
+ | endif | ||
+ | end | ||
+ | { b = x + y } | ||
==== Global reachability invariants ==== | ==== Global reachability invariants ==== |