• 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.

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 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}

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

Its annotation is

1
  {x ≥ 0}  x=x-1  {x ≥ 0}

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 is for locally establishing a component's initital condition.
• It is used for stand alone sequential programs.

Rule for Local correctness:

{Q} S {P}

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.

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. On a parallel execution it can be represented as, Annotation for this mutual exclusion could be shown as follows, Concurrent execution can be shown as, • 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)
• Value of B oscillates a finite number of times and then becomes stably false
• Value of B oscillates a finite number of times and then becomes stably true.

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.

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.

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.

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.

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.

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 #

In this scenario, individual progress is guaranteed whenever out ultimate solutions are free from total deadlock, no matter what that solution will look like. • It is a two component mutual exclusion algorithm
• 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.

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

• 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"
• 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.