Lecture Notes for Concurrent Programming

6 June 2003 - Avoiding Interference

Outline

• Weakening assertions.

• Read-Write separation.

• Global invariants.

• Atomic execution.

Weakened Predicates

• Consider

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

  This code seems reasonable under some execution assumptions.

• But, x = x + 1 interferes with { x = 0 }:

  Establish

  { x = 0 and x = 0 } x = x + 1 { x = 0 }.

  which equals

  { x = 0 } x = x + 1 { x = 0 }.

  The Assignment Rule gives

  { x = 0 }[ x <- x + 1]  x = x + 1  { x = 0 }
  

  which equals

  { x + 1 = 0 } x = x + 1 { x = 0 }

  or, with arithmetic

  { x = -1 } x = x + 1 { x = 0 }.

  However { x = -1 } does not imply { x = 0 } and

  { x = 0 and x = 0 } x = x + 1 { x = 0 }

  cannot be established.

• Why does this reasonable-seeming code have interference problems?

Strong Sequential Predicates

• Given

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

  only one co branch will see x equal to zero.

  • The other branch will see x equal to one.

  • And we can't say which co branch is which.

• Sequentially derived predicates tend to be too strong.

  • They don't account for concurrent execution.

• The fix for strong predicates is to weaken them.

  • Weaker predicates admit a larger set of states than do stronger predicates.

    { x = 0 } vs. { x = 0 or x = 1 }.

• Weakening a predicate involves characterizing the state resulting from other concurrent executions.

  • In this example, x is either zero or one for one branch.

Example Predicate Weakening

• Weaken the predicate to account for concurrent execution.

  • The new predicate is { x = 0 or x = 1 }.

• Any more interference?

  Establish

  { (x0 = 0 or x0 = 1) and x1 = 0 }
  x1 = x1 + 1
  { x0 = 0 or x0 = 1 }
  

  The precondition

  (x0 = 0 or x0 = 1) and x1 = 0
  

  simplifies to { x = 0 }

  By the Assignment rule, the precondition should be

  { x = 0 or x = 1 }[ x <- x + 1 ]
  

  which simplifies to { x = -1 or x = 0 }.

  If { x1 = 0 } is true (and it is), then so is { x = -1 or x = 0}.

  { (x = 0 or x = 1) and x = 0 }
  x = x + 1
  { x = 0 or x = 1 }
  

  is established and there's no more interference.

Predicate Weakening Fine Points

• Given

  co { P0 } S0 ... || { P1 } S1 ... oc
  

  and S₁ interfering with P₀, which predicate should you weaken?

  • Weaken the one being interfered with (P₀ in this case).

  • It may sometimes pay to consider weakening P₁ instead.

• Don't over-do predicate weakening.

  • Weaker predicates are less accurate than stronger ones.

  • Compare "I'll give you some money." to
    "I'll give you a million dollars."

• Sometimes the predicate is as weak as it can usefully get.

  • Given the triple
    { x >= 0 } y = sqrt(x) { y*y = x }

    the precondition can't be weakened any further.

• Re-establish the predicates derived from a weakened predicate.

  • For example, when the precondition of the triple
    { x = 0 } x = x + 1 { x = 1 }

    is weakened to { x = 0 or x = 1 }, the postcondition is no longer valid and needs to be re-established.

Read-Write Interference

• Consider

  int a2b = 0, b2a = 0
  while a2b >= 0 and b2a >= 0
    co { b2a >= 0 } a2b = f(b2a) { ... } 
    || { a2b >= 0 } b2a = g(a2b) { ... } oc
  

  Arguments to f() and g() must be non-negative.

• Each statement interferes with the other's precondition.

  • Neither
    

    { b2a >= 0 and a2b >= 0 } b2a = g(a2b) { b2a >= 0 }
    

    nor

    { a2b >= 0 and b2a >= 0 } a2b = g(b2a) { a2b >= 0 }
    

    holds.

• Each statement writes a variable in another thread's precondition.

  • And that potentially leads to interference.

Read-Write Separation

• Assertions reading variables that aren't changed can't be interfered with.

• Read one set of variables, write another set, and exchange them when it's safe.

  int old_a2b = 0, old_b2a = 0
  
  while old_a2b >= 0 and old_b2a >= 0
  
    int new_a2b, new_b2a
  
    co { old_b2a >= 0 } new_a2b = f(old_b2a) ...
    || { old_a2b >= 0 } new_b2a = g(old_a2b) ...
    oc
  
    old_b2a = new_b2a
    old_a2b = new_a2b
  

  • Notice that "when it's safe."

• Think in terms of a computation's write and read sets.

  • If write and read sets have no common variables, there's no interference.

  • Andrews calls the read set the reference set.

• Read-write separation is simple and effective.

  • However, each thread has to violate it at least once.

Global Invariants

• A loop invariant is a predicate

  • true before the loop executes,

  • true while the loop executes, and

  • true after the loop executes.

• A global invariant is a predicate

  • true before a computation executes,

  • true while the computation executes, and

  • true after the computation executes.

• There's one global invariant per concurrent computation.

  • All constituent computations maintain the invariant.

  • Loops have a different invariant per loop.

Using Global Invariants

• Define and establish the global invariant.

  • The invariant uses only global variables.

  • Establishing the invariant requires linear effort.

• Define and establish the each thread's assertions.

  • The assertions have the form { I and L }.

  • I is the global invariant.

  • L is a local assertion.

• The local assertion contains local variables.

  • Local variables can't be interfered with.

• The local assertion can also contain global variables.

Global Variables in Local Assertions

• Global variables can appear in local assertions.

  • And will have to, eventually.

• But consider

  int cnt = 0
  co . . . { I  and cnt = 3 } . . .
  || . . . { I and cnt = 3 } . . . 
  oc
  

• A global can appear in at most one thread's local assertions.

  co . . . { I } cnt++ . . .
  || . . . { I and cnt = 3 } . . . 
  oc
  

• If a thread changes a global, the global can only appear in that thread's local assertions.

  co . . . { I and cnt = 3 } cnt++
  || . . . { I } . . . 
  oc
  

Non-Interfering Interference

• Suppose thread t₁ executes

  { x = y }  x++  { x = y + 1 }  y++  { x = y }
  

  and thread t₂ executes y = -y.

• t₂ interferes with { x = y + 1 }. But,

  • t₂ can't interfere with { x = y + 1 } if it can't execute between x++ and y++.

  • t₂ may interfere with { x = y + 1 } at other times, but who cares?

  • This applies to { x = y + 1 } only; t₂ may interfere with other predicates in t₁, with { x = y }, for example.

• Suppose thread t₂ has the assertion { x = y }.

• t₁ executing x++ interferes with { x = y }, but

  • t₁ executing y++ un-interferes with { x = y }.

  • If t₂ can't execute between x++ and y++, { x = y } is maintained.

Atomic Execution

• If a thread t atomically executes the statements

  S1, S2, ..., Sn
  

  then no other thread executes from the time t starts executing S1 until t finishes executing Sn.

  • Only one thread at a time can execute atomically.

• Angle brackets <> enclose statements executed atomically.

  < S1 ; S2 ; ... ; Sn >
  

  • Angle brackets are a notational and design convenience.

  • No compiler implements atomic angle brackets.

• Atomic execution restricts external tread execution only.

  • Internal tread execution is unrestricted.

    < co [ i = 1 to n ] f(i) >
    

  • The internal threads might interfere with one another.

  • They could also deadlock the system.

Atomic Execution Properties

• An atomic sequence's postcondition is the cumulative effects of the sequence's statements on its precondition.

  { x = X and y = Y }  < x++ 
  { x = X + 1 and y = Y } 
  y++ > { x = X + 1 and y = Y + 1 }
  

• External threads can't see predicates in an atomic sequence.

  • Atomic predicates can't be interfered with.

    y = -y doesn't interfere with { x = y + 1 } in
    < x++ { x = y + 1 } y++ >

• Statements in an atomic sequence can't interfere with external predicates.

  < x++ ; y++ > doesn't interfere with { x = y }.

  • But the whole atomic sequence can cause interference

    { x = X and y = Y } 
    < x++ ; y++ > 
    { x = X + 1 and y = Y + 1 }
    

    interferes with { x <= 0 }.

Mutual Exclusion

• Restricting execution to a single thread is called mutual exclusion.

  • Mutual because any thread can do it.

  • Exclusion because all other threads are denied execution.

• Mutual exclusion is expensive.

  • Exclusive execution == no concurrency
    (at least conceptually).

  • Checking for mutual exclusion is expensive too.

    • Can I execute now? Can I execute now? ...

Points to Remember

• Sequentially derived predicates are too strong.

  • They don't account for concurrent execution.

• Weaken strong sequential predicates.

  • But don't over-do it.

• Different threads read and write the same variables.

  • They have to, at least once.

• Minimize the set of read-write shared variables.

• Global Invariants are easy to prove.

  • Only one local predicate should write a global.

• Atomic execution can hide interference.

  • This is only a design technique.

This page last modified on 11 June 2003.