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
.
where
and
, where
and
.
where
and
.
atomic
eval
where eval is a function
such that
eval
.
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))*
Global reachability invariants
Assume that atomic only applies to sequences of relations (so we treat them as biger atomic relations).
While theorem for parallel programs
(r1 [] ... [] rn)* || (r1 [] ... [] rn)* ||
While theorem when atomic is present - implementing atomic
- global lock
- transactions with state copying
Assume any set of states is expressible in our logic (allow set theory or FO logic with axioms).
Invariant for resulting while program is a global reachability invariant.
- good: only talks about current state
- bad: potentially refers to all components of parallel process
Alternative: complete history variables
- good: only talks about individual parallel process (except for join points)
- bad: refers not only to current, but also past states
Any point in between: introduce auxiliary variables, which can be local or global, whatever is best for the given program.
Example.
{x=0} (x:=x+1 || x:=x+10) {x=11}
Owicki-Gries method
Idea
- whenever modifying a group of shared variables (=resource), enforce certain invariants on those variables
- prevent interleavings within updates to variables of a resource
Examples: bytes of a word, nodes in a list
Parallel composition construct declares resources and starts parallel threads:
resource r1(vars1), ..., rn(varsn) cobegin S1 || ... || Sn coend
(Assume only one such top-level construct, for simplicity. Assume one resource.)
Accessing variables in a resource:
with r when B do S
Requirements:
- variable written in some process and used in another must be in a resource
- if a variable is in a resource, it can only be accessed using 'with' statement
Proof rules: introduce global invariant I for shared variables
{P & B & I} S {Q & I} -------------------------- {P} with r when B do S {Q}
{P1} S1 {Q1}, ..., {Pn} Sn {Qn} ------------------------------------------------------- {P1 & ... Pn & I} (S1 || ... || Sn) {Q1 & ... & Qn & I}
Requirements:
- variables in
not modified outside
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.