WWW.DIS.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Thesis, dissertations, books
 
<< HOME
CONTACTS



Pages:   || 2 | 3 |

«Abstract. Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check is ...»

-- [ Page 1 ] --

Termination Analysis with

Compositional Transition Invariants

Daniel Kroening1, Natasha Sharygina2,4,

Aliaksei Tsitovich2, and Christoph M. Wintersteiger3

Oxford University, Computing Laboratory, UK

Formal Verification and Security Group, University of Lugano, Switzerland

Computer Systems Institute, ETH Zurich, Switzerland

School of Computer Science, Carnegie Mellon University, USA

Abstract. Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of ranking relations to prove program termination. We provide an experimental evaluation over a set of 87 Windows drivers, and demonstrate that our algorithm is often able to conclude termination by examining only a small fraction of the program. As a consequence, our algorithm is able to outperform known approaches by multiple orders of magnitude.

1 Introduction Automated termination analysis of systems code has advanced to a level that permits industrial application of termination provers. One possible way to obtain a formal argument for termination of a program is to rank all states of the program with natural numbers such that for any pair of consecutive states si, si+1 the rank is decreasing, i.e., rank(si+1 ) rank(si ). In other words, a program is terminating if there exists a ranking function for every program execution.

Substantial progress towards the applicability of procedures that compute ranking arguments to industrial code was achieved by an algorithm called Binary Reachability Analysis (BRA), proposed by Cook, Podelski, and Rybalchenko [1].

This approach combines detection of ranking functions for program paths with a procedure for checking safety properties, e.g., a Model Checker. The key idea of the algorithm is to encode an intermediate termination argument into a program annotated with an assertion, which is then passed to the safety checker. Any counterexample for the assertion produced by the safety checker contains a path that violates the intermediate termination argument. The counterexample path is then used to compute a better termination argument with the help of methods that discover ranking functions for program paths.

Supported by the Swiss National Science Foundation under grant no. 200020-122077, by EPSRC grant no. EP/G026254/1, by the EU FP7 STREP MOGENTES, and by the Tasso Foundation.

A broad range of experiments with different implementations have shown that the bottleneck of this approach is the safety check [1, 2]: Cook et al. [1] report more than 30 hoursof runtime for some of their benchmarks. The time for computing the ranking function for a given program path is insignificant in comparison. Part of the reason for the difficulty of the safety checks is their dual role: they ensure that a disjunctively composed termination argument is correct and they need to provide sufficiently deep counterexamples for the generation of further ranking arguments.

We propose a new algorithm for termination analysis that addresses these challenges as follows: 1) We use a light-weight criterion for termination based on compositionality of transition invariants. 2) Instead of using full counterexample paths, the algorithm applies the path ranking procedure directly to increasingly deep unwindings of the program until a suitable ranking argument is found. We prove soundness and completeness (for finite-state programs) of our approach and support it by an extensive evaluation on a large set of Windows device drivers. Our algorithm performs up to 3 orders of magnitude faster than BRA, as it avoids the bottleneck of safety checking in the iterative construction of a termination argument.

2 Background Preliminaries We define notation for programs and record some basic properties we require later on. Programs are modeled as transition systems.

Definition 1 (Transition System). A transition system (program) P is a three tuple S, I, R, where – S is a (possibly infinite) set of states, – I ⊆ S is the set of initial states, – R ⊆ S × S is the transition relation.

A computation of a transition system is a maximal sequence of states s0, s1,... such that s0 ∈ I and (si, si+1 ) ∈ R for all i ≥ 0. A program is terminating iff all computations of the program eventually reach a final state. The non-reflexive transitive closure of R is denoted by R+, and the reflexive transitive closure of R is denoted by R∗. The set of reachable states is R∗ (I).

Podelski and Rybalchenko [3] use Transition Invariants to prove termination

of programs:

Definition 2 (Transition Invariant [3]). A transition invariant T for program P = S, I, R is a superset of the transitive closure of R restricted to the reachable state space, i.e., R+ ∩ (R∗ (I) × R∗ (I)) ⊆ T.

A well-founded relation is a relation that does not contain infinite descending

chains. Podelski and Rybalchenko define a weaker notion as follows:

Definition 3 (Disjunctive Well-foundedness [3]). A relation T is disjunctively well-founded (d.wf.) if it is a finite union T = T1 ∪... ∪ Tn of well-founded (wf.) relations.

A program is terminating if it does not have infinite computations, and Podelski and Rybalchenko show that disjunctive well-foundedness is enough to prove





termination of a program:

Theorem 1 (Termination [3]). A program P is terminating iff there exists a d.wf. transition invariant for P.

The literature presents a broad range of methods to obtain transition invariants. Usually, this is accomplished via synthesis of ranking functions, which define well-founded ranking relations [2, 4–6]. We refer to such methods as ranking procedures.

Binary Reachability Analysis [1]. Theorem 1 gives rise to an algorithm for proving termination that constructs a d.wf. transition invariant in an incremental fashion. Initially, an empty termination argument is used, i.e., T0 = ∅. Then, a Model Checker is used to search the reachable state space for a counterexample to termination argument Ti. If there is none, termination is proven. Otherwise, let π be the counterexample path. The counterexample may be genuine, i.e., demonstrate a prefix of a non-terminating computation. Otherwise, a wellfounded relation T that includes π is constructed (via a ranking procedure).

Finally, the current termination argument is updated, i.e., Ti+1 = Ti ∪ T and the process is repeated.

This principle has been put to the test in various tools, most notably in Terminator [1], ARMC [7], and in an experimental version of SatAbs [2].

3 Compositional Termination Analysis The literature contains a broad range of reports of experiments with multiple implementations that indicate that the bottleneck of Binary Reachability Analysis is that the safety checks are often difficult to decide by means of the currently available software Model Checkers [1, 2]. This problem unfortunately applies to both cases of finding a counterexample to an intermediate termination argument and to proving that no such counterexample exists.

As an example, consider a program that contains a trivial loop. The d.wf. transition invariant for the loop can be constructed in a negligible amount of time, but the computation of a path to the beginning of the loop may already exceed the computational resources available.

In this section, we describe a new algorithm for proving program termination that achieves the same result while avoiding excessively expensive safety checks.

We first define the usual relational composition operator ◦ for two relations A, B : S × S as

–  –  –

Note that a relation R is transitive if it is closed under relational composition, i.e., when R ◦ R ⊆ R. To simplify presentation, we also define R1 := R and Rn := Rn−1 ◦ R for any relation R : S × S.

While d.wf. transition invariants are not in general well-founded, there is a

trivial subclass for which this is the case:

Definition 4 (Compositional Transition Invariant). A d.wf. transition invariant T is called compositional if it is also transitive, or equivalently, closed under composition with itself, i.e., when T ◦ T ⊆ T.5 A compositional transition invariant is of course well-founded, since it is an inductive transition invariant for itself [3]. Using this observation and Theorem 1,

we conclude:

Corollary 1. A program P terminates if there exists a compositional transition invariant for P.

In Binary Reachability Analysis, the Model Checker needs to compute a counterexample to an intermediate termination argument, which is often difficult. The counterexample begins with a stem, i.e., a path to the entry point of the loop. For many programs, the existence of a d.wf. transition invariant does not actually depend on the entry state of the loop. For example, termination of a trivial loop that increments a variable i to a given upper limit u does not actually depend on the initial value of i, nor does it depend on u. The assurance of progress towards u is enough to conclude termination.

The other purpose of the Model Checker in BRA is to check that a candidate transition invariant indeed includes R+ restricted to the reachable states. To this end, we note that the (non-reflexive) transitive closure of R is essentially an

unwinding of program loops:

∞ R+ = R ∪ (R ◦ R) ∪ (R ◦ R ◦ R) ∪... = Ri.

i=1 Instead of searching for a d.wf. transition invariant that is a superset of R+, we can therefore decompose the problem into a series of smaller ones. We consider a series of loop-free programs in which R is unwound k times, i.e., the program that contains the transitions in R1 ∪... ∪ Rk.

Observation 2. Let P = S, I, R and k ≥ 1. If there is a d.wf. Tk with k j j=1 R ⊆ Tk and Tk is also transitive, then Tk is a compositional transition invariant for P.

–  –  –

This suggests a trivial algorithm that attempts to construct d.wf. relations Ti for incrementally deep unwindings of P until it finally finds a transitive Tk, which We use the term compositional instead of transitive for transition invariants in order to comply with the terminology in the existing literature [3].

proves termination of P. However, this trivial algorithm need not terminate, even for simple inputs. This is due to the fact that Ti does not necessarily have to be different from Ti−1, in which case the algorithm will never find a compositional transition invariant.

We provide an alternative that does not suffer from this limitation and takes advantage of the fact that most terminating loops encountered in practice have transition invariants with few disjuncts. To present this algorithm, we require the following lemma, which enables us to exclude computations from the program

that we have already proven terminating in a previous iteration:

–  –  –

As an optimization, we may safely omit some of the Ti while searching for a

transitive Tk :

Lemma 2 (Optimization). Let T0,..., Tk be the sequence of d.wf. relations for application of Lemma 1. The claim of the lemma holds even if some of the T1,..., Tk−1 are not provided (empty).

Proof. We show that Q is a transition invariant for P. Let (x, x ) ∈ R+ ∩(R∗ (I)× R∗ (I)). As in the proof of Obs. 2, (x, x ) ∈ Rl for some l. The claim holds k trivially for l ≤ k as i=1 Ri ⊆ Q. For l k, note that (x, x ) ∈ (Rjk ◦ Rl−jk ) and 0 ≤ l − jk k for some j ≥ 1. Note that Rjk ⊆ Qj and Rl−jk ⊆ Q. Thus, (x, x ) ∈ (Qj ◦ Q) = Qj+1. As Q is transitive, Qj+1 ⊆ Q, and thus (x, x ) ∈ Q.

The proof of Lemma 1 still applies. As an example, our implemenation only uses those Ti where i is a power of two.

The procedure that we draw from Lemma 2 is Algorithm 1, and we call it Compositional Termination Analysis (CTA). This algorithm makes use of an external ranking procedure called rank, which generates a d.wf. ranking relation for a given set of transitions, or alternatively a set C ∈ S of states such that R∗ (C) contains infinite computations. We say that rank is sound if it always returns either a d.wf. superset of its input or a non-empty set of states C, and we call it complete if it terminates on every input.

–  –  –

Algorithm 1 maintains a set X ⊆ S that is an over-approximation of the set of reachable states, i.e., R∗ (I) ⊆ X. It starts with X = S and at i = 1.

It iterates over i and generates d.wf. ranking relations Ti for the transitions in i j j=1 R \ T. As long as such relations are found, they are added to T. Once it finds a transitive T, the algorithm stops, as P terminates according to Lemma 2.

When ranking fails for some i, the algorithm checks whether there is a reachable state in C, in which case R∗ (C) contains a counterexample to termination and the algorithm consequently reports P as non-terminating. Otherwise, it removes C from X, which represents a refinement of the current over-approximation of the set of reachable states.

Theorem 3. Assuming the sub-procedure rank is sound, Algorithm 1 is sound.

Proof. When the algorithm terminates with ‘terminating’ (line 10), the sequence of relations Ti constructed so far is suitable for application of Lemma 2, which proves termination. It is easy to see that the set R∗ (I) in Lemma 2 can be overapproximated to X. If the algorithm returns ‘non-terminating’ at line 8, it has found a set of reachable states from which infinite computations exist, i.e., there is a concrete counterexample to termination.

Lines 12–14 ensure progress between iterations by excluding unreachable states (C) from the approximation X and adding the most recently found Ti in T. However, for non-terminating input programs, the algorithm may not terminate for two reasons: a) rank is not required to terminate, and b) there may be an infinite sequence of iterations.

This is not the case for finite S if the input program is non-terminating, since sound and complete ranking procedures exist (e.g., [5, 2]) and progress towards the goal can thus be ensured:



Pages:   || 2 | 3 |


Similar works:

«152 FERC 61,204 UNITED STATES OF AMERICA FEDERAL ENERGY REGULATORY COMMISSION Before Commissioners: Norman C. Bay, Chairman; Philip D. Moeller, Cheryl A. LaFleur, Tony Clark, and Colette D. Honorable. Seaway Crude Pipeline Company LLC Docket No. OR15-6-000 ORDER ON MARKET-BASED RATE APPLICATION AND ESTABLISHING HEARING PROCEDURES (Issued September 15, 2015) 1. On December 9, 2014, Seaway Crude Pipeline Company LLC (Seaway), pursuant to Part 348 1 of the Commission’s regulations, filed an...»

«DEVELOPMENT AND COMMISSIONING OF A PHOTON DETECTION SYSTEM FOR COLLINEAR LASER SPECTROSCOPY AT NSCL By Sophia Vinnikova A THESIS Submitted to Michigan State University in partial fulfillment of the requirements for the degree of Masters of Science Chemistry ABSTRACT DEVELOPMENT AND COMMISSIONING OF A PHOTON DETECTION SYSTEM FOR COLLINEAR LASER SPECTROSCOPY AT NSCL By Sophia Vinnikova A photon detection system has been developed for collinear laser spectroscopy measurements at the Beam COoling...»

«CLAIMS RESOLUTION TRIBUNAL In re Holocaust Victim Assets Litigation Case No. CV96-4849 Certified Award to Claimant Claudius Popovici, and to Claimant Cornelia Zissu-Hindichi in re Account of Rudolf Aronson Claim Numbers: 207773/LH;1 208485/LH Award Amount: 274,491.88 Swiss Francs This Certified Award is based upon the claims of Claudius Popovici ( Claimant Popovici ) and the claims of Cornelia Margareta Zissu-Hindichi, née Popovici, ( Claimant Zissu-Hindichi ) (together the Claimants ) to the...»

«Decision trees for error concealment in video decoding Song Cen, Pamela Cosman, Faramarz Azadegany ECE Dept., Univ. of California at San Diego, La Jolla, CA, 92093-0407 Rockwell Semiconductor Systems, A2-North, 9868 Scranton Road, San Diego, CA 92122 y faramarz.azadegan@rss.rockwell.com fscen,pcosmang@code.ucsd.edu Abstract: When macroblocks are lost in an MPEG decoder, the decoder can try to conceal the error by estimating or interpolating the missing area. Many di erent methods for this type...»

«PROJECT PERIODIC REPORT Grant Agreement number: 261679 Project acronym: CONTAIN Project title: Container Security Advanced Information Networking Funding Scheme: Collaborative Date of latest version of Annex I against which the assessment will be made: 05/11/2014 1st  2nd  3rd  4th  Periodic report: Period covered: from 01/10/2013 to 31/03/2015 Name, title and organisation of the scientific representative of the project's coordinator1: Dr. Joel Brynielsson, FOI Swedish Defence...»

«Driving down the extra costs disabled people face Final report Extra Costs Commission Investigating costs faced by disabled people The Extra Costs Commission is generously supported by the Barrow Cadbury Trust. The Barrow Cadbury Trust is an independent charitable foundation, committed to bringing about socially just change. This is the final report of the Extra Costs Commission. The Commission is an independent inquiry exploring the extra costs faced by disabled people and families with...»

«E COPTIC ORTHODOX PATRIARCHATE Contemplations on the Ten Commandments Volume 3 THE SIXTH COMMANDMENT BY H. H. POPE SHENOUDA III Title : The Sixth Commandment (Volume 3). Author : H. H. Pope Shenouda III. Translated by: Fr. Markos Hanna & Nadia. Reviewed by : Mr. Sobhy Botros. Revised by : Mrs Wedad Abbas. Illustrated by : Sister Sawsan. Edition : The Second February 1993. Typesetting : J.C.Center Heliopolis. Printing : Dar El Tebaa El Kawmia Cairo. Legal Deposit : 3940/1992. I.S.B.N :...»

«Assessment of Stream Resources at Regulated Coal Mining and Remining Sites in Ohio Robert Baker1, Tarunjit Butalia1, Chin-Min Cheng1, Cheryl Socotch2 The Ohio State University, Department of Civil, Environmental, and Geodetic Engineering, 2070 Neil Ave., Columbus, OH 43210; 2OhioDNR Division of Mineral Resources Management KEYWORDS: stream assessment, coal mine reclamation, Headwater Habitat Evaluation Index, Headwater Macroinvertebrate Field Evaluation Index Abstract The long-term effects of...»

«71 FR 61019, October 17, 2006 A-570-832 POR: 05/01/04-04/30/05 Public Document IA/NME/VIII: HL October 10, 2006 David M. Spooner MEMORANDUM TO: Assistant Secretary for Import Administration Stephen J. Claeys FROM: Deputy Assistant Secretary for Import Administration Issues and Decision Memorandum for the Final Results of the SUBJECT: Administrative Review of the Antidumping Duty Order on Pure Magnesium from the People’s Republic of China SUMMARY We have analyzed the comments of the interested...»

«6905 Mills Civic Parkway, Suite 120, West Des Moines, IA 50266 2 POLICIES & PROCEDURES Revised 9.4.2014 3 POLICIES & PROCEDURES Table of Contents Page # Contents Table of Contents Cover Page Table of Contents Table of Contents Table of Contents Mission Statement Program Options Tuition Chart Tuition Payment Options Tuition Payment Options Upcoming Start Dates and Holidays Upcoming Holidays Academic Completion Information Academic Completion Information Academic Completion Information Academic...»

«DHRD Course Announcement DATE: September 1, 2011 FROM: John Shafer Director, Division of Human Resource Development (HFC-60) SUBJECT: COURSE ANNOUNCEMENT: Inspection of Human Cells, Tissues & Cellular and Tissue Based Product Establishments (HCT/Ps) (BI206) Rockville, MD Begin: Monday, December 12 at 8:00 AM End: Friday, December 16 at 12:00 PM AUTHORIZED TRAVEL DATES: Arrival: Sunday, December 11 Departure: Friday, December 16 (schedule return flights after 2:30PM) Everyone is expected to...»

«ACTA • ARCH/ELOGICA BRIGETIONENSIA A RÓMAI KORI FALFESTÉSZET PANNONIÁBAN DIE ROMISCHE WANDMALEREI IN PANNONIÉN A RÓMAI KORI FALFESTÉSZET PANNONIÁBAN Nemzetközi konferencia a pannóniai falfestészet problémáiról DIE RÖMISCHE WANDMALEREI IN PANNONIÉN Internationale Fachkonferenz über Probleme der Wandmalerei in Pannonién Ser. I. Vol. 1. ACTA ARCHAEOLOGICA BRIGETIONENSIA Ser. I. Vol. 1. A RÓMAI KORI FALFESTÉSZET PANNONIÁBAN Nemzetközi konferencia a pannóniai falfestészet...»





 
<<  HOME   |    CONTACTS
2016 www.dis.xlibx.info - Thesis, dissertations, books

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.