model-checking, partial-order reductions

Computer aided verification

Lecture 4:

Algorithmic aspects of LTL

model-checking, partial-order reductions

Sławomir Lasota University of Warsaw

Algorithm

M  φ ?

(i) M 7→ AM

(ii) ¬φ 7→ A¬φ (never claim) ( not φ 7→ Aφ 7→ ¯Aφ ) (iii) Lω(AM) ∩ Lω(A¬φ) = ∅ ? ( not Lω(AM) ⊆ Lω(Aφ) )

Lω(AM × A¬φ) = ∅ ? yes −→ M  φ

no −→ ¬(M  φ), counterexample = a path in M

// 7654 0123 ,, 7654 0123 '&%$ !"#FED ABC

(i) M 7→ A ^M

 

{p, q}

?>=< 89:;

** ?>=< 89:;

jj 

{p}

?>=<

89:;

YY

{q}

7→

 ?>=<

89:; 7654 0123

{p,q}



{p}

?>=<

89:; 7654 0123

{p}

%% ?>=< 89:; 7654 0123

ee

{q}

 ?>=<

89:; 7654 0123

MM

Algorithm

M  φ ?

(i) M 7→ AM

(ii) ¬φ 7→ A¬φ (never claim) ( not φ 7→ Aφ 7→ ¯Aφ ) (iii) Lω(AM) ∩ Lω(A¬φ) = ∅ ? ( not Lω(AM) ⊆ Lω(Aφ) )

Lω(AM × A¬φ) = ∅ ? yes −→ M  φ

no −→ ¬(M  φ), counterexample = a path in M

// 7654 0123 ,, 7654 0123 '&%$ !"#FED ABC

(iii) L ^ω (A) 6= ∅?

Traversal of a graph:

[Clarke, Grumberg, Peled 2000]

(iii) L ^ω (A) 6= ∅?

Traversal of a graph:

[Clarke, Grumberg, Peled 2000]

// 7654 0123 ++ 7654 0123 '&%$ !"#FED XX ABC

On the fly verification

for each successsor si of s ^{do . . .}

?>=< 89:;

~~}} }} }} }} }

A A A A A A A A A

?>=<

89:;

?>=< 89:;

Reachability: F bad state

For reachability it is enough to use DFS or BFS

[Holzmann,Peled,Yannakakis 1996]

// 7654 0123 ,, 7654 0123 '&%$ !"#

Nested DFS

[Holzmann,Peled,Yannakakis 1996]

// 7654 0123 ,, 7654 0123 '&%$ !"#FED XX ABC

Proof of correctness

Assume an acceping state p with a cycle not detected by ndfs(p). Let p – the first such state.

Proof of correctness

Assume an acceping state p with a cycle not detected by ndfs(p). Let p – the first such state.

Let r – the first state inspected by ndfs(p) that is on a p-cycle and for which {r,1} in Statespace.

Proof of correctness

Assume an acceping state p with a cycle not detected by ndfs(p). Let p – the first such state.

Let r – the first state inspected by ndfs(p) that is on a p-cycle and for which {r,1} in Statespace.

Let p’ – the accepting state such that r visited by ndfs(p’).

. . .

// GFED @ABC ?>=< 89:;

%%

?

++

?>=<

89:;

gg

. . .

// GFED @ABC ?>=< 89:;

%% ?>=< 89:;

gg

GFED

@ABC ?>=< 89:;

OO

GFED

@ABC ?>=< 89:;

OO

Partial-order reductions?

(1) On the fly verification: ^{for each successsor} si of s ^{do . . .}

Partial-order reductions?

(1) On the fly verification: ^{for each successsor} si of s ^{do . . .}

(2) Partial-order reductions: for each selected successsor si of s ^{do . . .}

selected depends on the DFS stack !

Partial-order reductions?

(1) On the fly verification: ^{for each successsor} si of s ^{do . . .}

(2) Partial-order reductions: for each selected successsor si of s ^{do . . .}

selected depends on the DFS stack !

dfs: . . .

 ?>=<

89:;

 ~~

?>=<

89:;

?>=< 89:; 7654 0123

99 ?>=< 89:;

ll

Partial-order reductions?

(1) On the fly verification: ^{for each successsor} si of s ^{do . . .}

(2) Partial-order reductions: for each selected successsor si of s ^{do . . .}

selected depends on the DFS stack !

dfs: . . .

 ?>=<

89:;

 ~~

?>=<

89:;

?>=< 89:; 7654 0123

99 ?>=< 89:;

ll

nfds: . . .

 ?>=<

89:;

 }}{{ {{ {{ {{ {{

B B B B B B B B B

?>=<

89:;

?>=< 89:; 7654 0123

99 ?>=< 89:;

ll

Partial-order reductions?

(1) On the fly verification: ^{for each successsor} si of s ^{do . . .}

(2) Partial-order reductions: for each selected successsor si of s ^{do . . .}

selected depends on the DFS stack !

dfs: . . .

 ?>=<

89:;

 ~~

?>=<

89:;

?>=< 89:; 7654 0123

99 ?>=< 89:;

ll

nfds: . . .

 ?>=<

89:;

 }}{{ {{ {{ {{ {{

B B B B B B B B B

?>=<

89:;

?>=< 89:; 7654 0123

99 ?>=< 89:;

ll

Solution: Report a cycle when a stack is hit in ndfs.

Nested DFS compatible with p.-o.red.

[Holzmann,Peled,Yannakakis 1996]

Nested DFS compatible with p.-o.red.

[Holzmann,Peled,Yannakakis 1996]

Question: Is nested DFS correct now?

np-cycles: FG ¬ progress

[Holzmann,Peled,Yannakakis 1996]

np-cycles: never claim

[Holzmann,Peled,Yannakakis 1996]

// 7654 0123 BCD

@GA 88

¬progress

// 7654 0123 '&%$ !"#FED ABC

XX

np-cycles: never claim

[Holzmann,Peled,Yannakakis 1996]

// 7654 0123 BCD

@GA 88

¬progress

// 7654 0123 '&%$ !"#FED ABC

XX

Question: What overhead is introduced, when the never claim is used?

Partial-order reductions

for each selected successsor si ofs ^{do . . .}

?>=< 89:;

~~ A A A A A A A A A

?>=<

89:;

?>=< 89:;

Motivation

Idea: exploit indpendence (concurrency) of transitions

F¬p

?>=<

89:;

α

}}

β

B !!B B B B B B B B GFED

@ABC

β

!!

?>=<

89:;

α

}}|| || || || | GFED

@ABC

Motivation

 /.-, ()*+

α1

~~}} }} }} }}

A A A A A A A A /.-,

()*+

α2

~~}} }} }} }}

A A A A A A

A A /.-, ()*+

α1

~~}} }} }} }}

A A A A A A A A /.-,

()*+

β1

A A A A A A

A A /.-, ()*+

α2

~~}} }} }} }}

A A A A A A

A A /.-, ()*+

α1

~~}} }} }} }}

/.-, ()*+

β2

A A A A A A

A A /.-, ()*+

α2

~~}} }} }} }}

/.-,

()*+

Motivation

 /.-, ()*+

β1

$ A A A A A A A A

A A A A A A A A

/.-, ()*+

α1

z }} }} }} }}

}} }} }} }}

/.-, ()*+

α2

z }} }} }} }}

}} }} }} }}

/.-, ()*+

β2

$ A A A A A A A A

A A A A A A A A

/.-,

()*+

Model

Def.: M = hS, Sinit,T, Li T – operations (transitions) for α ∈ T : enα ⊆ S, α : enα → S (determinism)

path: Π = s0 α0

−−→ s¹ −−→ s^{α1 2} −−→ . . .^α2 s0 = sinit

αi(si) = si+1

ens := {α | s ∈ enα} (α ∈ ens ⇐⇒ s ∈ enα)

Idea: ample_s ⊆ ens instead of ens in nested DFS ?

Cost-effectivity

Idea: ample_s ⊆ ens instead of ens in nested DFS ?

This makes sense, when:

– the result of verification is the same (correctness) – significantly less states visited

– time overhead reasonable (effectivity)

Correctness?

When may we ignore α ?

?>=< 89:;

α

}}

β

B !!B B B B B B B B GFED

@ABC

β

!!

?>=<

89:;

α

}}|| || || || | GFED

@ABC

Problem 1: Property may depend on state

GFED @ABC

Problem 2:

GFED @ABC

Stuttering

Def.: Π = s0 −→ s1 −→ s2 −→ . . . and Π^′ = s^′0 −→ s^′1 −→ s^′2 −→ . . . are stuttering equivalent, Π ≡ Π^′, if sequences

L(s0), L(s1), L(s2), . . . L(s^′0), L(s^′1), L(s^′2), . . . become identical after grouping is done:

Def.: M ≡ M^′ if and only if – ∀Π in M ∃Π^′ in M^′ Π ≡ Π^′ – ∀Π^′ in M^′ ∃Π in M Π ≡ Π^′

LTL _−X

LTL_−X = LTL without X

Thm: If φ ∈ LTL−X and Π ≡ Π^′, then Π  φ ⇐⇒ Π^′  φ Thm: If φ ∈ LTL−X and M ≡ M^′, then M  φ ⇐⇒ M^′  φ

Thm: LTL−X = FO≡( ≤ )

Correctness

M  partial-order reduction

// M ^′

M ≡ M ^′

Sufficient condition for correctness

(C0) ample_s = ∅ ⇐⇒ ens = ∅

(C1) . . .

(C2) . . .

(C3) . . .

Invisibility

Def.: α is invisible if L(s) = L(α(s)), ∀ s ∈ enα.

Example: If α invisible, then

?>=< 89:;

α

~~}} }} }} }} }

β

A A A A A A A A A

?>=<

89:;

β

A A A A A A A A

A ?>=< 89:;

~~}} }} }} }} }

?>=<

89:;

Sufficient condition for correctness

(C0) ample_s = ∅ ⇐⇒ ens = ∅

(C1) if ample_s 6= ens then every α ∈ ample_s is invisible

(C2) . . .

(C3) . . .

Idea: Instead of doing sth now, do it in future!

Correctness?

Problem 1: Property may depend on state

GFED @ABC

?>=<

89:;

α

}}

β

B !!B B B B B B B B GFED

@ABC

β

!!

?>=<

89:;

α

}}|| || || || | GFED

@ABC

Solved due to ^(C1) !

(C1) if ample_s 6= ens, then every α ∈ ample_s is invisible

Independence

Def.: Relation of independence I ⊆ T × T : – irreflexive and antisymmetric

– if αIβ, α ∈ ens, β ∈ ens, then (s ∈ enα ∩ enβ) – β(s) ∈ enα, α(s) ∈ enβ

– β(α(s)) = α(β(s))

?>=< 89:;

α

}}|| || || || |

β

B !!B B B B B B B B 7654

0123

β

D !!D D D D D D D

D

7654 0123

α

}}zz zz zz zz z 7654

D = T × T \ I (dependency)

0123

Independence

Example: Independent may be:

– 2 instructions of different processes operating on local variables

Independence

Example: Independent may be:

– 2 instructions of different processes operating on local variables

– 2 instructions of different processes that increment the same global variable

Independence

Example: Independent may be:

– 2 instructions of different processes operating on local variables

– 2 instructions of different processes that increment the same global variable – 2 instructions of different processes writing to/reading from different buffers

Independence

Example: Independent may be:

– 2 instructions of different processes operating on local variables

– 2 instructions of different processes that increment the same global variable – 2 instructions of different processes writing to/reading from different buffers – 2 instructions of different processes:

one writing to a buffer

the other one reading from the same buffer

Independence

Example: Independent may be:

– 2 instructions of different processes operating on local variables

– 2 instructions of different processes that increment the same global variable – 2 instructions of different processes writing to/reading from different buffers – 2 instructions of different processes:

one writing to a buffer

the other one reading from the same buffer

Question: Can 2 instructions of the same process be independent ?

Independence

Question: Let αIβ. Is it possible that

s ∈ enα \ enβ α(s) ∈ enβ ?

?>=< 89:;

α

}}|| || || || |

β

 7654 0123

β

D !!D D D D D D D

D

7654

0123

Independence

Question: Let αIβ. Is it possible that

s ∈ enα \ enβ α(s) ∈ enβ ?

?>=< 89:;

α

}}|| || || || |

β

 7654 0123

β

D !!D D D D D D D

D

7654 0123

Yes! E.g. asynchronous reading and writing from/to the same buffer by two different processes.

Sufficient condition for correctness

(C0) ample_s = ∅ ⇐⇒ ens = ∅

(C1) if ample_s 6= ens then every α ∈ ample_s is invisible

(C2) ? ens \ ample_s
I ample_s

(C3) . . .

Idea: Instead of doing sth now, do it in future!

(C2)

(C2) a transition dependent on some transition from ample_s

can not be enabled before some transition from ample_s is executed

(C2)

(C2) a transition dependent on some transition from ample_s

can not be enabled before some transition from ample_s is executed

(C2) for every path Π starting in s:

if α ∈ ample_s, β ∈ ample/ _s, αDβ then β does not appear in Π

before some transition from ample_s is executed

(C2)

Lemma: (C2) implies ens \ ample_s
I ample_s.

Proof: Let β ∈ ens \ ample_s, α ∈ ample_s, αDβ.

s −→^β β(s) −→ . . . contradiction with (C2) .

Correctness?

Problem 2:

?>=< 89:;

?>=<

89:;

α

}}zz zz zz

D !!D D D D D

?>=<

89:;

β

B B B B B

B

?>=< 89:;

~~}} }}

}}

A A A A A A

?>=<

89:;

GFED @ABC

e.g., let α ∈ ample_s,β ∈ ample/ _s

Correctness?

Problem 2:

?>=< 89:;

?>=<

89:;

α

}}zz zz zz

D !!D D D D D

?>=<

89:;

β

B B B B B

B

?>=< 89:;

~~}} }}

}}

A A A A A A

?>=<

89:;

GFED @ABC

e.g., let α ∈ ample_s,β ∈ ample/ _s

by (C2) applied to βγ . . ., we deduce γIα

Problems?

Problem 2:

?>=< 89:;

?>=<

89:;

α

}}zz zz zz

""D D D D D D

?>=<

89:;

β

B B B B B

B

?>=< 89:;

}}|| ||

||

A A A A A A

?>=<

89:;

γ

αIγ

GFED @ABC

~~

?>=<

89:;

e.g., let α ∈ ample_s,β ∈ ample/ _s

by (C2) applied to βγ . . ., we deduce γIα α invisible, thus ss1rr^′ ≡ ss²s^′2

Problems?

Problem 2^∞:

?>=< 89:;

?>=<

89:;

α

}}zz zz zz

""D D D D D D

?>=<

89:;

β

B B B B B

B

?>=< 89:;

}}|| ||

||

A A A A A A

?>=<

89:;

γ

αIγ

GFED @ABC

~~

γ^′

>

> >

> >

> >

?>=<

89:;

α invisible, thus ss1rr^′ . . . ≡ ss2s^′2 . . .

Problems?

Problem 2^∞:

?>=< 89:;

?>=<

89:;

α

}}zz zz zz

""D D D D D D

?>=<

89:;

β

B B B B B

B

?>=< 89:;

}}|| ||

||

A A A A A A

?>=<

89:;

γ

αIγ

GFED @ABC

~~

γ^′

>

> >

> >

> >

?>=<

89:;

α invisible, thus ss1rr^′ . . . ≡ ss2s^′2 . . .

Problem 2^∞ does not appear under weak fairness

Fairness

Def. (weak fairness): if α enabled from some point on then α eventually executed.

Corollary: for every reachable state s, if α ∈ ens then eventually some β will be executed such that αDβ.

/.-, ()*+

α

~~~~ ~~ ~~ ~~

β



...

@ @

@ @

@ @

@ @ ?>=< 89:;

α

}}zz zz zz

""D D D D D D

?>=<

89:;

β

B B B B B

B

?>=< 89:;

}}|| ||

||

A A A A A A

?>=<

89:;

γ

αIγ

GFED @ABC

~~

γ^′

>

> >

> >

> >

?>=<

89:;

Enough?

Are ^(C0) – ^(C2) sufficient?

Enough?

Are ^(C0) – ^(C2) sufficient?

No!

 

?>=<

89:;

β



7654 0123

α1

 GFED

@ABC

7654 0123

2

// 7654 0123

α3

``

Enough?

Are ^(C0) – ^(C2) sufficient?

No!

 

?>=<

89:;

β



7654 0123

α1

 GFED

@ABC

7654 0123

2

// 7654 0123

α3

``

(C3) we forbid cycles C such that ∃β ∀s ∈ C β ∈ ens \ ample_s

Sufficient condition for correctness

(C0) ample_s = ∅ ⇐⇒ ens = ∅

(C1) if ample_s 6= ens then every α ∈ ample_s is invisible

(C2) for every path Π starting in s:

if α ∈ ample_s, β ∈ ample/ _s, αDβ then β does not appear in Π

before some transition from ample_s is executed

(C3) we forbid cycles C such that ∃β ∀s ∈ C β ∈ ens \ ample_s

How to implement ^(C1) – ^(C3) ?

Sufficient condition for correctness

(C1) easy

(C2) hard, implemented in an approximate manner – an over-approximation of D is computed – condition (C2) is monotonic

– static analysis only

(C3) replaced by another condition which is easier but stronger:

(C3’) if ample_s 6= ens then ∀α ∈ ample_s α(s) /∈ stack

Implementation

Implementation decision:

ample_s = all transitions of some process i enabled in s

Implementation

Implementation decision:

ample_s = all transitions of some process i enabled in s

whenever

– they are independent from all operations of all other processes – no operation of any other process may enable

any other operation of process i

β enabling α (over-approximation)

– if β modifies pc so that α may be executed

– if Promela enabling condition for α depends on global variables, then any β that modifies these variables

– if α is reading from/writing to a buffer then any β that reads from/writes to this buffer

αDβ (over-approximation)

– α and β refer to the same global variable

and at least one of them modifies the variable

– α and β belong to the same process; synchronous communication is understood as belonging to both processes

– α and β write to/read from the same buffer

However reading from a buffer is independent from writing to the same buffer!

What remains independent?

Example:

Operations independent from all operations of other processes:

– operating on local variables

– reading from a buffer with xr flag set – writing to a bugger with xs flag set – test nempty(q) if xr flags is set for q – test nfull(q) if xs flag is set for q