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

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

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