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 .
atomiceval where eval is a function such that eval.
An example
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.