Concurrent Programming Class Notes

Lecture Notes for Concurrent Programming

5 June 2003 - Interference

Outline

State predicates and understanding computations.
Concurrency and state predicates.
- Concurrency and interference.
- Concurrency and noninterference.
- Interference analysis.
Interference and name clashes.
- Minimal scope programming.

Sequential State Predicates

The Hoare triple { pre } S { post } means
If the state predicate pre is true
and S executes to termination
then the state predicate post is true.
- For example,
```
{ x = 2 }  x = x + 1  { x = 3 }
```
If pre is not true and S executes, the results are undefined.
- Anything can happen; post may be true or false.
A triple is valid if { post } can be established given the { pre } and the predicate rule for S.
- Given { x = 2 }, you can get
  { x + 1 = 2 + 1 = 3 }.
- { x + 1 = 3 } is identical to
  { x = 3}[ x <- x + 1 ].
- By the predicate rule for assignment,
  { x = 2 } x = x + 1 { x = 3 } is valid.

Understanding Computations

Computations can be described by interleaving state predicates and statements.

If the precondition is true
and every state predicate along the way is valid
then the postcondition will be true when execution ends.

swap(x, y)

    { x = X and y = Y }

  t = x

    { x = X and y = Y and t = X }

  x = y

    { x = Y and y = Y and t = X }

  y = t

    { x = Y and y = X and t = X }
    { x = Y and y = X }

Concurrency and State Predicates

Consider { pre } S { post } again.
- pre most be true before S starts executing.
If pre is true, there's nothing to worry about. Right?
- For sequential computations, yes.
- For concurrent computations, no.

Consider now

int x = 0 co x = x + 1 || x = 1 oc

int x = 0 { x = 0 } co { x = 0 } x = x + 1 { x = 1 } || { x = 0 } x = 1 { x = 1 } oc { x = 1 }

x = 2 is a possible result of executing the co statement.

Concurrency and Interference

Concurrent execution can invalidate state predicates.
Given
```
co { x = 0 }  x = x + 1  { x = 1 }
|| { x = 0 }  x = 1      { x = 1 }
oc
```
executing the statement x = 1
invalidates the predicate { x = 0 }.
- It makes no difference if it's real or virtual concurrency.
A statement S interferes with a predicate { P } when executing S makes P evaluate to false.
Interference is a global property of statements and predicates.
- Any statement might interfere with any predicate.
Interference can occur in any concurrency type.
- Even in distributed computations, where nothing may be shared.
Controlling interference is the essential task in concurrent programming.

Noninterference

A statement may or may not interfere with a predicate.
- x = 1 does not interfere with { y = 3 }.
A statement S does not interfere with a predicate P if executing S does not change the value of P.
More formally, given the triple
```
{ pre } S { post }
```
and the property P, then S interferes with P if the if the triple
```
{ pre and P } S { P }
```
is not valid.
If { pre and P } S { P } is valid, then S does not interfere with P.
A second important task in concurrent programming is to minimize interference.

Interference Example

Given
```
co { x = 0 }  x = x + 1  { x = 1 }
|| { x = 0 }  x = 1      { x = 1 }
oc
```
does x = 1 interfere with { x = 0 }?
1. The precondition for x = 1 is { x = 0 }.
2. Is { x = 0 and x = 0 } x = 1 { x = 0 } valid?
3. Simplify { x = 0 and x = 0 } to { x = 0 }.
4. Is { x = 0 } x = 1 { x = 0 } valid?
5. Get { x = 0 }[ x <- 1] x = 1 { x = 0 } from the predicate rule for assignment.
6. { x = 0 }[ x <- 1] is identical to { 1 = 0 }, which is identical to false.
7. The triple { false } x = 1 { x = 0 } can never establish { x = 0 }.
8. x = 1 interferes with { x = 0 }.
Does x = x + 1 interfere with { x = 0 }?

Interference Analysis

Given

co { P₀ } S₀ ; . . . ; { P_m } S_m { P_{m + 1} }
|| { Q₀ } R₀ ; . . . ; { Q_n } R_n { Q_{n + 1} }
oc

how much interference analysis do you have to do, in the worst case?

In the worst case, interference analysis takes O(n²) effort for an n-statement computation.
Now you know why concurrent programming is hard.
- Concurrent programming is preventing interference.
- Preventing interference requires effort proportional to the square of the computation size in statements.

Name Clashes

Remember that threads obey scoping rules.
- Only a local thread can access local variables.
- All threads can access global variables.
When checking interference, distinguish between local and global variables.
- Non-local threads can never interfere with local variables.
For example, in
```
int x = 0, y = 0
co int i = 2  { x = 0 and i = 2 }  i++  ...
|| int i = 2  { y = 0 and i = 2 }  y = y + i ...
oc
```
the statement i++ does not interfere with any predicate in the other branch of the co statement.
- Each i is local, and so distinct from all the others.
- Think about renaming each local uniquely throughout the computation.
```
co int i₀ = 2  { x = 0 and i₀ = 2 }  i₀++  ...
|| int i₁ = 2  { y = 0 and i₁ = 2 }  y = y + i₁ ...
oc
```

Locals, Globals, and Interference

Local variables cut down on interference.
- Fewer threads access locals.
This suggests an important principle:
make all variables as local as possible.
So you see - global variables really are bad.
- Unfortunately, they're also occasionally necessary.

Hierarchical structures provide controlled local scope.

Move shared state as deep into the hierarchy as possible.

ok:

int i
proc f() 
  co i = ... // i = ... oc

better:

proc f()
  int i 
  co i = ... // i = ... oc

best:

proc f()
  co int i ; i = ... 
  // int i ; i = ...
  oc

Points to Remember

Concurrent execution can interfere with predicates.
- Interfered-with predicates lead to undefined execution.
A statement may or may not interfere with a predicate.
- It's your responsibility to see that they don't.
Interference analysis can be expensive.
- Proportional to the square of the computation size.
Scoping provides control over possible interference.
- Use it wisely and reduce analysis effort.
Interference control is the essence of concurrent programming.

This page last modified on 11 June 2003.