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, $[[c]] \subseteq 2^{R^*}$ as the set of all possible sequences of relations of c. $[[c]] = { r_1^1 r_2^1 \ldots r_{n1}^1, r_1^2 r_2^2 \ldots r_{n2}^2, \ldots, r_1^l r_2^2 \ldots r_{nk}^k}$ .

$[[\, [r]\, ]] = \{ r \}$

$[[C_1; C_2]] = [[C_1]] [[C_2]] = \{r_1 \ldots r_n s_1 \ldots s_m | r_i \in [[C_1]] and s_j \in [[C_2]] \}$ (This is similar to a language theoretic approach, where we express the concatenation of two languages $L_1$ and $L_2$ as $L1.L2 = \{w_1 w_2 \mid w_1 \in L_1$ and $w_2 \in L_2 \}$ .

$[[C_1 [] C_2 ]] = [[C_1]] \cup [[C_2]]$ .

Let $A = \{bar, rab\}$ and $B = \{bara\}$ . Then $A.B = \{barbara, rabbara\}$ and $A \cup B = \{bar, rab, bara\}$ .

$[[ C_1 || C_2 ]] = \bigcup {\{I(S_1,S_2)\}}$ where $S_1 = [[C_1]]$ and $S_2 = [[C_2]]$ , where

$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$ and $S_2 = S_2^1 S_2^2 \ldots S_2^n \}$ .

$[[ C^* ]] = \cup_{n \ge 0} [[C^n]]$ where $[[C^0]] = \emptyset$ and $[[C^{n+1}]] = [[ C^n ; C]]$ .

$[[$ atomic $(C) ]] =$ eval $([[C]])$ where eval is a function $eval: 2^{R^*} \rightarrow R$ such that eval $(\{r_1^1 \ldots r_{n1}^1, r_1^2 \ldots r_{n2}^2, \ldots, r_1^k \ldots r_{nk}^k \}) = (r_1^1 \circ r_1^2 \ldots \circ r_{n1}^1) \cup \ldots \cup (r_1^k \circ r_2^k \ldots \circ r_{nk}^k)$ .

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))*

$= (r1[]r2)^*||(r3[]r4)^* \subseteq (r1 [] r2 [] r3 [] r4)^*$

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

Verifying properties of parallel programs: an axiomatic approach

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:

$FV(I) \subseteq r$
variables in $FV(P_i) \cup FV(Q_i)$ not modified outside $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.