Lab for Automated Reasoning and Analysis LARA

Lecture 13: Concurrency

(See also SAV07 Lecture 26.)

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

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.

 
sav07_lecture_18.txt · Last modified: 2007/06/19 21:43 by vkuncak
 
© EPFL 2018 - Legal notice