Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav07_lecture_18 [2007/05/28 22:49] vasu.singh |
sav07_lecture_18 [2007/05/29 00:43] 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 84: | Line 86: | ||
| while (*) do | while (*) do | ||
| if (*) then | if (*) then | ||
| - | x++; | + | atomic{ |
| - | y--; | + | x++; |
| + | y--; | ||
| + | } | ||
| else | else | ||
| - | y++; | + | atomic{ |
| - | x--; | + | y++; |
| + | x--; | ||
| + | } | ||
| endif | endif | ||
| 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 ==== | ||