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
Last revision Both sides next revision
sav07_lecture_18 [2007/05/29 00:37]
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 This suggests that the two programs above are not equivalent for the purpose of reasoning
 in concurrently executing programs. in concurrently executing programs.
 +
 +
  
  
Line 75: Line 77:
   while (*) do   while (*) do
     if (*) then     if (*) then
-      x++; +      ​atomic{ 
-      y--;+        ​x++; 
 +        y--; 
 +      }
     else     else
-      y++; +      ​atomic{ 
-      x--;+        ​y++; 
 +        x--; 
 +      }
     endif     endif
   end   end
Line 97: Line 103:
   end   end
   { b = x + y }   { 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 ====