Differences

This shows you the differences between two versions of the page.

--- sav07_lecture_18 [2007/05/28 21:33]
vasu.singh
+++ sav07_lecture_18 [2007/05/29 21:40]
vasu.singh
@@ Line 27: / Line 27: @@
 This suggests that the two programs above are not equivalent for the purpose of reasoning
 in concurrently executing programs.
@@ Line 40: / Line 49: @@
      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}$.
@@ Line 53: / Line 62: @@
 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
+$[[ 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$.
+$[[ 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
+      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))*
-$[[ \atomic(C) ]] = \eval([[C]])$.
+$ = (r1[]r2)^*||(r3[]r4)^* \subseteq (r1 [] r2 [] r3 [] r4)^*$
 ==== Global reachability invariants ====