• English only

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. 