This is an old revision of the document!
Lecture 13: Concurrency
A language with concurrency primitives
c ::= [r] | c[]c | c;c | c* | c||c | atomic(c)
[r] - havoc, assume, assert, assignments, any simple command, given by relation r
Examples
What are the possible results?
(x := 1; y := 1; z := x+y) || (y := 2; x := 12; z := x+y)
(x := 1; y := 1; z := x+y) || (y := 2; x := y+10; z := x+y)
For the above two programs, we assume that every statement is atomic. The above two programs result in different possible values for x, y and z. Consider the first program. When it terminates, the possible values for x, y and z are {(1,1,2), (12, 2, 14), (12, 1, 13)}. As for the second program, the possible values upon termination are {(1,1,2), (12, 2, 14), (12, 1, 13), (11,1,12)}. We note that the last possible valuation on (x,y,z) results from an interleaving of assignments where (y:=1) occurs between (y:=2) and (x:=y+10).
This suggests that the two programs above are not equivalent for the purpose of reasoning in concurrently executing programs.
A semantics of the language with concurrency
What would be the semantics of || as a composition of relations?
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.
.
(This is similar to a language theoretic approach, where we express the concatenation of two languages
and
as
and
.
.
Let and
. Then
and
.
S_1 = C_1
S_2 = C_2
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
S_2 = S_2^1 S_2^2 \ldots S_2^n \}
C^* = \cup_{n \ge 0} C^n
C^0 = \emptyset
\atomic(C) = \eval(C)
FV(I) \subseteq r
FV(P_i) \cup FV(Q_i)
S_i$
Need for history variables.
Granularity of concurrency
Using concurrency for efficiency: trade off between sizes of atomic sections and ease of reasoning.
Theorems about equivalence can be used to verify less concurrent version, run more concurrent one.
Operational description of
with r when B do S
with lock per resouce:
atomic(assume r_available & B; r_available := false); S; r_available := true;
it by
atomic (assume B; S)
and replace cobegin with simple || under the assumptions of Owicki-Gries?
Transactions: a more abstract mechanism for atomicity, promises to get good point in reasoning/efficiency space.