LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Next revision Both sides next revision
sav07_lecture_18 [2007/05/28 21:33]
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.
 +
 +
 +
 +
 +
 +
 +
  
  
Line 40: Line 47:
      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 53: Line 60:
 Let $A = \{bar, rab\}$ and $B = \{bara\}$. Then $A.B = \{barbara, rabbara\}$ and $A \cup B = \{bar, rab, bara\}$. 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 \}$. $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 ​
  
-$[[ \atomic(C) ]] = \eval([[C]])$.+  { 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 ====