Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav07_lecture_18 [2007/05/28 22:48] vasu.singh |
sav07_lecture_18 [2007/06/19 21:43] (current) 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 70: | Line 76: | ||
{ b = x + y } | { b = x + y } | ||
- | + | while (*) do | |
- | while (*) do | + | |
if (*) then | if (*) then | ||
- | x++; | + | atomic{ |
- | y--; | + | x++; |
+ | y--; | ||
+ | } | ||
else | else | ||
- | y++; | + | atomic{ |
- | x--; | + | y++; |
+ | x--; | ||
+ | } | ||
endif | endif | ||
end | end | ||
- | + | || | |
- | || | + | |
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 ==== |