The Arithmetic Geometric Progression Abstract Domain

Jérôme Feret

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

• Several
• Variable
• Geometric progression

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 8
• Langue: English

Extrait

TheArithmetic-GeometricProgression AbstractDomain ? Je´roˆmeFeret DI,E ´ coleNormaleSupe´rieure,Paris,FRANCE [e-mail] AbstractWepresentanewnumericalabstractdomain.Thisdomain automaticallydetectsandprovesboundsonthevaluesofprogramvari- ables.Forthatpurpose,itrelatesvariablevaluestoaclockcounter. Moreprecisely,itboundsthesevalueswiththei-thiterateofthefunc- tion[X 7→ α × X+β]appliedonM,whereidenotestheclockcounterand thefloating-pointnumbersα,β,andMarediscoveredbytheanalysis. Suchpropertiesareespeciallyusefultoanalyzeloopsinwhichavariable isiterativelyassignedwithabarycentricmeanofthevaluesthatwere associatedwiththesamevariableatsomepreviousiterations.Because ofroundingerrors,thecomputationofthisbarycentermaydivergewhen theloopisiteratedforever.Ourdomainprovidesaboundthatdepends ontheexecutiontimeoftheprogram. Keywords:AbstractInterpretation,staticanalysis,numericaldomains. 1Introduction Acriticalsynchronousreal-timesystem(asfoundinautomotive,aeronautic, andaerospaceapplications)usuallyconsistsiniteratingahugeloop.Because practicalsystemsdonotrunforever,aboundonthemaximumiterationnumber ofthisloopcanbeprovidedbytheend-userordiscoveredautomatically.Thefull certificationofsuchasoftwaremayrequirerelatingvariablevaluestothenumber ofiterationsofthemainloop.Itisespeciallytruewhenusingfloating-point numbers.Somecomputationsthatarestablewhencarriedoutintherealfield, maydivergebecauseoftheroundingerrors.Roundingerrorsareaccumulatedat eachiterationoftheloop.Whenexpressionsarelinearandwhentheevaluation ofexpressionsdoesnotoverflow,theroundingerrorsateachloopiterationare usuallyproportionaltothevalueofthevariables.Thustheoverallcontribution ofroundingerrorscanbeobtainedbyiteratingafunctionoftheform[X 7→ α × X+β].Thenbyusingthemaximumnumberofiterationswecaninfer boundsonthevaluesthatwouldnormallyhavedivergedinthecaseofaninfinite computation. Weproposeanewnumericalabstractdomainthatassociateswitheachvari- ablethecorrespondingcoefficientsαandβandthestartingvalueM.This ? ThisworkwaspartiallysupportedbytheASTRE ´ ERNTLproject.