Proving Termination of Program Loops

(1)

Proving Termination of Program Loops

Ashutosh K. Gupta

Supervisor: Andrey Rybalchenko Responsible Professor : Thomas A. Henzinger

June 11, 2007

(2)

Abstract

Proving termination of program loops is needed in software verification. Rank- ing functions provide an effective tool for this task, which can be efficiently automated for several classes of ranking functions.

In this work, we improve the existing algorithms for the synthesis of linear ranking function, which are widely used in practice, in two ways. Firstly, we increase their applicability by devising heuristic that provide ranking functions that are particularly useful for software verification. Secondly, we propose an extension ton-depth linear ranking functions, which are strictly more powerful than the (plain) linear ranking functions.

The abilities of ranking function synthesis algorithm are inherently limited by the class of generated functions: a failure to compute a ranking function does not imply that the subject program does not terminate. To address this limitation, we propose an algorithm for proving non-termination of program loops. This algorithm can be applied if no ranking function can be synthesized.

We implemented the proposed algorithms and experimentally evaluated their practical applicability for (dis-)proving termination.

(3)

Introduction

Guaranteed termination of program loops is a desirable property to be verified.

In many time critical systems it is very much necessary for termination of certain loops.

Ranking functions provide an effective tool for this task, which can be efficiently automated for several classes of ranking functions. There has been suggestions of other methods, such as Tiwari showed that termination of a class of single-path loops with linear guards and assignment is decidable, proving a decision procedure via constructive proofs [8]. Ranking function corresponding to a loop not only shows the termination property but also it describes an abstract behavior of the loop. This information can be used by higher verification tools which try to prove properties over whole program.

In this work, we improve the existing algorithms for the synthesis of linear ranking function [6], which are widely used in practice, in two ways. Firstly, we increase their applicability by devising heuristic that provide ranking functions that are particularly useful for software verification. Secondly, we propose an extension ton-depth linear ranking functions, which are strictly more powerful than the (plain) linear ranking functions.

The abilities of ranking function synthesis algorithm are inherently limited by the class of generated functions: a failure to compute a ranking function does not imply that the subject program does not terminate. To address this limitation, we propose an algorithm for proving non-termination of program loops. This algorithm can be applied if no ranking function can be synthesized.

We implemented the proposed algorithms and experimentally evaluated their practical applicability for (dis-)proving termination.

This master thesis is organized as following. In second chapter, preliminaries and background theorems related to thesis are presented. In third chapter, previous work over which this work is based are discussed. In forth chapter, technique to improve performance of rankfinder¹is described. In fifth chapter, definition of n-depth ranking function is introduced and algorithm for synthesis of n-depth linear ranking function is presented. In chapter six, a method to detect non termination of loop is explained. And it is also discussed that how can this method be improved. In seventh chapter, future work and conclusion are discussed.

1rankfinder is a tool base on work in [6] and used in other verification tools.

(5)

Chapter 2

Preliminaries

In this chapter, we define programs and provide useful facts from the theory of Linear Programming.

2.1 Program and Loops

We assume a finite vector of variables xwhich we call program variables. We define aprogram stateto be a real-valued assignment to the program variablesx.

A program over the variablesxis given abstractly by a binary relation over the program state, which we call transition relation R(x, x^′). We assume that the transition relation is represented by an assertion over the program variables x and their primed versions x^′, which relate the values of the program variables before and after taking the transition.

In this work, we restrict our attention to transition relations of particular form, which is motivated by the applications in software verification [5]. We assume that the transition relation represents a single while loop that contains a set of update statements executed simultaneously. Furthermore, we assume that the loop condition and the updates are represented using linear inequalities over the program variables. We refer to this kind of loops as “linear while loops”.

Definition 2.1 (Linear While Loop). A linear while loop L : (x, A, A^′, a) over|x|program variables xrepresents the transition relation

(AA^′) µ x

x^′

¶

≤a,

whereA andA^′ are|x| ×m matrices andaism-dimensional vector.

Definition 2.2 (Well-founded relation). A transition relation R(x, x^′) is well-founded if and only if there is no infinite sequence of x0, x1, . . . such that R(xn−1, xn)for everyn∈N.

Example 2.1. RelationR(x, x^′) ={x≥0∧x^′=x−1}is well-founded because non infinite sequence of x can satisfy the relation .And, RelationR(x, x^′) ={x≥ 0∧x^′ =x+ 1} is non-well-founded because infinite sequences 1,2, . . . satisfy the relation.

(6)

Non-well-founded relation is equivalent to non-termination of the corresponding loop.

Note that our definition of linear while loop uses only non-strict inequalities.

We shall observe that some of the results are sensitive to this limitation of not using strict inequality (see Chapter 6). The transition relation of the loop is given by a conjunction of linear constraints. In particular, this implies that the loop condition cannot contain disequalities, e.g. x6= 0. In some cases, a loop that does not satisfy the conditions of our definition can be represented as a linear loop by using approximations. For example, non linear update expressions can be approximated to linear ones, andx6= 0 can be approximated byx≥1.

Example 2.2. We assume the loop statement (in C notation):

while (x >= 0) { x = x+1;

}

We translate it to the linear while loop L: ({x}, A, A^′, a) such that:

A=





−1

−1 1



 A^′=



 0 1

−1



 a=



 0 1

−1





2.2 Facts from Linear Programming Theory

We present some useful results from the theory of Linear Programming.

Theorem 2.1 (Farkas’ Lemma [7]). Consider the following system of linear inequality over real variablesx=hx1, ..., xdi:

S:







A11x1+· · ·+A1dxd≤b1

... ... ... An1x1+· · ·+Andxd≤b1







If S is satisfiable then it implies a linear inequalityr1x1+· · ·+rdxd≤c if and only if there exist real numbersλ1, . . . , λn ≥0 such that

r1=

n

X

i=1

λiAi1 . . . rd =

n

X

i=1

λiAid c≥

n

X

i=1

λibi.

Example 2.3. Let us consider{y−x≤1∧x≤2}system of inequalities.Farkas lemma states any linear inequality that satisfy this system can be reproduced by positive linear combination of inequalities of the system.

As we can observe from the Figure 2.1,y≤4 andx+y≤5 satisfy the given system. So, combination for above inequalities are,

x+y≤5 = 1∗(y−x≤1) + 2∗(x≤2)

y≤4 = 1∗(y−x≤1) + 2∗(x≤2) + 1∗(0≤1) Observe that 0≤1 is part of any conjunctive constraint system.

(7)

6

-

¡¡¡¡¡¡¡¡¡¡

.........................

R ¾

@@

@@@

@@

@@@

@@

@@ @

. .. .. . .. .. .. .. .. .. .. . .. .. .. .. .. ..ª

?

@@

@

@@

y − x ≤ 1

x + y ≤

5 x ≤ 2

y ≤ 4

Figure 2.1: Shaded region is the set that satisfy the system of inequality{y−x≤ 1∧x≤2}. y ≤4 andx+y≤5 also satisfy this set as they are positive linear combination of system inequalities.

Theorem 2.2 (Decomposition theorem for polyhedra). A setP of vectors in Euclidean space is a polyhedron, if and only ifP =Q+C for some polytope Qand some polyhedral coneC.

Example 2.4. Let us consider a polyhedron P = {(x, y)|y −2x ≤ 0∧y− x ≥ −1∧x+y ≥ 3}. The polyhedron can be broken into polytope Q = convex.hull((1,2),(2,1)) and polyhedral coneC={(x, y)|y−2x≤0∧y−x≥0}

such thatP =Q+C.

¢¢¢¢¢¢¢

- 6

@@@¡¡¡¡¡¡¡

- 6

¡¡¡¡¡¡¡¡¡¡¡

¢¢¢¢¢¢¢¢¢¢¢

- 6

@@@

(c) Polytope (b) Polyhedral cone

(a) Polyhedron

Figure 2.2: (a) P = {(x, y)|y−2x ≤ 0∧y−x ≥ −1∧x+y ≥ 3} (b) C = {(x, y)|y−2x≤0∧y−x≥0}(c)Q= convex.hull((1,2),(2,1))

2.3 Ranking Functions and Relations

Definition 2.3 (Ranking Function). A ranking function for a transition relation R(x, x^′)is a function r(x)for someδ <0 such that,

∀(x, x^′)R(x, x^′)→r(x)≥0∧r(x^′)−r(x)≤δ

Definition 2.4 (Ranking Relation). Given a ranking function r, we define

(8)

the ranking relation forr to be a binary relation such overxandx^′ such that r(x)≥0∧r(x^′)−r(x)≤δ .

Definition 2.5 (Linear Ranking Function). A linear Ranking function for a linear arithmetic simple while loopL: (x, A, A^′, a)is vectorrfor someδ0<0 such that,

rx≥δ1

rx^′−rx≤δ0

satisfy the Loop.

Example 2.5. Lets consider the loopx≥0∧y= 1∧y^′ =y∧x^′ =x−y then r=£

1 0 ¤

will be a linear ranking function of the loop because





 x≥0 y= 1 y^′=y x^′ =x−y







|=







£ 1 0 ¤

· x y

¸

≥0

£ 1 0 ¤

· x^′ y^′

¸

−£

1 0 ¤

· x y

¸

≤ −1





 .

If a linear while loop has a linear ranking function then it will certainly terminates.

(9)

Chapter 3

Earlier works

Finding a ranking function is one of the dominant methods of proving termination of a program loop. There has been suggestions of other methods such as Tiwari showed that termination of a class of single-path loops with linear guards and assignment is decidable,proving a decision procedure via constructive proofs [8]. Ranking function corresponding to a loop not only shows the termination property but also it describes an abstract behavior of the loop.

This information can be used by higher verification tools which try to prove properties over whole program.

In [6], a complete method for the synthesis of linear ranking function is proposed. In [1], definition of lexicographic linear ranking function is presented.

This kind of ranking function covers the multi-path linear program loops. The extension of this formulation for polynomial programs is presented in [2].In [2, 3],The idea of eventually negative is described.

3.1 Algorithm for finding linear Ranking func- tion

Algorithm 1Synthesis of linear Ranking function forL: (x, A, A^′, a)

1: if exists rational-valuedλ1and λ0 such that λ1, λ0≥0

λ1A^′ = 0 (λ1−λ0)A= 0 λ0(A+A^′) = 0 λ0a <0

then

2: return “Program Terminates”

3: else

4: return “Linear ranking function does not Exists”

5: end if

6: return

In [6], an algorithm for synthesis of linear ranking function of linear while loop is presented. Solution space of a given loop L: (x, A, A^′, a) can satisfy a

(10)

ranking function{rx≥δ1∧rx^′−rx≤δ0}only if these two inequalities can be generated using farkas lemma.So,

λ0(AA^′) µ x

x^′

¶

≤λ0a ≡ rx^′ ≤rx+δ0

λ1(AA^′) µ x

x^′

¶

≤λ1a ≡ 0≤rx+δ1

where, λ1, λ0>0 δ0<0 Simplifying above equations,

λ0A=−r λ0A^′=r λ0a=δ0 λ0≥0 δ0<0 λ1A=−r λ1A^′= 0 λ1a=δ1 λ1≥0

Above equations induce Algorithm 1. This algorithm creates the following linear constraint system

λ0A+λ0A^′ = 0;

(λ1−λ0)A^′= 0;

λ1A^′ = 0;λ0a <0; λ0≥0; λ1>0;

and if the constraint system has a solution then there will exist a linear ranking function which will satisfy the loop constraints.

3.2 Lexicographic Ranking Function

In [1], the idea of Lexicographic Linear Ranking Function is introduced. This kind of ranking function is capable of handling multi path loops.

Definition 3.1 (Multipath linear program loop). A Multi-path linear program loop M L : hx,Li is disjunction of a set L of linear while loop over x.

where,

L:hL0, . . . , Lri Li : (x, Ai, A^′_i, ai)

If next state satisfy any one of the linear while loop Li then loop can make an step to that state.

A linear ranking function can also show termination of a multi-path linear program loopM L:hx,Li. For this one have to show that a single linear ranking function can satisfy eachLi’s. Availability of such a solution is very less likely.

Following formulation of ranking function can improve the proving capabilities.

Definition 3.2 (Lexicographic linear ranking function). A lexicographic linear ranking function for a multi-path linear loop M L : hx,Li is n-tuple of linear expressionshr^T₁x, . . . , rn^Txisuch that for someδ >0 and for eachL∈L, for somei∈ {1, . . . , n},

L|=r^Tix≥0;

L|=r^Tix−r^Ti x^′ ≥δ;

forj < i L|=rj^Tx−r^Tjx^′≥0.

In this definition lexicographic term is used because the order of expressions hr^T₁x, . . . , r^T_nxiis important.

If a multi-path linear loop satisfy a Lexicographic linear ranking function then it terminates.

(11)

3.3 Eventually Negative Function

In [2, 3] the idea of Eventually Negative Function is presented. Its definition is presented with a difference such that it fits with our definition of loops.

Definition 3.3 (Eventually Negative by S ⊂ L). Given multi-path loop M L:hx,Li overx, an expressionE(x) is eventually negative byS ⊂L(⊂L), for S 6= ∅, if either case Negative or case Eventually Negative holds in following conditions.

(Negative)E(x)is bounded: L|=E(x)≤ −δ for someδ >0

(Eventually Negative) For eachL∈L, one of the following conditions holds:

(Nonincreasing)L∈L−S andLdoes not increase E(x) : {(L∈L−S)∧(L|=E(x^′)−E(x)≤0)}

(Eventually Decreasing)L does not increase E(x) by mode than some eventually negative F(x):

{(L|=E(x^′)−E(x)≤F(x))∧(F(x)is eventually negative by{L} ⊂L)}

For caseEventually Negative to hold, recursion must have finite depth.

Intuitively, transitions inS should make progress towards decreasingE(x), while transition inLshould not interfere counter productively. Eventually negative expressions is able to show termination. Following Definition integrates Lexicographic ranking function and eventually negative expressions.

Definition 3.4 (Lexicographic Polyranking Function). The n-tuple of functionshr1(x), . . . , rl(x)iis a lexicographic Polyranking Function of multi-path loop M L:hx,Liif for some π:L→ {1, . . . , n},

(Bounded) forL∈L, L|=rπ(L)(x)≥0;

(Ranking) ri(x)is eventually negative by{L:π(L) =i} ⊂ {L:π(L)≥i}.

If a multi-path loopM L: hx,Lihas a lexicographic polyranking function, then it always terminates.

Synthesis methods of these kind of ranking functions are discussed in [2, 3, 1].

In short, they all assume a template of ranking function and try to find satisfying parameters for the ranking function using Farks lemma.

In this masters thesis, n-depth linear Ranking function uses similar idea as eventually negative functions.

(12)

Chapter 4

Maximizing Ranking Relations

The existing algorithms for the synthesis of linear ranking functions can compute a set of possible answers, wheres the result is arbitrarily selected by the applied constraint solver. In many applications naturally impose a preference ordering on the ranking functions. In this chapter, we address the preferences determined by the application of ranking functions for proving termination via transition invariants [5]

4.1 Preference for Maximization

One application of ranking synthesis is to compute ranking relations for transition relations defined by sequences of program statements in general programs with complex control flow, which may include nested loops, branching statements, etc. The goal of this process lies in finding a finite set of ranking relations that ‘covers’ all possible sequences of statements through the control-flow graph of the program. To achieve this goal is may be desirable to compute largest possible ranking relations, which cover as many sequences as possible.

Example 4.1. We assume that the input sequence of statements represents the transition relationR such that

R=x≤1∧x≤100∧x^′ =x+ 1 .

For this relation we can choose a ranking relation x≤1∧x^′ ≥x+ 1. Another option to consider is the relation x≤100∧x^′ ≥x+ 1. We observer that the latter strictly contains the first one, and hence, is preferred for our ‘covering’

application described above.

4.2 Maximization of Ranking Relation

Linear ranking function rx ≥ δ0 ∧rx^′−rx ≤ δ1∧δ1 < 0, for a given loop L: (x, A, A^′, a) can be computed by solving following equations as discussed in

(13)

section 3.1:

r=−λ0A=λ1A^′=−λ1A;

λ0A^′= 0; δ1=λ1a=−1;

δ0=λ0a; λ0≥0; λ1≥0;

As we observed in Example 4.1 choosing a solution for which δ0 is maximum produces slower or bigger ranking function. This technique is illustrated in following example.

Example 4.2 (Biggest Solution). Lets take the loop L = {x ≥ 0 ∧ x ≥ 10 ∧ x^′ ≤x−1}

A=





−1



 A^′=



 0 0 1



 a=



 0

−10

−1





Lets assume λ0 = hλ0,1, λ0,2, λ0,3iand λ1 = hλ1,1, λ1,2, λ1,3i. It will generate following set of equations.

r=λ0,1+λ0,2+λ0,3=λ1,3=λ1,1+λ1,2+λ1,3; λ0,3= 0; 10λ1,2+λ1,3= 1;

λ0,1≥0; λ0,2≥0; λ0,3≥0;

λ1,1≥0; λ1,2≥0; λ1,3≥0;

max(−10λ0,2−λ0,3)

And above equations will produce following solution space, λ0,3=λ1,1=λ1,2= 0; λ1,3= 1

λ0,1+λ0,2= 1; max(−10λ0,2); λ0,1≥0; λ0,2≥0;

On maximizing the solution,

λ0,2=λ0,3=λ1,1=λ1,2= 0; λ0,1=λ1,3= 1 so ranking function will be,{x≥0 ∧ x^′≤x−1}.

Example 4.3 (Maximum doesn’t exist). Now, lets consider the loop{x= 0∧x^′≥1∧x^′≤100}.

A=





 1

−1 0 0





 A^′ =





 0 0

−1 1





 a=





 0 0

−1 100







Lets assume λ0 = hλ0,1, λ0,2, λ0,3, λ0,4i and λ1 = hλ1,1, λ1,2, λ1,3, λ1,4i, then equations for computing ranking function are,

r=−λ0,1+λ0,2=−λ1,3+λ1,4=−λ1,1+λ1,2

−λ0,3+λ0,4= 0; −λ1,3+ 100λ1,4=−1;

λ0,1≥0; λ0,2≥0; λ0,3≥0; λ0,4≥0;

λ1,1≥0; λ1,2≥0; λ1,3≥0; λ1,4≥0;

max(−λ0,3+ 100λ0,4)

(14)

There exist solution of above constraint system but maximum of the term

−λ0,3+ 100λ0,4 doesn’t exist. In this case we can choose any of the available solution. So, solution of the above equations is

λ0,1=λ1,1=λ1,3= 1;

λ0,2=λ0,3=λ0,4=λ1,2=λ1,4= 0;

If maximum doesn’t exist for the loop then any solution from the solution set can be accepted. It is to be noted that appearance of many zero can cause failure of existence of the maximizing term. It has been observed that there are fair chances that maximum doesn’t exist for the given loop.

In following section we will present a heuristic technique by which we can improve the possibility of existence of maximum of maximizing term.

4.3 Existence of maximum

As we observed in the last example that it is not necessary that maximum exist for the given constraint system for the above maximization term. In that case, any of the available solution can be chosen. Criteria of maximization can also be modified such that maximum will exist in the solution set for that criteria.

First we have to identify in which case maximum doesn’t exist. The following theorem shows general condition when no maximum exists.

Theorem 4.1 (Existence of Maxima). For a given Matrix A , vector b and row-vector c:

{max(λb)|λA=c, λ≥0} exist if and only if∀µ: (µA= 0, µ≥0)→µb≤0 Proof. Solution set of constraint systemλA=c∧λ≥0 will be a polyhedron. By Decomposition theorem for polyhedral(See Theorem 2.2), λ∈this polyhedron can be decomposed in two vectors λ0and λc such thatλ0∈a polyhedral cone P andλc∈a polytope Q.

λ=λ0+λc; λ0∈P&λc∈Q

where,polyhedral P ={λ0|λ0A= 0, λ0 ≥0} and polytope Q can be generated by a finite set of vectors.

So,max(λb) =max(λ0b+λcb)

Asλ0andλcare independently chosen from set P and Q therefore max operator can be distributed over ’+’.

max(λb) =max(λ0b) +max(λcb)

We know that polytope Q is a finite size object in space. So, maximum of linear function λcb will certainly exist. Other termλ0b is an element of infinite size object P. So,max(λb) exists≡max(λ0b) exists.

First we assume,∃λ0∈P :λ0b >0.

By definition of P,λ0∈P →2λ0∈P.

⇒2λ0b > λ0b

⇒ ∀(λ0)[λ0∈P, λ0b >0]→ ∃(λ^′₀)[λ^′₀∈P, λ^′₀b > λ0b]

Therefore,max(λ0b) doesn’t exist.

Now we assume,∀λ0∈P :λ0b≤0 By definition of P, 0∈P

(15)

⇒max(λ0b) = 0

Therefore,max(λ0b) exist.

⇒(∀µ)∈(µA= 0, µ≥0) :µb≤0≡ {max(λb)|λA= 0, λ≥0}exists

⇒(∀µ)∈(µA= 0, µ≥0) :µb≤0≡ {max(λb)|λA=c, λ≥0}exists

From the above formulation of the problem, following is the set of equations,

¡ λ0 λ1 ¢

µ A^′ A 0 0 0 A^′ A+A^′ a

¶

=¡

0 0 0 −1 ¢ max

µ

¡ λ0 λ1 ¢ µ a

0

¶¶

Existence of maximum translats to,

∀(λ0, λ1) µ

¡ λ0 λ1 ¢

µ A^′ A 0 0 0 A^′ A+A^′ a

¶

= 0→λ0a≤0

¶

Using above observation, maximization criteria can be modified such that possibility of existence of maximum increases. Lets assumeλ0=hλ0,1. . . λ0,ni and a = ha1. . . ani. The heuristic used is that in maximization criteria we replace ai to 0 if Ai( i^th row of A) contains only zero entries. So, objective function for maximazation will become

n

X

i=1

λ0,iaici where,

½ ci = 0 ifAi= 0 ci = 1 ifAi6= 0

If rowAi is zero and a solution of equationλ0A^′= 0, λ0,iai>0 exists then there is no other constraint which can keep λ0,iai’s value in bound. So, if we drop λ0,iai term in maximization criteria then possibility of finding maximum increases.

Example 4.4. We consider the loopx= 0∧x^′ ≥1∧x^′ ≤100. If we modify maximization critaria of Example 4.3 according to new technique then we obtain objective function which is equal to zero.

n

X

i=1

λ0,iaici=λ0,1∗0∗1 +λ0,2∗0∗1 +λ0,3∗ −1∗0 +λ0,4∗100∗0 = 0

Now this term is empty and any of the solution of solution space will be accepted.

This heuristic is not the best possible way of choosing maximization criteria.

It can be investigated in future to find better heuristics .

(16)

Chapter 5

n-Depth linear ranking function

There exist terminating simple while loops for which no linear ranking function exist. In this section, we propose an extension of linear ranking functions that can handle a strictly larger set of loops.

5.1 Extending the definition of linear ranking function

For example, we consider the loop x≥0∧x^′ =x+y∧y^′=y−1. The value of variable y will eventually go negative. After that x will start decreasing.

Finally, x will be negative after finite steps and condition x ≥ 0 will not be satisfied and loop will terminate. But for this loop there exist no linear ranking function.

Termination of the above example can be proved using following extension in definition of linear ranking function. This extension of definition goes along the idea of eventually negative functions described in [2, 3].

Definition 5.1 (n-Depth linear ranking function). A n-depth linear Rank- ing function for a linear arithmetic simple while loop L: (x, A, A^′, a) is n-tuple of vectors hr1, . . . , rnifor some δ0<0,

r1x^′ ≤r1x+δ0

rix^′≤rix+ri−1x+δi−1; ∀1< i≤n 0≤rnx+δn.

For n = 1, it is a linear ranking function.

Theorem 5.1. A given loop L : (x, A, A^′, a) is terminating if there exist a n-depth ranking function which satisfy the loop.

Proof. According to the first inequality of the ranking function evaluation ofr1x will decrease strictly with lower bound in decrementδ0 andr1x <−δ1 will be true after finite number of executions of loop. Ini^thinequality, ifri−1x+δi−1<0 thenrixwill also start decreasing strictly with lower bound in decrement . By

(17)

induction these two conditions imply,rnxwill decrease strictly with lower bound in decrement.So, after finite no of execution of looprnx <−δnwill be true. So, Loop will terminate because it can’t satisfy the ranking function anymore.

n-depth linear Ranking function have n+ 1 linear inequalities which must be implied by the transition relation of the loop. We assume that the equations of the ranking function are produced by multiplying n+1-tuple of row vectors hλ0, . . . , λniwith loop constraints.

λ0(AA^′) µ x

x^′

¶

≤λ0a ≡ r1x^′ ≤r1x+δ0

λi−1(AA^′) µ x

x^′

¶

≤λi−1a ≡ rix^′≤rix+ri−1x+δi−1; ∀1< i≤n λn(AA^′)

µ x x^′

¶

≤λna ≡ 0≤rnx+δn

where, λj>0 ∀0≤j≤n After simplifying the equations,

λ0A=−r1; λ0A^′=r1; λ0a=δ0<0 λi−1A=−ri−ri−1; λi−1A^′=ri; λi−1a=δi−1

λnA=−rn; λnA^′ = 0; λna=δn

Without loosing any possibility of finding a solution we can fix value of δ0=−1. So, Finally,

For, X =−(A+A^′); Y =A^′ λ0X = 0; λ0a=δ0=−1;λ0≥0;

λiX =λi−1Y =ri;λi≥0; ∀0< i≤n λnY = 0;λn≥0.

If a solution of the set of equations exists then n-depth linear ranking function exists.

Translation to reachability problem: Solution of above equations can be seen as following transition relation overλ,

init: λX = 0∧λa=−1∧λ≥0;

update: λ^′X =λY ∧λ^′≥0

If state space of above transition relation is reachable to λ = 0 then a ranking function exist. It is interesting to observe that problem of finding ranking function canbe translated to a reachability problem.

5.2 Algorithm for synthesis of n-depth linear rank- ing function

Above analysis induces Algorithm 2 for finding ranking function. This algorithm uses following function of a constraint solver.

solve constraints(constraint system, variable list) →vector of values: This function solves current constraint system passed to constraint solver

(18)

Algorithm 2Synthesis of n-depth Ranking function forL: (x, A, A^′, a)

1: X← −(A+A^′)

2: Y ←A^′

3: Λ← {λ0}

4: Φ←λ0X = 0∧λ0a=−1∧λ0≥0

5: if Φ6=∅then

6: fori= 1 to MAXDEPTHdo

7: Λ = Λ∪ {λi}

8: Φ←Φ∧λiX=λi−1Y ∧λi ≥0

9: if Φ6=∅ then

10: if (Φ∧λiY = 0)6=∅ then

11: Φ←Φ∧λiY = 0

12: return solve constraints(Λ,Φ)

13: end if

14: else

15: print “n-depth ranking function does not exist”

16: return

17: end if

18: end for

19: else

20: print “n-depth ranking function does not exist”

21: return

22: end if

23: print “Failed to find n-depth ranking function”

24: return

(19)

and returns values of the variables for one of the solution of the constraint system. If there are more then one solution of the constraint system then it all depends on the solver that which solution it returns.

This algorithm tries to find a n-depth ranking function. First values of X and Y matrices are initialized. It also initialize constraint system Φ←λ0X = 0∧λ0a = −1∧λ0 ≥ 0 and variable list Λ ← λ0. If Φ is ∅ then no n-depth linear ranking function exist and algorithm terminates. Otherwise, Algorithm enters in a loop which iterates i from 1 to MAXDEPTH. In each run of the loop, constraint λiX =λi−1Y ∧λi ≥0 is added to Φ with conjunction and also new set of variablesλiare added to Λ. If at any of the iterations Φ becomes∅then no n-depth linear ranking function exist and algorithm terminates. Further in the iteration, if (Φ∧λiY = 0) =∅ then loop continue to next iteration otherwise a ranking function is found and loop terminates and returns the values or variable set Λ.

Example 5.1. Lets take the example {x≥0∧x^′ =x+y∧y^′=y−1} again.

Lets take set of variable (x, y) then,

A=







−1 0

−1 −1

1 1

0 −1

0 1





 A^′=







0 0

1 0

−1 0

0 1

0 −1





 a=





 0 0 0

−1 1







⇒ X =−(A+A^′) =







1 0

0 1

0 −1

0 0







Y =A^′=







0 0

1 0

−1 0

0 1

0 −1







The algorithm runs and finds solution in 2 steps, λ0= ( 0 0 0 1 0 ) λ1= ( 0 1 0 0 0 ) λ2= ( 1 0 0 0 0 )







r1= ( 0 1 ) r2= ( 1 0 )

So, the 2-depth linear ranking function is {0 ≤x∧x^′ ≤x+y∧y^′ ≤y−1}.

Hence loop will terminate.

5.3 Termination of the algorithm 2

Loop in the algorithm terminates ati=MAXDEPTH, MAXDEPTH is a heuristically chosen number for depth of search. The fair choice can be the number of rows inA matrix. Each constraint of ranking function is linear combination of constraints of original loop. So, ranking function cannot have more linearly in- dependent constraints then original loop. It gives the intuition that if a ranking function exist it must be found with in depth ofrank(AA^′). For more simple bound we can choose number of rows ofA.

A proof of this bound on the depth of ranking function has been tried but couldn’t complete it. see in Appendix A for the discussion.

(20)

Chapter 6

Non-well-founded Relation

Other side of the problem will be proving that the given loop will not terminate. If we fail to show that the loop terminats does not imply that it is non terminating. It may be possible that the loop always terminats, but the given methodology of ranking functions is fail to detect it. So if we want to deduce that given loop will not-terminate then it needs a separate proof.

6.1 Condition for non well founded relation

Our interest is to form a condition for a transition relation such that if the relation satisfies the condition then it is non well founded. This condition should be easily checkable by an algorithm.

A condition for non-well-founded Relation. We propose the following condition for for testing non-well-founded relation. Transition relationR(x, x^′) is non-well-founded if there exist set of satesGsuch that,

∃(x, x^′)G(x)∧R(x, x^′) and

∀(x, x^′)G(x)∧R(x, x^′)|=G(x^′) and

∀(x, x^′)∃(x^′′)G(x)∧R(x, x^′)|=R(x^′, x^′′)

The first expression implies that there exist at least one state xin set G which has a successer within R. The second condition implies that all the states in set G cannot be related with relation R to another state out side set G. The third condition implies that if an state in G has a successer then this successer will also have at least one successor.

6.2 Proving non-well-founded relation

It is difficult to create an algorithm with∃operator in the conditions. One can remove ∃ operator by assuming x^′′ as a function of xand x^′′. If we assume , x^′′=E(x, x^′) +ethen,

∃(G)

½ ∃(x, x^′)G(x)∧R(x, x^′)

∀(x, x^′)G(x)∧R(x, x^′)∧(x^′′=E(x, x^′) +e)|=G(x^′)∧R(x^′, x^′′)

(21)

Problem of proving non-well-foundedness will reduce to the existence of constraints G(x) andx^′′ =E(x, x^′) +e. For given loop L : (x, A, A^′, a), theG is assumed as a conjection of linear constraints, and E can be assumed to be a linear expression overxandx^′:

G(x) ≡Gx≤g x^′′=E(x, x^′) +e ≡¡

E E^′ −I ¢



 x x^′ x^′′



=−e So, non-well-founded condition will be,∃(G, g, E, E^′, e)

µ G 0 A A^′

¶ µ x x^′

¶

≤ µ g

a

¶

6= ∅







G 0 0

A A^′ 0

E E^′ −I

−E −E^′ I









 x x^′ x^′′



≤





 g a

−e e







|= ¡

0 G 0 ¢



 x x^′ x^′′



≤g







G 0 0

A A^′ 0

E E^′ −I

−E −E^′ I









 x x^′ x^′′



≤





 g a

−e e







|= ¡

0 A A^′ ¢



 x x^′ x^′′



≤a

Solving above conditions by using Farkas lemma and any constraint solver can prove that loop is non-well-founded. It is to be noted here that not only values of Gand g are missing but also sizes are unknown. We assume a template for G(x, x^′) or a number of rows of matrix G. Using farkas lemma and a constraint solver to check any value ofG, g, E, E andeexist for the loopL.

The above constraint system is similar to the constraint system appears in invariant generation problem [4]. So, already developed invariant generation solver is used to solve above constraint system. We create a constraint system with unknownG, g, E, Eandeand pass it to an invariant generator. It returns a valid set of values if it succeeds to find a solution. In the current implementation Gis a single linear inequality. Otherwise invariant generator takes long time to produce result.

Example 6.1. Lets take the loop {x≥0∧x^′=x+y∧y^′=y+ 1}. wherex andy are loop variables then , we have

R(x, y, x^′, y^′) ={x≥0∧x^′=x+y∧y^′=y+ 1}

∃(x^′, y^′)R(x, y, x^′, y^′) ={x≥0}

∃(x, y)R(x, y, x^′, y^′) ={x^′−y^′+ 1≥0}

⇒ ∃(x, y)R(x, y, x^′, y^′)*∃(x^′′, y^′′)R(x^′, y^′, x^′′, y^′′) This expression is equivalent to,¹

⇒ ¬∀(x, y, x^′, y^′)∃(x^′′, y^′′)(R(x, y, x^′, y^′)|=R(x^′, y^′, x^′′, y^′′))

Observe that without any guarded command G(x), R(x, y, x^′, y^′) can’t satisfy the non-well-founded relation definition. The logic formula equivalence ¹helps to visualize the analysis as shown in Figure 6.1.

1Note that:∀(x^′)∃(x)R(x, x^′)|=∃(x^′′)R(x^′, x^′′)≡ ∀(x, x^′)∃(x^′′)(R(x, x^′)|=R(x^′, x^′′)) see Appendix C

(22)

6

@@

@@@

@@

-

@@

@

@@

@@@

................................. 6

-

.................................

@@@

@@

@

@@

@@@

@@

¡¡

¡

¡¡

x

^′

y

^′

y

^′

x

^′

(a) (b)

Figure 6.1: (a) ∃(x^′′, y^′′)R(x^′, y^′, x^′′, y^′′) is shown by solid lines and

∃(x, y)R(x, y, x^′, y^′) is shown by dash lines. By figure its clear that ∃(x, y)R(x, y, x^′, y^′) * ∃(x^′′, y^′′)R(x^′, y^′, x^′′, y^′′) (b)Similarly shown

∃(x, y)G(x, y)∧R(x, y, x^′, y^′) and ∃(x^′′, y^′′)G(x^′, y^′)∧R(x^′, y^′, x^′′, y^′′) regions.

Now,∃(x, y)G(x, y)∧R(x, y, x^′, y^′)⊆ ∃(x^′′, y^′′)G(x^′, y^′)∧R(x^′, y^′, x^′′, y^′′)

Using the proposed method to findG(x, y), our system gives following solution,

G≡ {y≥0}

E≡ {x^′′=x^′+y^′∧y^′′=y^′+ 1}

Now,

∃(x^′, y^′)G(x, y)∧R(x, y, x^′, y^′) ={x≥0∧y≥0}

∃(x, y)G(x, y)∧R(x, y, x^′, y^′) ={x^′−y^′+ 1≥0∧y^′≥1}

⇒ ∃(x, y)G(x, y)∧R(x, y, x^′, y^′)⊆ ∃(x^′′, y^′′)G(x^′, y^′)∧R(x^′, y^′, x^′′, y^′′) We can observe in the Figure 6.1, that now G(x)∧R(x, y, x^′, y^′) satisfy the non-well-founded condition.

⇒ ∀(x, y, x^′, y^′)(∃(x^′′, y^′′)G(x, y)∧R(x, y, x^′, y^′)|=G(x^′, y^′)∧R(x^′, y^′, x^′′, y^′′)) Hence loop is non terminating.

6.3 Understanding Non-well-founded Relation

The above condition of non-well-founded relation is an intuitive condition but one can formulate other weakened and strengthened conditions. Consider the following conditions.

(23)

(1) ∃(G)







∀(x, x^′)G(x)∧R(x, x^′)|=G(x^′)

∃(x)G(x)

∀(x)∃(x^′)G(x)|=R(x, x^′)

(2) ∃(G)







∀(x, x^′)G(x)∧R(x, x^′)|=G(x^′)

∃(x, x^′)G(x)∧R(x, x^′)

∀(x, x^′)∃(x^′′)G(x)∧R(x, x^′)|=R(x^′, x^′′)

(3) ∃(G)







∀(x, x^′)G(x)∧R(x, x^′)|=G(x^′)

∃(x, x^′, x^′′)G(x)∧R(x, x^′)∧R(x^′, x^′′)

∀(x, x^′, x^′′)∃(x^′′′)G(x)∧R(x, x^′)∧R(x^′, x^′′)|=R(x^′′, x^′′′) .

All of the above conditions are sufficient to prove non well founded relation.

First condition is the strongest. The second and third conditions are weaker and weaker. If G and R satisfy first condition then they will also satisfy second condition. Second condition is the original condition we presented above. We can serialize the conditions above to a sequence.

Now, Lets assume following series of conditions forn∈N,

Condn(G, R) =







∀(x0, x1)G(x0)∧R(x0, x1)|=G(x1)

∃(x0, x1, . . . , xn)G(x0)∧(Vn−1

i=0 R(xi, xi+1))

∀(x0, x1, . . . , xn)∃(xn+1)G(x0)∧(Vn−1

i=0 R(xi, xi+1))|=R(xn, xn+1) .

Lemma 6.1. A binary relation R is non well founded if ∃(G, n)Condn(G, R).

Proof. Lets assumenandGexist for relationRsuch thatCondn(G, R) is true.

Form first and second conditions ofCondn(G, R) there exists atleast a sequence of states of lengthr+ 1 such that,

{x0, x1, . . . , xr: (R(xi−1, xi)∀(i)1≤i≤r) and (G(xi)∀(i)0≤i≤r)}

forr≥n.

So,G(xr−n)∧(

r−1

^

i=r−n

R(xi, xi+1)) is true.

From third condition ofCondn(G, R),∃(xr+1)R(xr, xr+1).

Therefore, there exists a sequence of states of lengthr+ 2 such that {x0, x1, . . . , xr: (R(xi−1, xi)∀(i)1≤i≤r) and (G(xi)∀(i)0≤i≤r)}

By induction, There exist a infinite length of states which satisfy the relation R. Hence relation is non-well-founded.

Lemma 6.2 (Hierarchy of conditions). For a given binary relation R and G,Condn(G, R)|=Condn+1(G, R).

Proof. Lets assumeCondn(G, R) is true forGandR,

The second and third condition of theCondn(G, R) imply∃(xn+1)R(xn, xn+1)

⇒ ∃(x0, x1, . . . , xn+1)G(x0)∧(Vn

i=0R(xi, xi+1))

(24)

⇒ ∃(x1, x1, . . . , xn+1)G(x1)∧(Vn−1

i=1 R(xi, xi+1))⇒ ∃(xn+2)xn+2

⇒ ∀(x0, x1, . . . , xn+1)∃(xn+2)G(x0)∧(Vn

i=0R(xi, xi+1))|=R(xn+1, xn+2)

⇒

Condn+1(G, R) =







∀(x0, x1)G(x0)∧R(x0, x1)|=G(x1)

∃(x0, x1, . . . , xn+1)G(x0)∧(Vn

i=0R(xi, xi+1))

∀(x0, x1, . . . , xn+1)∃(xn+2)G(x0)∧(Vn

i=0R(xi, xi+1))|=R(xn+1, xn+2) .

This analysis indicates the first approach we used for finding non-well- founded relation can be improved. In next section we will discuss properties induced by the Linear Constraint system. This analysis is not complete but it seems this can lead us to a simple and complete algorithm.

6.4 Interesting properties of binary relation con- structed by Linear Constraints

If relation R is defined by Linear constraints then certain properties of linear space can be useful to detect non-well-founded Relation. Here, we describe these properties.

Definition 6.1 (Relational Space). Relational space is a vector space formed by (x, x^′) wherex, x^′ ∈R^d.

⇒R(x, x^′)⊆Relational Space

Definition 6.2 (Finite relation). An binary relationR(x, x^′)is a finite relation if it is defined by linear constraints over(x, x^′)and set formed in relational space due to these constraints is a polytope.

Definition 6.3 (Infinite relation). An binary relationR(x, x^′) is a infinite relation if it is defined by linear constraints over (x, x^′) and set formed in relational space due to these constraints is infinite(a polyhedron with non empty polyhedral component).

Definition 6.4 (E space). E={(x, x^′)|x=x^′} x, x^′∈R^d

Theorem 6.1 (Existence of dividing hyperplane). Given a relation R there exist a(2d−1)dimensional hyperplaneH in relational space that contains E, andR∧H =∅if and only if R∧E=∅.

Proof. Lets first show sufficient condition, (E⊂H)∧(R∧H =∅)|=R∧E=∅

For necessary condition, Let R=

½µ x x^′

¶

|(AA^′) µ x

x^′

¶

≤a

¾ and,

E=

½µ x x^′

¶

|

µ I −I

−I I

¶ µ x x^′

¶

≤ µ 0

0

¶¾

(25)

Then,

R∧E=





 µ x

x^′

¶

|





A A^′ I −I

−I I



 µ x

x^′

¶

≤



 a 0 0









 As,R∧E=∅

⇒ ∃([λ α1α2]≥0)







[λ α1α2]





A A^′ I −I

−I I



= 0 λa=−1





 After simplifying,

λA+α1I−α2I=λA^′−α1I+α2I= 0 λA=−α1I+α2I; λA^′ =α1I−α2I λA=−λA^′

Lets Assume,c=λA By Farkas Lemma,

⇒(x, x^′)∈R|=cx−cx^′ ≤ −1

⇒(x, x^′)∈R|=cx−cx^′ <0 AsE⊂ {(x, x^′)|cx−cx^′ = 0}, So, H ={(x, x^′)|cx−cx^′= 0}

Theorem 6.2. For a given finite relation R, ∃(x)(x, x)∈ R ≡R is non-well- founded.

Proof. For necessary condition,∃(x)(x, x)∈Rthen relation contains a self loop and it can have an infinite sequence of same state. So, It is not-well-founded.

For sufficient condition, Lets Assume,

∀(x)(x, x)∈/R≡R∧E=∅ From previous theorem,

∃(c)(x, x^′)∈R|=cx−cx^′≤ −1

Now,max(cx) exists in setRbecauseRis finite object in relational space.Lets assume,

M =max(cx) (x, x^′)∈R|=cx≤M

(x, x^′)∈R|= (cx≤M)∧(cx+ 1≤cx^′)

Above condition is a ranking function for relation R therefore relation can’t have infinite sequence. So, It will be well-founded relation.

Now we are presenting conjecture which we think is true but couldn’t prove in limited time.

Definition 6.5 (Self projecting cone). A self projecting cone C(x, x^′) is polyhedral cone in relational space(x, x^′)if,

∃(x)C(x, x^′)⊆ ∃(x^′′)C(x^′, x^′′)

Conjecture 6.1. A relation R is non-well-founded relation if and only if there exist a self projecting cone C(⊆R) and size of generator vector set of cone C is bounded by 2d, wheredis number of variables.

If this conjuncture holds then the algorithm for proving non-termination for linear while loop is complete.

(26)

Chapter 7

Conclusion and Future work

In this masters thesis, we presented two improvement in synthesis of ranking function for linear while loop. First improvement is maximizing for the biggest ranking function. It is found that not for all the linear while loop this maximum of the objective function exist. A heuristic is proposed to increase the possibility of existence of maximum. This heuristic is implemented and tested with other system and it improved the performance. Second, a formulation of n-depth linear ranking function is proposed which is capable of proving termination for bigger subset of linear while loop compared to (plain) linear ranking function. An algorithm for the synthesis of n-depth linear ranking function is also presented. This algorithm is implemented also implemented with our system. We also presented a method of proving non termination of linear while loop. This method is also implemented. This method can be used for proving non-termination when system fails to detect termination. It is also shown that this method is weak and can be improved.

7.1 Future work

Heuristic used in maximization of linear ranking function can be improved.

It may be possible to find another maximization objective function for which existence of maximum is certain and it solves the objective of earlier maximization technique. Algorithm 2 for the synthesis of n-depth linear ranking function terminates on a heuristically chosen bound. A proof for its bounded termination can be tried. In Appendix A its incomplete prove is described. As discussed in Section 6.4, the conjuncture 6.1 implies a complete algorithm for non-termination of linear while loop. Proof of this conjuncture will be tried.

(27)

Appendix A

Termination of Algorithm 2

Algorithm 2 terminates on a heuristically chosen bound. If the algorithm failed to find any ranking function in the given bound it doesn’t imply that a ranking function does not exist. Here is an incomplete proof which can possibly prove the termination of algorithm. Consider following transition relation.

init: λX = 0∧λa=−1∧λ≥0;

update: λ^′X =λY ∧λ^′≥0

Follwing conjecture holds for above transition relation then bound on the depth of then-ranking function exists.

Conjecture A.1 (Bound on the depth of the ranking function). For given matrix X and Y of n rows, if above transition relation is reachable to λ= 0 then there exist a path of size n exist which reaches toλ= 0.

Proof. Proof is not complete. Here we try to explain how it might be proved?

We have to show that any path reachable to λ= 0 which is longer than n can be reduced to smaller path with same final state.

Lets assume a path of size n+2 hλ0. . . λn+1ithen λ0X= 0; λ0a <0;λ0≥0;

λiX =λi−1Y =ri;λi≥0; ∀0< i≤n+ 1 As, ri ∈ Rⁿ → (∃j)[rj = Pj−1

i=1ciri; 0 < j ≤ n+ 1] (It needs a separate proof)

wlog, we can assumern+1=Pn i=1ciri

let k be highest index for whichck6= 0, Now, consider λ^′_i= (Pi

j=0ck−i+jλj) 0≤i < k

This new sequence ofλ^′_iwill be a valid path of the above atom andλn+1X =λ^′_kY If we assume, λ^′_i ≥ 0 then a shorter path is possible which is at least 1 step smaller. Hence proved.

Incompleteness of the proof ⇒λ^′_i≥0

(28)

Appendix B

Bug in Sictus CLPQ

During implementation of Rankfinder following bug is found.

?- {A=B,C=1+D,D>=0},sup(A-B,Max,[A,B,C,D],Res).

Res = [0,0,0,-1]

yes.

check that value ofD is -1 and in constraint systemD≥0 is passed.

Following workaround is used in using Sictus CPLQ

?- {A=B,C=1+D,D>=0},sup(A-B,Max),{A-B = Max}, find_val([A,B,C,D]).

A = 0 B = 0 C = 1 D = 0 yes.

First Compute the max of maximization expression without computing ac- tual values of variables then put maximization expression equal to computed maximum value. After this find the values of variables usingfind val

Proving Termination of Program Loops