La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

06-these

134 pages
◦ ◦N d’ordre:388 N attribuéparlabibliothèque:06ENSL0388ÉCOLE NORMALE SUPÉRIEURE DE LYONLaboratoiredel’InformatiqueduParallélismeTHÈSEprésentéeetsoutenuepubliquementle21novembre2006parGuillaume MELQUIONDpourl’obtentiondugradedeDocteurdel’ÉcoleNormaleSupérieuredeLyonspécialité:Informatiqueautitredel’Écoledoctoraledemathématiquesetd’informatiquefondamentaledeLyonDel’arithmétiqued’intervallesàlacertificationdeprogrammesDirecteurdethèse: Marc DAUMASAprèsavisde: Guillaume HANROTChristine PAULIN-MOHRINGDevantlacommissiond’examenforméede:Jean Daniel B OISSONNAT MembreMarc DAUMASGuillaume HANROT Membre/RapporteurJohn HARRISON MembreJean Michel M ULLERChristine PAULIN-MOHRINGRemerciementsJetiensàremerciermondirecteurdethèseMarcDaumasd’avoirvulepotentieldestravauxprésentésicietdem’avoirlaisséunegrandeliberté.Je tiens à remercier Christine Paulin Mohring et Guillaume Hanrot d’avoir étéles rapporteurs de cette thèse, Jean Daniel Boissonnat d’avoir présidé, John Har-risson d’être venu de si loin et Jean Michel Muller d’avoir complété le jury d’unmembrelocalmaisnéanmoinscompétent.Je tiens à remercier mes coauteurs, Sylvie Boldo, Hervé Brönnimann, FlorentdeDinechin,ChristophLauter,CésarMuñozetSylvainPion.Je tiens à remercier Simone Criqui, Claude Pierre Jeannerod, Nathalie Revolet Arnaud Tisserand pour leur relecture attentive de ce document. Toute faute quevouspourriezydétecterprovientvraisemblablementdesretouchesdedernièremi ...
Voir plus Voir moins

Vous aimerez aussi

◦ ◦N d’ordre:388 N attribuéparlabibliothèque:06ENSL0388
ÉCOLE NORMALE SUPÉRIEURE DE LYON
Laboratoiredel’InformatiqueduParallélisme
THÈSE
présentéeetsoutenuepubliquementle21novembre2006par
Guillaume MELQUIOND
pourl’obtentiondugradede
Docteurdel’ÉcoleNormaleSupérieuredeLyon
spécialité:Informatique
autitredel’Écoledoctoraledemathématiquesetd’informatiquefondamentaledeLyon
Del’arithmétiqued’intervalles
àlacertificationdeprogrammes
Directeurdethèse: Marc DAUMAS
Aprèsavisde: Guillaume HANROT
Christine PAULIN-MOHRING
Devantlacommissiond’examenforméede:
Jean Daniel B OISSONNAT Membre
Marc DAUMAS
Guillaume HANROT Membre/Rapporteur
John HARRISON Membre
Jean Michel M ULLER
Christine PAULIN-MOHRINGRemerciements
JetiensàremerciermondirecteurdethèseMarcDaumasd’avoirvulepotentiel
destravauxprésentésicietdem’avoirlaisséunegrandeliberté.
Je tiens à remercier Christine Paulin Mohring et Guillaume Hanrot d’avoir été
les rapporteurs de cette thèse, Jean Daniel Boissonnat d’avoir présidé, John Har-
risson d’être venu de si loin et Jean Michel Muller d’avoir complété le jury d’un
membrelocalmaisnéanmoinscompétent.
Je tiens à remercier mes coauteurs, Sylvie Boldo, Hervé Brönnimann, Florent
deDinechin,ChristophLauter,CésarMuñozetSylvainPion.
Je tiens à remercier Simone Criqui, Claude Pierre Jeannerod, Nathalie Revol
et Arnaud Tisserand pour leur relecture attentive de ce document. Toute faute que
vouspourriezydétecterprovientvraisemblablementdesretouchesdedernièremi
nutequej’aieffectuéesetnonpasd’unmanquedesérieuxdeleurpart.
Je tiens à remercier Francisco, Nicolas, Romain et Sylvain d’avoir été des co
1bureaux sympathiques . Je tiens à remercier les thésards du laboratoire qui ont su
me faire perdre de nombreuses heures dans des jeux en réseau : Damien, Florent,
Jérémie, Nicolas, Victor, Vincent. Les jeux en réseau ne sont pas la seule source
de non productivité et je tiens donc aussi à remercier Anne, Damien, Emmanuel,
Florent, Laurent, Stéphane et Stéphane, Sylvain et Sylvain. Comme tous les che
mins viennent de Lyon, il me faut aussi mentionner Benoît, Blaise, Christophe,
Emmanuelle et Emmanuel, Laurent, Philippe. Et enfin, Camille et Camille pour
leurréapparitionsurprise.J’aiprobablementoubliédenombreusespersonnesdans
ces quelques listes et, tôt ou tard, je me réveillerai en sursaut au milieu de la nuit
enmedisant:«Flûtine,j’aioubliéderemercierMachin!»
Je tiens à remercier les membres de l’équipe Arénaire qui ont su échapper aux
énumérations précédentes, en particulier Gilles Villard et Sylvie Boyer. Il faudrait
aussiquejeremercieleshabitantsdutroisièmeétage,Corinne,Dominique,Serge,
Simone, mais il y en a trop, je ne vais pas m’en sortir. Sans compter les ensei
gnants du département d’informatique de l’ENSL, ainsi que Jean François Pon
signon pour l’INSA. Et enfin, les étudiants qui m’ont subi pendant ces quelques
annéesdethèse.
CedocumenttientàremercierGedit,LatexetRubber.
Pourfinir:Pierre,onnet’oubliepas.
1Si votre prénom n’apparaît pas dans cette liste, ce n’est pas que vous m’êtes antipathique, c’est
justequevousavezdéjàétéremerciéunefois.Lamêmeremarques’appliqueauxlistessuivantes.
iiiTabledesmatières
1 Introduction 1
1.1 Certificationdecodesnumériques . . . . . . . . . . . . . . . . . 2
1.1.1 Bornesdevariablesetcomportementsinvalides . . . . . . 2
1.1.2 Erreursnumériques . . . . . . . . . . . . . . . . . . . . . 3
1.2 L’outilGappa . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3 Positionnement . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3.1 Certificationformelledecodesarithmétiques . . . . . . . 6
1.3.2 Calculautomatiquedel’erreurd’arrondi . . . . . . . . . . 6
1.3.3 Certificationautomatiquedeprogrammes . . . . . . . . . 7
1.4 Plandudocument . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Preuveetarithmétiqued’intervalles 9
2.1 Preuves,ensemblesetinclusion . . . . . . . . . . . . . . . . . . . 10
2.1.1 Preuvedepropositions . . . . . . . . . . . . . . . . . . . 10
2.1.2 Réductionauxintervalles . . . . . . . . . . . . . . . . . . 11
2.2 Arithmétiqued’intervalles . . . . . . . . . . . . . . . . . . . . . 11
2.2.1 Typesalles . . . . . . . . . . . . . . . . . . . . . 11
2.2.2 Opérateursarithmétiques . . . . . . . . . . . . . . . . . . 12
2.2.3 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3 Lesintervallesenpratique . . . . . . . . . . . . . . . . . . . . . 14
2.3.1 Bornesd’intervalles . . . . . . . . . . . . . . . . . . . . 15
2.3.2 Croissanceetarrondidesbornes . . . . . . . . . . . . . . 16
2.3.3 Simplificationetoracle . . . . . . . . . . . . . . . . . . . 17
3 Intervallesetpertedecorrélation 19
3.1 Bissectiond’intervalles . . . . . . . . . . . . . . . . . . . . . . . 20
3.1.1 Exemplesetinconvénients . . . . . . . . . . . . . . . . . 20
3.1.2 Avantagesdelabissection . . . . . . . . . . . . . . . . . 21
3.2 Réécrituresd’expressionsd’erreur . . . . . . . . . . . . . . . . . 21
3.2.1 Àpartirdesarbressyntaxiques . . . . . . . . . . . . . . . 22
3.2.2 Àpartird’expressionsintermédiaires . . . . . . . . . . . 23
3.2.3 Autresréécritures . . . . . . . . . . . . . . . . . . . . . . 23
3.3 Améliorationd’encadrements . . . . . . . . . . . . . . . . . . . . 24
iiiiv TABLEDESMATIÈRES
3.3.1 Dérivationd’expressions . . . . . . . . . . . . . . . . . . 24
3.3.2 Nouveauxopérateursarithmétiques . . . . . . . . . . . . 25
3.3.3 Laquestiondelavaleurabsolue . . . . . . . . . . . . . . 28
3.3.4 Représentationsaméliorées . . . . . . . . . . . . . . . . . 29
4 Arithmétiquesapprochéesenmachine 33
4.1 Opérateursd’arrondi . . . . . . . . . . . . . . . . . . . . . . . . 33
4.1.1 Opérateursunaires . . . . . . . . . . . . . . . . . . . . . 34
4.1.2généralisés . . . . . . . . . . . . . . . . . . . 34
4.1.3 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . 35
4.1.4 Changerl’ensemblesous jacent . . . . . . . . . . . . . . 36
4.2 Représentations . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.1 Arithmétiqueàvirgulefixe . . . . . . . . . . . . . . . . . 37
4.2.2flottante . . . . . . . . . . . . . . . . . . . 38
4.2.3 Directionsd’arrondi . . . . . . . . . . . . . . . . . . . . 39
4.3 Théorèmesassociés . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.3.1 Bornesdevaleursarrondies . . . . . . . . . . . . . . . . 41
4.3.2 Erreursabsolues . . . . . . . . . . . . . . . . . . . . . . 42
4.3.3relatives . . . . . . . . . . . . . . . . . . . . . . 44
4.3.4 Réécritures . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.4 Prédicatsdeprécision . . . . . . . . . . . . . . . . . . . . . . . . 45
4.4.1 Prédicatdevirgulefixe . . . . . . . . . . . . . . . . . . . 46
4.4.2devirguleflottante . . . . . . . . . . . . . . . . 47
4.4.3 Exemple:Sterbenz . . . . . . . . . . . . . . . . . . . . . 47
5 FonctionnementdeGappa 49
5.1 Prétraitement . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.1.1 Miseenformedespropositionslogiques . . . . . . . . . . 50
5.1.2 Recherchedescheminsdecalcul . . . . . . . . . . . . . . 51
5.2 Graphesdepreuve . . . . . . . . . . . . . . . . . . . . . . . . . 52
5.2.1 Théorèmesetgraphesdepreuves . . . . . . . . . . . . . 53
5.2.2 Intersections . . . . . . . . . . . . . . . . . . . . . . . . 54
5.2.3 Encadrementsenvaleurabsolue . . . . . . . . . . . . . . 55
5.3 Bissections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
5.3.1 Déroulementd’unebissection . . . . . . . . . . . . . . . 56
5.3.2 Déclarationdebissections . . . . . . . . . . . . . . . . . 57
5.3.3 Découpageciblé . . . . . . . . . . . . . . . . . . . . . . 58
5.4 Règlesderéécriture . . . . . . . . . . . . . . . . . . . . . . . . . 60
5.4.1 Règlesprédéfinies . . . . . . . . . . . . . . . . . . . . . 61
5.4.2 Expressionsapprochéesetexpressionsexactes . . . . . . 61
5.4.3 Règlesutilisateur . . . . . . . . . . . . . . . . . . . . . . 62TABLEDESMATIÈRES v
6 Vérificationautomatique 65
6.1 Certificatsetapprocheoracle . . . . . . . . . . . . . . . . . . . . 66
6.2 Vérificationparlecalcul . . . . . . . . . . . . . . . . . . . . . . 67
6.2.1 Opérationssurlesnombresdyadiques . . . . . . . . . . . 68
6.2.2 Fonctionsbooléennes . . . . . . . . . . . . . . . . . . . . 70
6.3 Calculssimplifiés . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.3.1 Spécialisationdesthéorèmes . . . . . . . . . . . . . . . . 71
6.3.2 Gestiondesvaleursabsolues . . . . . . . . . . . . . . . . 73
6.3.3 Utilisationdesmultiplications . . . . . . . . . . . . . . . 73
6.3.4 Influencedelaprécision . . . . . . . . . . . . . . . . . . 74
6.4 Théorèmesetarrondis . . . . . . . . . . . . . . . . . . . . . . . . 75
6.4.1 Fonctiond’exposant . . . . . . . . . . . . . . . . . . . . 76
6.4.2 Arrondidesnombresdyadiques . . . . . . . . . . . . . . 76
6.4.3 Exempledethéorème . . . . . . . . . . . . . . . . . . . . 78
7 ApplicationdeGappaauxfonctionsélémentaires 79
7.1 L’exponentielledeTang . . . . . . . . . . . . . . . . . . . . . . . 80
7.1.1 Présentationdel’algorithme . . . . . . . . . . . . . . . . 80
7.1.2 FormalisationGappa . . . . . . . . . . . . . . . . . . . . 81
7.1.3 Ajoutd’indices . . . . . . . . . . . . . . . . . . . . . . . 82
7.2 Arithmétiquedouble double . . . . . . . . . . . . . . . . . . . . 83
7.2.1 Opérationsexactes . . . . . . . . . . . . . . . . . . . . . 83
7.2.2enprécisionélevée . . . . . . . . . . . . . . . 85
7.3 Gestiondeserreurs . . . . . . . . . . . . . . . . . . . . . . . . . 87
8 Prédicatsgéométriqueshomogènes 89
8.1 Géométriealgorithmiqueetcalculexact . . . . . . . . . . . . . . 89
8.1.1 Orientationdetroispointsduplan . . . . . . . . . . . . . 90
8.1.2 Approcheparfiltre . . . . . . . . . . . . . . . . . . . . . 93
8.2 Nouvellearithmétique . . . . . . . . . . . . . . . . . . . . . . . . 94
8.2.1 Additionetmultiplication . . . . . . . . . . . . . . . . . 94
8.2.2 Arrondis . . . . . . . . . . . . . . . . . . . . . . . . . . 94
8.2.3 Derniersdétails . . . . . . . . . . . . . . . . . . . . . . . 95
8.2.4 TranscriptionGappa . . . . . . . . . . . . . . . . . . . . 96
8.3 Filtresemi statiquerobuste . . . . . . . . . . . . . . . . . . . . . 96
8.3.1 Implantation . . . . . . . . . . . . . . . . . . . . . . . . 97
8.3.2 Performances . . . . . . . . . . . . . . . . . . . . . . . . 97
8.3.3 Généralisation . . . . . . . . . . . . . . . . . . . . . . . 98
9 Conclusionetperspectives 99
9.1 Unoutild’aideàlacertification . . . . . . . . . . . . . . . . . . 99
9.2 ParticularitésdeGappa . . . . . . . . . . . . . . . . . . . . . . . 100
9.3 Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100vi TABLEDESMATIÈRES
A Travailleraveclesintervalles 103
A.1 Boost . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
A.2 Normalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
B SyntaxeetsémantiquedulangageGappa 107
B.1 Expressionsréelles . . . . . . . . . . . . . . . . . . . . . . . . . 107
B.1.1 Nombres . . . . . . . . . . . . . . . . . . . . . . . . . . 107
B.1.2 Opérateurs,fonctionsetexpressions . . . . . . . . . . . . 108
B.2 ScriptGappa . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
B.2.1 Définitionsd’expression . . . . . . . . . . . . . . . . . . 108
B.2.2 Propositionlogique . . . . . . . . . . . . . . . . . . . . . 109
B.2.3 Indicationsderésolution . . . . . . . . . . . . . . . . . . 110
C Listedesthéorèmes 111Chapitre1
Introduction
+L’explosion d’Ariane 5 lors de son vol inaugural [L 96], la chute de l’in
dice de la bourse de Vancouver dans les années 80 [MV99], la défaillance d’un
missile Patriot lors de la première guerre du Golfe [Inf92] sont quelques uns des
nombreux exemples de problèmes informatiques aux conséquences parfois dra
matiques. Dans certains cas, il s’agit d’une opération qui renvoie une valeur trop
grande pour être stockée dans les registres, provoquant un comportement excep
tionnelduprogramme.Dansd’autrescas,depetiteserreursdecalculs’accumulent
au cours du temps et font progressivement diverger les valeurs du programme des
valeursidéales.
Ces problèmes n’ont pas été causés par un facteur extérieur : il n’y a pas eu
de défaillance matérielle ou de rayon cosmique pour venir perturber les calculs.
Le comportement de ces applications était conforme à leur implantation. Le pro
blème réside donc en amont, au niveau de la conception. À l’heure où logiciels et
matérielsinformatiquess’immiscentdanstouslesdomaines,ildevientdoncindis
pensabledegarantirqu’uneapplicationfaitbiencequ’onattendd’elle.Unenorme
internationale [ISO05] propose différents niveaux (Evaluation Assurance Level)
décrivant le soin apporté durant la conception d’un système. Le niveau le plus sûr,
EAL 7, est accordé à condition que le logiciel/matériel ait non seulement été testé
maisqu’enplussespartiescritiquesaientétévérifiéesformellement,c’est à direà
l’aidedeméthodesmathématiques.
Cettenormeestprincipalementconçuepourévaluerlescomposantsquijouent
un rôle en matière de sécurité informatique (systèmes d’exploitation, pare feux,
etc). Mais cette obligation d’une vérification formelle pourrait être étendue aux
applications qui effectuent des calculs numériques. Il est en effet indispensable de
s’assurerquelerésultatcalculéparl’applicationrépondbienauproblèmeposépar
l’utilisateur, au moins dans une certaine mesure. L’arithmétique d’intervalles est
une des approches possibles : elle fournit des algorithmes et méthodes permettant
de calculer des bornes rigoureuses sur des solutions approchées (erreur et valeur
calculée)[Moo79,JKDW01].
Une autre approche consiste à effectuer une certification statique de l’applica
12 CHAPITRE1. INTRODUCTION
tion. Le développeur apporte la preuve que les résultats calculés sont toujours en
accord avec les spécifications et qu’il n’y a donc pas besoin de recourir à des mé
thodesrobustespourl’exécutiondel’application.Mêmes’ilestdeplusenplusem
ployé,cetypedecertificationformelleconstitueuntravaillong,pénibleetpropice
auxerreurs,àcausedelacomplexitédesapplicationsàtraiter.L’outilinformatique
pourrait automatiser une part importante de ce travail et certifier formellement les
applicationseffectuantdescalculsnumériques.Cettethèsedécritlesméthodesdé
1veloppéespourlelogicielGappa afinqu’ilaccomplissecetravaildecertification.
Mêmesinousnousplaçonsicidansledomainedelacertificationstatique,cela
nesignifiepaspourautantquel’arithmétiqued’intervallesestabandonnée.Elleest
eneffetutilisée,nonpasdansleprogrammeàcertifier,maisdansl’outilquisertàle
certifier.Sonemploigarantitquel’outilnes’estpasfourvoyé.Enadaptantcertaines
desesméthodes,ellepermetmêmedegénéreruncertificatformelprouvantquele
programme se comportera correctement. L’un des enjeux de cette thèse consiste à
sélectionner les méthodes de l’arithmétique d’intervalles suffisamment puissantes
pour traiter des applications numériques tout en étant suf simples pour
nepasêtreunfreinàlaconstructiondescertificatsdecesapplications.
1.1 Certificationdecodesnumériques
Les programmes considérés ici sont des codes effectuant des calculs numé
riques avec des arithmétiques approchées. Ces codes calculent des valeurs sans
que leur flot d’exécution ne soit perturbé. Structures conditionnelles, terminaison
des boucles, validité des accès mémoire sont laissées à l’analyse d’outils de certi
ficationplusgénéralistes[Fil03,vdBJ01].Lesportionsdeprogrammequ’ilresteà
analyser après le traitement de ces outils ne contiennent que des opérateurs arith
métiques et sont généralement qualifiées de Straight Line Programs . Elles sont
représentables par des graphes dirigés acycliques dont les nœuds sont des opéra
teurs arithmétiques. Afin de coller au comportement du programme tel qu’il sera
exécutésurunprocesseur,cesopérateursnesontpaslesopérateursthéoriquesqui
calculent en précision infinie mais bien les opérateurs tels qu’ils sont implantés en
matériel. En particulier, la précision des formats numériques utilisés est limitée et
chaquevaleurcalculéeestdoncpotentiellemententachéed’uneerreurd’arrondi.
1.1.1 Bornesdevariablesetcomportementsinvalides
Ceserreursproduitesaucoursduprogrammerisquentdeprogressivements’ac
cumuler et de faire diverger les valeurs calculées des valeurs théoriques. À force
de diverger, ces valeurs peuvent se retrouver hors des domaines prévus, condui
sant ainsi à des divisions par zéro ou des racines carrées de nombres négatifs par
exemple. Les valeurs peuvent aussi augmenter démesurément, franchissant alors
1Gappaestl’acronymede«GénérationAutomatiquedePreuvesdePropriétésArithmétiques».