Tutorial: Proving termination and liveness Byron Cook Microsoft Research and Queen Mary, Univ. of London 1 Introduction

2 Introduction 3 Introduction 4

Introduction 5 Introduction 6

Introduction 7 Introduction 8 Introduction

9 Outline Basics Refinement-based termination proving Variance analysis Recent and future work

Conclusion 10 Outline Basics Refinement-based termination proving Variance analysis Recent and future work

Conclusion 11 Well-founded relations = 12

Well-founded relations = 13 Well-founded relations =

14 Well-founded relations 15 Well-founded relations

16 Well-founded relations 17 Well-founded relations 18

Well-founded relations 19 Well-founded relations 20

Well-founded relations 21 Termination proof rules 22 Termination proof rules

23 Termination proof rules 24 Termination proof rules

25 Termination proof rules 26 Termination proof rules 27

Termination proof rules 28 Termination proof rules 29

Termination proof rules 30 Termination proof rule 31 Termination proof rule

32 Termination proof rule 33 Termination proof rule

34 Termination proof rule 35 Termination proof rule 36

Termination proof rule 37 Termination proof rule 38

Termination proof rule 39 Termination proof rule ; ); );

y 1 1 >= >= x y x

( ( e e = m : u um

s s x s a as 40

Termination proof rule ; ); ); y 1 1

>= >= x y x ( ( e e

= m : u um s s x s

a as 41 Termination proof rule ; );

); y 1 1 >= >= x y

x ( ( e e = m : u

um s s x s a as 42

Termination proof rule ; ); ); y 1 1

>= >= x y x ( ( e

e = m : u um s s x

s a as 43 Termination proof rule ;

); ); y 1 1 >= >= x

y x ( ( e e = m :

u um s s x s a as

44 Termination proof rule 45 Termination proof rule 46

Outline Basics Refinement-based termination proving Variance analysis Recent and future work Conclusion 47

Outline Basics Refinement-based termination proving Variance analysis Recent and future work Conclusion 48

Outline Basics Refinement-based termination proving Variance analysis Recent and future work Conclusion 49

Refinement Strategy: Start with empty termination argument Iteratively weaken and re-check termination argument Weaken using linear rank function synthesis Advantages:

Can use existing safety property checking technology to check argument validity Finds complex termination arguments with only linear rank functions Leads to counterexamples Accurate Disadvantages: Very slow May not terminate (in several ways)

50 Refinement 51 Refinement

52 Refinement 53

Refinement 54 Refinement

55 Refinement 56 Refinement

57 Refinement 58 Refinement 59

Refinement 60 Refinement 61

Refinement 62 Refinement 63 Refinement

64 Refinement 65 Refinement

66 Refinement 67 Refinement 68

Refinement 69 Refinement 70

Refinement 71 Refinement 72 Refinement

73 Refinement copied = 0; . . . while(x

x =(!copied) f(x,y); { if g(&y,x); if (*) { } H[x] = x; H[y] = y; copied = 1;

} } else { assert(T1 || T2 || T3); } copied = 0; 74 Examples

75 Examples 76 Examples

77 Examples 78 Examples 79

Examples 80 Examples 81

Examples 82 Examples 83 Examples

84 The bad news 85 The bad news

86 The bad news 87 The bad news 88

The bad news 89 The bad news 90

The bad news 91 The bad news 92 The bad news

93 The bad news 94 The bad news

95 The bad news 96 More bad news 97

More bad news 98 More bad news 99

Outline Basics Refinement-based termination proving Variance analysis Recent and future work Conclusion 100

Outline Basics Refinement-based termination proving Variance analysis Recent and future work Conclusion 101

Outline Basics Refinement-based termination proving Variance analysis Recent and future work Conclusion 102

Variance analysis 103 Variance analysis 104 Variance analysis

Strategy: Use abstract interpretation techniques to compute (disjunctive) overapproximation Check that the parts of the disjunction are well founded Advantages: Can use existing abstract interpretation tools to compute overapproximation Always terminates Fast

Disadvantages: No counterexamples Less accurate than refinement-based approach Abstract domains (currently) not built for our application Widening can be too aggressive Redundant information kept 105

Variance analysis 106 Variance analysis 107 Variance analysis

108 Variance analysis 109 Variance analysis

110 Variance analysis 111 Variance analysis 112

Variance analysis 113 Variance analysis 114

Variance analysis 115 Variance analysis 116 Variance analysis

117 Variance analysis 1 2

3 118 Variance analysis 1 2

3 119 Variance analysis 1

2 3 120 Variance analysis 1

2 3 121 Variance analysis

1 2 3 122 Variance analysis

1 2 3 123

Variance analysis 1 2 3 124

Variance analysis 1 2.1 2

3 125 2.2 Variance analysis 1

0 2.1 2 3 126

2.2 Variance analysis 1 0 2.1

2 3 127 2.2

Variance analysis 1 0 2.1 2

3 128 2.2 Variance analysis 1

0 2.1 2 3 129

2.2 Variance analysis 1 0 2.1

2 3 130 2.2

Variance analysis 1 0 2.1 2

3 131 2.2 Variance analysis 1

0 2.1 2 3 132

2.2 Variance analysis 1 0 2.1

2 3 133 2.2

Variance analysis 1 0 2.1 2

3 134 2.2 Variance analysis 1

0 2.1 2 3 135

2.2 Variance analysis 1 0 2.1

2 3 136 2.2

Variance analysis 1 0 2.1 2

3 137 2.2 Variance analysis 1

0 2.1 2 3 138

2.2 Variance analysis 1 0

2.1 2 3 139

2.2 Variance analysis Strategy: Use abstract interpretation techniques to compute (disjunctive) overapproximation Check that the parts of the disjunction are well founded

Advantages: Can use existing abstract interpretation tools to compute overapproximation Always terminates Fast Disadvantages: No counterexamples Less accurate than refinement-based approach Abstract domains (currently) not built for our application

Widening can be too aggressive Redundant information kept 140 Variance analysis Strategy: Use abstract interpretation techniques to compute (disjunctive) overapproximation Check that the parts of the disjunction are well founded

Advantages: Can use existing abstract interpretation tools to compute overapproximation Always terminates Fast Disadvantages: No counterexamples Less accurate than refinement-based approach

Abstract domains (currently) not built for our application Widening can be too aggressive Redundant information kept 141 Termination proof rules 142

Termination proof rules 143 Termination proof rule 144 Termination proof rule

145 Termination proof rule 146 Outline

Basics Refinement-based termination proving Termination analysis Recent and future work Conclusion 147 Outline

Basics Refinement-based termination proving Termination analysis Recent and future work Conclusion 148 Recent and future work

Concurrency Proving thread-termination [PLDI08] Proving that non-blocking algorithms dont block [POPL09] Recursion Proving termination of recursive programs [Submitted] Synthesizing pre-conditions to termination Proving conditional termination [CAV08]

Termination for non-linear programs Proving termination by divergence [SEFM07] 149 Recent and future work Concurrency Proving thread-termination [PLDI08]

Proving that non-blocking algorithms dont block [POPL09] Recursion Proving termination of recursive programs [Submitted] Synthesizing pre-conditions to termination Proving conditional termination [CAV08] Termination for non-linear programs

Proving termination by divergence [SEFM07] 150 Proving that non-blocking algorithms dont block 151 Proving that non-blocking algorithms dont block

152 Proving that non-blocking algorithms dont block 153 Proving that non-blocking algorithms dont block 154

Recent and future work Concurrency Proving thread-termination [PLDI08] Proving that non-blocking algorithms dont block [POPL09] Recursion Proving termination of recursive programs [Submitted]

Synthesizing pre-conditions to termination Proving conditional termination [CAV08] Termination for non-linear programs Proving termination by divergence [SEFM07] 155 Recent and future work

Concurrency Proving thread-termination [PLDI08] Proving that non-blocking algorithms dont block [POPL09] Recursion Proving termination of recursive programs [Submitted] Synthesizing pre-conditions to termination

Proving conditional termination [CAV08] Termination for non-linear programs Proving termination by divergence [SEFM07] 156 Recent and future work Concurrency

Proving thread-termination [PLDI08] Proving that non-blocking algorithms dont block [POPL09] Recursion Proving termination of recursive programs [Submitted] Synthesizing pre-conditions to termination Proving conditional termination [CAV08]

Termination for non-linear programs Proving termination by divergence [SEFM07] 157 Recent and future work Concurrency Proving thread-termination [PLDI08] Proving that non-blocking algorithms dont block [POPL09]

Recursion Proving termination of recursive programs [Submitted] Synthesizing pre-conditions to termination Proving conditional termination [CAV08] Termination for non-linear programs Proving termination by divergence [SEFM07]

158 Recent and future work Concurrency Proving thread-termination [PLDI08] Proving that non-blocking algorithms dont block [POPL09] Recursion

Proving termination of recursive programs [Submitted] Synthesizing pre-conditions to termination Proving conditional termination [CAV08] Termination for non-linear programs Proving termination by divergence [SEFM07] 159

Synthesizing preconditions to termination Automatic termination/liveness proving is now a reality Advanced termination/liveness tools now supporting

Concurrency, Pointers, Heap, Recursion, Omega-regular properties, Counterexample-generation, etc

Tools: 160 Terminator (currently being transferred into Windows SDV product)

ARMC (Andreys publicly available version) Polyrank (from Bradley, Manna, Sipma) T2 (in development for my book and CMU course) Motivation Automatic termination/liveness proving is now a reality Advanced termination/liveness tools now supporting

Concurrency, Pointers, Heap,

Recursion, Omega-regular properties, Counterexample-generation, etc Tools:

161 Terminator (currently being transferred into Windows SDV product) ARMC (Andreys publicly available version) Polyrank (from Bradley, Manna, Sipma) T2 (in development for my book and CMU course) Automatic termination/liveness proving is now a reality

Advanced termination/liveness tools now supporting

Concurrency, Pointers, Heap, Recursion, Omega-regular properties, Counterexample-generation, etc Tools:

162 Terminator (currently being transferred into Windows SDV product) ARMC (Andreys publicly available version) Polyrank (from Bradley, Manna, Sipma)

T2 (in development for my book and CMU course) Recent and future work Concurrency Proving thread-termination [PLDI08] Proving that non-blocking algorithms dont block [POPL09] Recursion

Proving termination of recursive programs [Submitted] Synthesizing pre-conditions to termination Proving conditional termination [CAV08] Termination for non-linear programs Proving termination by divergence [SEFM07] 163

Recent and future work Concurrency Proving thread-termination [PLDI08] Proving that non-blocking algorithms dont block [POPL09] Recursion Proving termination of recursive programs [Submitted]

Synthesizing pre-conditions to termination Proving conditional termination [CAV08] Termination for non-linear programs Proving termination by divergence [SEFM07] 164 Recent and future work

Proving termination inductively Podelski & Rybalchenko [LICS04] Ranking abstractions [ESOP08] Liveness properties (fair termination) Proving that software eventually does something good [POPL07b] Better support for heap-manipulating programs

Automatic termination proofs for programs with shapeshifting heaps [CAV06] 165 Recent and future work Proving termination inductively Podelski & Rybalchenko [LICS04] Ranking abstractions [ESOP08]

Liveness properties (fair termination) Proving that software eventually does something good [POPL07b] Better support for heap-manipulating programs Automatic termination proofs for programs with shapeshifting heaps [CAV06] 166 Induction

167 Induction 168 Recent and future work

Proving termination inductively Podelski & Rybalchenko [LICS04] Ranking abstractions [ESOP08] Liveness properties (fair termination) Proving that software eventually does something good [POPL07b] Better support for heap-manipulating programs

Automatic termination proofs for programs with shapeshifting heaps [CAV06] 169 Recent and future work 170 Recent and future work

171 Recent and future work 172 Recent and future work Proving termination inductively

Podelski & Rybalchenko [LICS04] Ranking abstractions [ESOP08] Liveness properties (fair termination) Proving that software eventually does something good [POPL07b] Better support for heap-manipulating programs Automatic termination proofs for programs with shapeshifting heaps [CAV06]

173 Recent and future work Proving termination inductively Podelski & Rybalchenko [LICS04] Ranking abstractions [ESOP08] Liveness properties (fair termination)

Proving that software eventually does something good [POPL07b] Better support for heap-manipulating programs Automatic termination proofs for programs with shapeshifting heaps [CAV06] 174 Recent and future work Separation logic based shape analysis for systems code:

Scalable shape analysis for systems code [CAV08] Proving termination Support forinductively concurrency: Thread-modular shape analysis [PLDI07b] Podelski & Rybalchenko [POPL07a]

Local reasoning for storable locks and threads [APLAS07] Ranking abstractions Shape analysis for complex data structures: [ESOP08] Shape analysis for composite data structures [CAV07] Producing arithmetic abstractions of programs with heap: Arithmetic strengthening for shape analysis [SAS07]

Automatic termination proofs for programs with shape-shifting heaps [CAV06] Liveness properties (fair termination) Proving that software eventually does something good [POPL07b] Better support for heap-manipulating programs Automatic termination proofs for programs with shapeshifting heaps [CAV06]

175 Recent and future work Separation logic based shape analysis for systems code: Scalable shape analysis for systems code [CAV08] acquire(); Variance analysis, and inductive techniques

Support for concurrency: while() { } shape analysis [PLDI07b] Variance analysesThread-modular from invariance analyses [POPL07a] Local reasoning for storable locks and threads [APLAS07]

release(); Ranking abstractions Shape analysis for complex data structures: [ESOP08] Shape analysis for composite data structures [CAV07]

Producing arithmetic abstractions of programs with heap: Arithmetic strengthening for shape analysis [SAS07] Automatic termination proofs for programs with shape-shifting heaps [CAV06] Liveness properties (fair termination) Proving that software eventually does something good [POPL07b]

Better support for heap-manipulating programs Automatic termination proofs for programs with shapeshifting heaps [CAV06] 176 Recent and future work Separation logic based shape analysis for systems code: Scalable shape analysis for systems code [CAV08] acquire(); Variance analysis,

and inductive techniques Support for concurrency: while() { } shape analysis [PLDI07b] Variance analysesThread-modular from invariance

analyses [POPL07a] Local reasoning for storable locks and threads [APLAS07] release(); Ranking abstractions Shape analysis for complex data structures: [ESOP08]

Shape analysis for composite data structures [CAV07] Producing arithmetic abstractions of programs with heap: Arithmetic strengthening for shape analysis [SAS07] Automatic termination proofs for programs with shape-shifting heaps [CAV06] Liveness properties (fair termination) Proving that software eventually does something good

[POPL07b] Better support for heap-manipulating programs Automatic termination proofs for programs with shapeshifting heaps [CAV06] 177 Experimental results 178

Experimental results 179 Experimental results 180

Experimental results 181 Experimental results 182 Experimental results

183 Experimental results 184 Experimental results

185 Experimental results 186 Experimental results 187

Experimental results 188 Experimental results 189

Experimental results 190 Experimental results 191 Experimental results

192 Experimental results 193 Recent and future work

Current frontiers:

194 Bitvectors + unbounded numbers Scalability Precision

Finding inductive termination arguments Non-linear systems Counterexamples/non-termination Concurrency Programs with data structures Finding better pre-conditions Programs with higher-order functions Collatz program (a.k.a. the 3n+1 problem)

Outline Basics Refinement-based termination proving Termination analysis Recent and future work Conclusion 195

Outline Basics Refinement-based termination proving Termination analysis Recent and future work Conclusion 196

Conclusion Trend: use of modular termination arguments Easier to construct Harder to prove valid, but techniques are available New termination proving strategies Refinement-based termination proving Variance analysis using invariance analysis Size-change, etc

Result: termination proving is not impossible after all Next step: Judgment day Scalability, precision, concurrency, heap, commercial viability 197 Conclusion

See research.microsoft.com/~bycook for pointers to papers Write to [email protected] Thank you for your attention 198