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
sav07_lecture_18 [2007/05/28 21:33]
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 41: 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 58: Line 67:
 $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  
 + 
 +  { 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 ==== ==== Global reachability invariants ====