The Arithmetic Geometric Progression Abstract Domain
17 pages
English

The Arithmetic Geometric Progression Abstract Domain

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
17 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Niveau: Supérieur, Doctorat, Bac+8
The Arithmetic-Geometric Progression Abstract Domain? Jerome Feret DI, Ecole Normale Superieure, Paris, FRANCE Abstract We present a new numerical abstract domain. This domain automatically detects and proves bounds on the values of program vari- ables. For that purpose, it relates variable values to a clock counter. More precisely, it bounds these values with the i-th iterate of the func- tion [X 7? ??X+?] applied on M , where i denotes the clock counter and the floating-point numbers ?, ?, and M are discovered by the analysis. Such properties are especially useful to analyze loops in which a variable is iteratively assigned with a barycentric mean of the values that were associated with the same variable at some previous iterations. Because of rounding errors, the computation of this barycenter may diverge when the loop is iterated forever. Our domain provides a bound that depends on the execution time of the program. Keywords: Abstract Interpretation, static analysis, numerical domains. 1 Introduction A critical synchronous real-time system (as found in automotive, aeronautic, and aerospace applications) usually consists in iterating a huge loop. Because practical systems do not run forever, a bound on the maximum iteration number of this loop can be provided by the end-user or discovered automatically.

  • all real

  • progression abstract

  • variable

  • geometric progression

  • coefficients ?

  • loop iteration

  • over-approximates all

  • rounding errors


Sujets

Informations

Publié par
Nombre de lectures 8
Langue English

Exrait

TheArithmetic-GeometricProgressionAbstractDomain?Je´roˆmeFeretDI,E´coleNormaleSupe´rieure,Paris,FRANCEjerome.feret@ens.frAbstractWepresentanewnumericalabstractdomain.Thisdomainautomaticallydetectsandprovesboundsonthevaluesofprogramvari-ables.Forthatpurpose,itrelatesvariablevaluestoaclockcounter.Moreprecisely,itboundsthesevalueswiththei-thiterateofthefunc-tion[X7→α×X+β]appliedonM,whereidenotestheclockcounterandthefloating-pointnumbersα,β,andMarediscoveredbytheanalysis.Suchpropertiesareespeciallyusefultoanalyzeloopsinwhichavariableisiterativelyassignedwithabarycentricmeanofthevaluesthatwereassociatedwiththesamevariableatsomepreviousiterations.Becauseofroundingerrors,thecomputationofthisbarycentermaydivergewhentheloopisiteratedforever.Ourdomainprovidesaboundthatdependsontheexecutiontimeoftheprogram.Keywords:AbstractInterpretation,staticanalysis,numericaldomains.1IntroductionAcriticalsynchronousreal-timesystem(asfoundinautomotive,aeronautic,andaerospaceapplications)usuallyconsistsiniteratingahugeloop.Becausepracticalsystemsdonotrunforever,aboundonthemaximumiterationnumberofthisloopcanbeprovidedbytheend-userordiscoveredautomatically.Thefullcertificationofsuchasoftwaremayrequirerelatingvariablevaluestothenumberofiterationsofthemainloop.Itisespeciallytruewhenusingfloating-pointnumbers.Somecomputationsthatarestablewhencarriedoutintherealfield,maydivergebecauseoftheroundingerrors.Roundingerrorsareaccumulatedateachiterationoftheloop.Whenexpressionsarelinearandwhentheevaluationofexpressionsdoesnotoverflow,theroundingerrorsateachloopiterationareusuallyproportionaltothevalueofthevariables.Thustheoverallcontributionofroundingerrorscanbeobtainedbyiteratingafunctionoftheform[X7→α×X+β].Thenbyusingthemaximumnumberofiterationswecaninferboundsonthevaluesthatwouldnormallyhavedivergedinthecaseofaninfinitecomputation.Weproposeanewnumericalabstractdomainthatassociateswitheachvari-ablethecorrespondingcoefficientsαandβandthestartingvalueM.This?ThisworkwaspartiallysupportedbytheASTRE´ERNTLproject.
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents