The Arithmetic Geometric Progression Abstract Domain

pages

English

Documents

Écrit par
Jérôme Feret

Publié par
pefav

Lire un extrait

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

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

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

Publié par

pefav

Nombre de lectures

Langue

English

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

Voir

Publié par

pefav

Nombre de lectures

Langue

English

Floating point

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 ﬂoating point arithmetics,
some computations may diverge because of rounding errors.
• We prove the absence of ﬂoating point number overﬂows:
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 efﬁcient (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: ﬁrst 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: ﬁrst 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