The Arithmetic Geometric Progression Abstract Domain

Jérôme Feret

Description

MPRI The Arithmetic-Geometric Progression Abstract Domain VMCAI 2005 Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS feret December, 2008.

• using floating


• laboratoire d'informatique de l'ecole normale


• progression abstract


• arithmetic-geometric progressions


• floating point

Sujets

• Floating point

Informations

• Publié par: pefav
• Nombre de lectures: 19
• Langue: English

Extrait

n.fwwwi.//s.:epr/ttferethd
MPRI
The Arithmetic-Geometric Progression
Abstract Domain
VMCAI 2005
Jérôme Feret
Laboratoire d’Informatique de l’École Normale Supérieure
INRIA, ÉNS, CNRS
∼
December, 2008.Overview
1. Introduction
2. Case study
3. Arithmetic-geometric progressions
4. Benchmarks
5. Conclusion
Jérôme Feret 2 December, 2008Issue
• In automatically generated programs using floating point arithmetics,
some computations may diverge because of rounding errors.
• We prove the absence of floating point number overflows:
we bound rounding errors at each loop iteration by a linear combination
of the loop inputs; we get bounds on the values that depends exponen-
tially on the program execution time.
• We use non polynomial constraints. Our domain is both precise (no
false alarm) and efficient (linear in memory /nln(n) in time).
Jérôme Feret 3 December, 2008Overview
1. Introduction
2. Case study
3. Arithmetic-geometric progressions
4. Benchmarks
5. Conclusion
Jérôme Feret 4 December, 2008Running example (inR)
1 : X :=0;k :=0;
2 : while (k<1000) {
3 : if (?) {X∈ [−10;10]};
4 : X :=X/3;
5 : X :=3×X;
6 : k :=k +1;
7 : }
Jérôme Feret 5 December, 2008Interval analysis: first loop iteration
1 : X :=0;k :=0;
X =0
2 : while (k<1000) {
X =0
3 : if (?) {X∈ [−10;10]};
|X|≤10
4 : X :=X/3;
10
|X|≤
3
5 : X :=3×X;
|X|≤10
6 : k :=k +1;
7 : }
Jérôme Feret 6 December, 2008Interval analysis: Invariant
1 : X :=0;k :=0;
X =0
2 : while (k<1000) {
|X|≤10
3 : if (?) {X∈ [−10;10]};
|X|≤10
4 : X :=X/3;
10
|X|≤
3
5 : X :=3×X;
|X|≤10
6 : k :=k +1;
7 : }
|X|≤10
Jérôme Feret 7 December, 2008Including rounding errors [Miné–ESOP’04]
1 : X :=0;k :=0;
2 : while (k<1000) {
3 : if (?) {X∈ [−10;10]};
4 : X :=X/3 + [−ε ;ε ].X + [−ε ;ε ];
1 1 2 2
5 : X :=3×X + [−ε ;ε ].X + [−ε ;ε ];
3 3 4 4
6 : k :=k +1;
7 : }
The constantsε ,ε ,ε , andε (≥0) are computed by other domains.
1 2 3 4
Jérôme Feret 8 December, 2008Interval analysis
LetM≥0 be a bound:
1 : X :=0;k :=0;
X =0
2 : while (k<1000) {
|X|≤M
3 : if (?) {X∈ [−10;10]};
|X|≤ max(M,10)
4 : X :=X/3 + [−ε ;ε ].X + [−ε ;ε ];
1 1 2 2
1
|X|≤ (ε + )× max(M,10) +ε
1 2
3
5 : X :=3×X + [−ε ;ε ].X + [−ε ;ε ];
3 3 4 4
|X|≤ (1 +a)× max(M,10) +b
6 : k :=k +1;
7 : }
ε
3
witha =3×ε + +ε ×ε andb =ε × (3 +ε ) +ε .
1 1 3 2 3 4
3
Jérôme Feret 9 December, 200877
Ari.-geo. analysis: first iteration
1 : X :=0;k :=0;
X =0,k =0
2 : while (k<1000) {
X =0
3 : if (?) {X∈ [−10;10]};
|X|≤10
4 : X :=X/3 + [−ε ;ε ].X + [−ε ;ε ];
1 1 2 2
£ ¡ ¢ ¤
1
|X|≤ v→ +ε ×v +ε (10)
1 2
3
5 : X :=3×X + [−ε ;ε ].X + [−ε ;ε ];
3 3 4 4
(1)
|X|≤f (10)
6 : k :=k +1;
(k)
|X|≤f (10),k =1
7 : }
£ ¡ ¢ ¤
ε
3
withf = v→ 1 +3×ε + +ε ×ε ×v +ε × (3 +ε ) +ε .
1 1 3 2 3 4
3
Jérôme Feret 10 December, 2008