On a method of Multi-Programming

#On-a-method-of-Multi-Programming

- W.H.J Feijen, A.J.M Van Gasteren

#--W.H.J-Feijen,-A.J.M-Van-Gasteren

Submitted by: Padma Pasupathi, McMaster University

#Submitted-by:-Padma-Pasupathi,-McMaster-University

Supervised by: Emil Sekerenski

#Supervised-by:-Emil-Sekerenski

Hoare-Triples and wlp

#Hoare-Triples-and-wlp
  • Weakest liberal precondition (wlp)
  • Hoare-triple is the notation that explains wlp
  • It consists of pair of predicates P, Q and a statement S
1
2
3
4
5
  {P}  S  {Q} 
  
It can be represented as,
  
  P ⇒ S.Q

It is a boolean value which is true only if statement S starts with initial perecondition P and ends up with post condition Q.

Annotations

#Annotations

Correctness of the program is checked using the precondition, postcondition and intermediate conditions.

There are two types of correctness:

  • Global correctness
  • Local correctness

Global Correctness

#Global-Correctness

Global correctness of P in a component tells us that rest of the system does not falsify P; i.e., does not flip the state of the system from P to ¬P.

Rules of Global correctness:

{P ∨ Q} S {P}

Example

#Example

Assuming x as the integer variable with condition x ≥ 0 and statement x=x-1.

Its annotation is

1
  {x0}  x=x-1  {x0}

Global correctness proof:

#Global-correctness-proof:

Here is the proof of Global correctness

Given, statement x=x-1 condition {x ≥ 0}

By wlp representation, the above statement can be represented as,

1
2
3
4
5
6
7
    x  ≥ 0 ⇒ (x:=x-1).(x ≥ 0)  ⇒
≡         {by substitution}
    x  ≥ 0 ⇒ x-1 ≥ 0
≡         {by predicate calculus and arithmetic}
    x < 0 ∨ x ≥ 1
≡         {x is integer}
    x ≠ 0 

So x ≥ 0 is globally correct under {x ≠ 0}x:=x-1

Local Correctness

#Local-Correctness
  • Local correctness is for locally establishing a component's initital condition.
  • It is used for stand alone sequential programs.

Rule for Local correctness:

{Q} S {P}

Example

#Example

Consider the atomic statement x:=y with a condition y ≥ 0, then

1
2
3
4
5
6
7
  {P}  S  {Q} 
  
  It can be represented as,
  
  P ⇒ S.Q
  
  So, it becomes {y ≥ 0} x:=y {x ≥ 0}

Here Post condition always requires a precondition.

Mutual Exclusion

#Mutual-Exclusion

Consider a statement x+y=z and there are two components(process) C1 and C2.

Let C1 has the statements x:=x+1 and z=z+1

and C2 has the statements y:=y+1 and z=z+1

The final result of z depends on two different calls C1 and C2 as x is in C1 and y is in C2.

It can represented as shown.

3.jpg

On a parallel execution it can be represented as,

4.jpg

Annotation for this mutual exclusion could be shown as follows,

6.jpg

Concurrent execution can be shown as,

7-3.jpg

Progress Issues

#Progress-Issues

Individual Starvation

#Individual-Starvation
  • Also known as infinite overtaking
  • when there exists a computation in which the value of B oscillates an infinite number of times (between true and false)

Deadlock

#Deadlock
  • Value of B oscillates a finite number of times and then becomes stably false

Progress

#Progress
  • Value of B oscillates a finite number of times and then becomes stably true.

Total Deadlock

#Total-Deadlock

Consider the following scenario:

1
2
3
  P: ¬x ∧ ¬y
  S1: x:=true
  B1: if ¬y → skip
1
2
3
  P: ¬x ∧ ¬y
  S2: y:=true
  B2: if ¬x → skip

In this case, deadlock occurs for each of the components individually and even for the two of them simultaneously. Hence its a total deadlock.

Individual Deadlock

#Individual-Deadlock

Consider the following scenario,

1
2
3
  P: ¬x ∧ ¬y 
  B1: if ¬y → skip
  S1: x:=true
1
2
3
  P: ¬x ∧ ¬y 
  B2: if ¬x → skip
  S2: y:=true

Here deadlock occurs individually in each component but the total deadlock is impossible.

No deadlock - Guaranteed Termination

#No-deadlock---Guaranteed-Termination

Consider the following scenario,

1
2
3
4
  P: ¬x ∧ ¬y 
  B1: if ¬y → skip
  S1: x:=true
  T1: x:=false
1
2
3
4
 P: ¬x ∧ ¬y
 B2: if ¬x → skip
 S2: y:=true
 T2: y:=false

By adding y:=false and x:=false in both components, the condition is weakened in both components and now both components are guaranteed to terminate.

Individual Starvation

#Individual-Starvation

Consider the following scenario,

1
2
3
4
 P: ¬x ∧ ¬y
 *[ B2: if ¬x → skip
 S2: y:=true
 T2: y:=false ] 

Now both components have individual starvation, as A only inspects ¬y in states where y equals true and vice versa.

Progress

#Progress

Consider the following scenario,

1
2
3
4
5
  P: ¬x ∧ ¬y 
  Q2: {¬y}
  B2: if ¬x → skip
  S2: y:=true
  T2: y:=false 

Here variables x and y are private to components C1 and C2 respectively. The correctness of the condition easily follows from the rules of sequential programming.

Producer and Consumer problem

#Producer-and-Consumer-problem

We consider the classical Producer/Consumer problem for exhibiting individual progress and the multi-bond. i.e., multi-program.

Here in variable is used to record the number of portions produced and added to the buffer by Producer.

Similarly out variable is used to record the number of portions taken from the buffer by Consumer.

Buffer has a finite capacity C, its invariant can be C ≥ in - out ≥ 0.

This invariant is equivalent to, C+out ≥ in ∧ out ≥ in

#

Here the precondition P is in = 0 ∧ out = 0

Producer infinitely executes as long as it meets the condition, *[in:=in+1]

Consumer infinitely executes as long as it meets the condition *[out:=out+1]

System invariant of this problem is, C ≥ in - out ≥ 0 ≡ C+out ≥ in ∧ out ≥ in

13-2.jpg

#

In this scenario, individual progress is guaranteed whenever out ultimate solutions are free from total deadlock, no matter what that solution will look like.

14.jpg

Safe Sluice Algorithm

#Safe-Sluice-Algorithm
  • It is a two component mutual exclusion algorithm
  • Total deadlock occurs.
  • Here,
    • ncs is the non critical section
    • cs is the critical section
    • x.p and x.q are variables

Precondition: ¬x.p ∧ ¬x.q

1
2
3
4
5
6
Component Q:
    * [ ncs.q
    x.q:=true
    if ¬x.q → skip
    cs.q
    x.q:=false ]
  • Desired outcome is a component that terminates its non critical section is guaranteed to enter its critical section within a finite number of steps in a multi-program.
  • In this algorithm, the guards are too strong to meet the above requirement.

Peterson's Two-Component Mutual Exclusion Algorithm

#Peterson's-Two-Component-Mutual-Exclusion-Algorithm
  • This algorithm follows Safe Sluice algorithm but it weakens the guard to avoid the Total deadlock.
  • For weakening the guard, a new variable v is introduced

Precondition: ¬x.p ∧ ¬x.q

1
2
3
4
5
6
Component Q:
    * [ ncs.q
    x.q,v:=true,q
    if ¬x.q ∨ v = p → skip
    cs.q
    x.q:=false ]
  • Weakening the guards potentially violates the safety of the algorithm.
  • This algorithm has individual starvation problem.

Re-inventing the great idea

#Re-inventing-the-great-idea

Let us consider the variable r to keep track of the number of components engaged in the critical section. Hence in terms of Mutual exclusion, the required Invariant is 1 ≥ r.

Precondition: r=0

Component i:

* [ ncs.i if 0 ≥ r → r:=r+1 cs.i r:=r-1 ]

Invariant: 1 ≥ r

Introducing variable s to be coupled to r by system invariant s=1-r. This helps to eliminate r and the solution is in terms of s.

Precondition: s=1

Component i:

* [ ncs.i if s ≥ 1 → s:=s-1 cs.i s:=s+1 ]

Invariant: s ≥ 0

#

Here, the guarded statement if s ≥ 1 → s:=s-1 and assignment s:=s+1 should be atomic together. Hence we use P() and V() statements

P(s): if s ≥ 1 → s:=s-1

V(s): s:=s+1

With P() and V() we can rewrite the above algorithm as follows,

Precondition: s=1

Component i:

* [ ncs.i P(s) cs.i V(s) ]

Invariant: s ≥ 0

Advantages of using P() and V():

#Advantages-of-using-P()-and-V():
  • helps to achieve "strong fairness requirement"
  • helps to get rid of individual starvation
  • it is the synchronization primitives, helps to eliminate "busy form of waiting"

Phase synchronization for two machines

#Phase-synchronization-for-two-machines
  • It is the construction of correct multi-programs.
  • Addresses the performance of the program.

Precondition: d=1

1
2
3
4
5
6
7
Component B:
    * [ { assert d ≥ 1 }
        T
        d:=d-1
        if d ≥ 1 → skip
        { assert d ≥ 1 }
      ]

Invariant:d ≥ 0 ∧ 2 ≥ d

There is no deadlock in this example.