Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav07_lecture_18 [2007/05/28 22:22] vasu.singh |
sav07_lecture_18 [2007/06/19 21:43] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Lecture 13: Concurrency ====== | ====== Lecture 13: Concurrency ====== | ||
+ | (See also [[SAV07 Lecture 26]].) | ||
==== A language with concurrency primitives ==== | ==== A language with concurrency primitives ==== | ||
Line 27: | Line 28: | ||
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. | ||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
Line 42: | Line 50: | ||
c ::= [r] | c[]c | c;c | c* | c||c | atomic(c) | c ::= [r] | c[]c | c;c | c* | c||c | atomic(c) | ||
- | We express the semantics of c as the set of all possible sequences of relations of 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}$. | $[[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}$. | ||
Line 61: | Line 69: | ||
$[[ C^* ]] = \cup_{n \ge 0} [[C^n]]$ where $[[C^0]] = \emptyset$ and $[[C^{n+1}]] = [[ C^n ; C]]$. | $[[ 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: R* \rightarrow R$ such that | + | $[[ $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 | 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)$. | r_2^k \ldots \circ r_{nk}^k)$. | ||
+ | |||
+ | An example | ||
+ | |||
+ | { b = x + y } | ||
+ | while (*) do | ||
+ | if (*) then | ||
+ | atomic{ | ||
+ | x++; | ||
+ | y--; | ||
+ | } | ||
+ | else | ||
+ | atomic{ | ||
+ | y++; | ||
+ | x--; | ||
+ | } | ||
+ | endif | ||
+ | end | ||
+ | || | ||
+ | while (*) do | ||
+ | if (*) then | ||
+ | atomic{ | ||
+ | x++; | ||
+ | y--; | ||
+ | } | ||
+ | else | ||
+ | atomic{ | ||
+ | y++; | ||
+ | x--; | ||
+ | } | ||
+ | endif | ||
+ | end | ||
+ | { b = x + y } | ||
+ | |||
+ | In our language, this example can be expressed as | ||
+ | | ||
+ | (atomic(x:=x+1;y:=y-1)[]atomic(x:=x-1;y:=y+1))* || (atomic(x:=x+1;y:=y-1)[]atomic(x:=x-1;y:=y+1))* | ||
+ | |||
+ | $ = (r1[]r2)^*||(r3[]r4)^* \subseteq (r1 [] r2 [] r3 [] r4)^*$ | ||
==== Global reachability invariants ==== | ==== Global reachability invariants ==== |