Concurrent Programming Class Notes

Lecture Notes for Concurrent Programming

How much would you pay for a program that never produces wrong answers?
- Ten dollars? A million dollars? I'll give you that program for free:
```
int main() { while (true) ; }
```
Given a computation, I want to know that
- it won't produce a wrong answer, and
- it will eventually produce an answer.
- These are not always the same thing.
More generally, given a computation, I want to know that
- nothing bad ever happens, and
- something good eventually happens.

A safety property is a predicate that's always true during execution.
- A safety property is analogous to a forall predicate.
A liveness property is a predicate that's eventually true during execution.
- A liveness property is analogous to a forsome predicate.
- A liveness predicate does not have to stay true; it just has to be true once during execution.
The relation between safety and liveness is slippery.
- If P is a liveness property,
  then not P is not a safety property.
- If P is a safety property,
  then not P is not a liveness property.
- I usually forget the second not.

Proving safety properties is (relatively) hard.
- A safety property is an invariant requiring global work.
A safety property is usually the negation of a bad state.
- Bad state: a critical region has more than one thread.
- Safety property: a critical region has at most one thread.
Sometimes you can replace a global proof with local properties.
- Can this code deadlock?
```
co < await even(i) ; S₁ ; i++ > 
|| < await odd(i) ; S₂ ; i++ > 
oc
```
- Can this code deadlock?
```
co < await i % 2 == 0 ; S₁ ; i++ > 
|| < await i % 3 == 0 ; S₂ ; i++ > 
oc
```
- Make sure the predicates really are local.

Liveness properties are tricky because they can flicker between true and false.
- This is fine for the liveness property itself.
  - It just has to be true once during execution.
- It is a problem when the liveness property is a precondition too.
```
{ LNP } S { post }
```
  LNP is true sometime during execution
  but not necessarily just before S is executed.
Liveness properties as preconditions can be protected with an await statement.
```
{ true } < await LNP ; S > { post }
```
Unfortunately, await protection only solves half the problem.
- S will not execute until LNP is true.
- Flicker is still causing problems, though.

A computation contains an instruction list (the code) and two or more pointers into the list (the program counters, or PCs).
The scheduler selects the program counter that supplies the next instruction.
The scheduler uses a scheduling policy to select the next program counter.
Here's a scheduling policy for executing n threads:
```
for i = 1 to n
  while thread i has statements left
    execute the next statement in thread i
```
Execute thread 1 to completion,
then execute thread 2 to completion,
then . . .
But consider
```
bool done = false
co while (!done) skip 
|| done = true 
oc
```
Thread 2 never executes and the computation never terminates

An unconditionally fair scheduling policy eventually executes every unconditional eligible atomic statement.
- A round-robin scheduler is unconditionally fair.
```
for i = 1 to n
  if thread i statement is eligible
    execute the statement
```
Unconditional fairness doesn't deal with conditional atomic statements.
- < await B ; s > is conditionally enabled on B.

Conditional atomic statements may flicker.

co < await odd(i) ; S > 
|| while (true) i++ oc

The conditional atomic statement < await B ; S > is monotonic if B, once true, stays true.
A weakly fair scheduler is an unconditionally fair scheduler that includes monotonic conditional atomic statements.
- But only if conditional atomic statements are monotonic.

A weakly fair scheduler doesn't deal with flickering (non-monotonic) conditional atomic statements.
```
co < await odd(i) ; S > 
|| while (true) i++ 
oc
```
A persistent conditional atomic statement is true infinitely often.
- That is, it flickers infinitely often.
A strongly fair scheduler is an unconditionally fair scheduler that will eventually execute every persistent conditional atomic statement.
- A round-robin scheduler is not be strongly fair.
Strongly fair schedulers are impractical to implement.

A computation's safety and liveness properties are important.
- Nothing bad happens; something good eventually happens.
Proving safety properties requires global effort.
- But exploit local properties when possible (and try to make it possible as often as you can).
Liveness properties need to be true only once during execution.
- Easy to prove, but hard to use as preconditions.
Understand the scheduling policy in effect for programs.
- The scheduling policy influences liveness predicates.
Weakly fair scheduling policies are easy to implement.
- But require monotonic liveness properties.
Strongly fair scheduling policies are hard to implement.
- But require only persistent liveness properties.

This page last modified on 19 June 2003.