of 9

Un nouvel algorithme de consistance locale sur les nombres flottants

0 views
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Share
Description
Actes JFPC 0 Un nouvel algorithme de consistance locale sur les nombres flottants Mohammed Said BELAID, Claude MICHEL, Michel RUEHER I3S UNS/CNRS, 000 route des Lucioles, BP, Sophia Antipolis Cedex,
Transcript
Actes JFPC 0 Un nouvel algorithme de consistance locale sur les nombres flottants Mohammed Said BELAID, Claude MICHEL, Michel RUEHER I3S UNS/CNRS, 000 route des Lucioles, BP, Sophia Antipolis Cedex, France {MSBelaid, Résumé La résolution de contraintes sur les nombres à virgule flottante soulève des problèmes critiques dans de nombreuses applications, notamment en vérification de programmes. Jusqu à maintenant, les algorithmes de filtrage sur les nombres à virgule flottante ont été limités à la B consistance et ses dérivées. Bien que ces filtrages soient conservatifs des solutions, ils souffrent des problèmes bien connus des consistances locales, e.g., leur incapacité à traiter efficacement les occurrences multiples de variables. Leurs limitations proviennent aussi de la pauvreté des propriétés de l arithmétique des nombres à virgule flottante. Afin de pallier à ces limitations, nous proposons dans cet article un nouvel algorithme de filtrage de contraintes sur les flottants qui repose sur des relaxations successives sur les réels du problème initial sur les flottants. Des bornes conservatives des domaines sont obtenues à l aide d un solveur de programme linéaire mixte (MILP) appliquées à des linéarisations conservatives de ces relaxations. Les résultats préliminaires sont prometteurs et montrent que cette approche peut effectivement accélérer les filtrages par consistances locales. Abstract Solving constraints over floating-point numbers is a critical issue in numerous applications notably in program verification. Capabilities of filtering algorithms over the floating-point numbers have been so far limited to b-consistency and its derivatives. Though safe, such filtering techniques suffer from the well known pathological problems of local consistencies, e.g., inability to efficiently handle multiple occurrences of the variables. These limitations also take roots in the strongly restricted floating-point arithmetic. To circumvent the poor properties of floating-point arithmetic, we propose in this paper a new filtering algorithm which relies on various relaxations over the reals of the problem over the floats. Safe bounds of the domains are computed with a mixed integer linear programming solver (MILP) on safe linearizations of these relaxations. Preliminary experiments on a relevant set of benchmarks are very promising and show that this approach can be very effective for boosting local consistency algorithms over the floats. Introduction Les logiciels critiques s appuient de plus en plus sur le calcul en virgule flottante. Par exemple, les systèmes embarqués sont contrôlés par des logiciels qui utilisent des mesures et des données de leur environnement évaluées par des nombres flottants. Les calculs effectués sur ces nombres font l objet d erreurs d arrondi. Ces erreurs d arrondi peuvent avoir des conséquences importantes et même, modifier le flot de contrôle du programme. Ainsi, la vérification de programmes qui effectuent des calculs sur les nombres flottants est un problème clef dans le processus de développement de systèmes critiques. Les méthodes de vérification de programmes numériques sont principalement issues des méthodes classiques de vérification de programmes. La vérification bornée de modèles (BMC) a largement été utilisée pour détecter des bugs lors de la conception de processeurs [3] ou de logiciels [0]. Les solveurs SMT sont aujourd hui présents dans la plupart des outils de BMC pour manipuler directement des formules de haut niveau [, 8, 0]. L outil CBMC de vérification bornée de modèles code chacune des opérations sur les flottants comme une fonction logique sur des vecteurs de bits. Cet encodage nécessite l introduction de milliers de variables additionnelles et rend souvent le problème insoluble [6]. D autres outils basés sur l interprétation abstraite [9, 0] peuvent montrer l absence d erreurs d exécution (e.g., la division par zéro) dans des programmes numériques. Grâce à une sur- approximation du calcul sur les flottants, ces outils sont conservatifs de l ensemble des solutions. Cependant, cette sur-approximation peut être très large et, par conséquent, ces outils rejettent un nombre significatif de programmes valides. La programmation par contraintes (CP) a aussi été utilisée pour la génération de cas de tests [, 3] et la vérification de programmes [7]. La CP offre de multiples bénéfices tels que la capacité de déduire des informations de problèmes partiellement instanciés ou de fournir des contreexemples. La programmation par contraintes est dotée d un cadre très flexible qui facilite l intégration de nouveau solveurs sur des domaines spécifiques comme les solveurs sur les flottants. Notons que les solveurs sur les réels ne sont pas capable de traiter correctement l arithmétique sur les flottants. Des solveurs dédiés et corrects sont donc requis par les outils de programmation par contraintes et de vérification bornée de modèles pour tester ou vérifier des programmes numériques. Les techniques existantes de résolution de contraintes sur les flottants sont basées sur une adaptation des consistances locales sur les réels (e.g. boxconsistance, B-consistance) [9, 8, 5]. Toutefois, ces solveurs peinent à passer à l échelle. C est pourquoi nous introduisons ici une nouvelle méthode qui s appuie sur des solveurs sur les réels pour filtrer des contraintes sur les nombres à virgule flottante. L idée principale est de construire des relaxations fines et conservatives sur les réels pour des contraintes sur les flottants. Afin d obtenir des relaxations fines, chaque opération sur les flottants est approximée selon le mode d arrondi. Par exemple, supposons que x et y sont des nombres flottants positifs normalisés, alors le produit x y, pour un mode d arrondi vers, sera borné par : α (x y) x y x y où α = /( + p+ ) et p est la taille de la mantisse. Nous avons aussi défini des approximations fines pour les autres cas tels que l addition avec un mode d arrondi au plus près ou la multiplication par une constante. À l aide de ces relaxations, le problème initial sur les nombres flottants est tout d abord transformé en un ensemble de contraintes non-linéaires. voir, par exemple, FPSE (http :// carlier/fpse.html), un solveur de contraintes sur les flottants issue de programmes C.. Un nombre flottant x est déterminé par un triplet (s, e, m) où s est son signe, e son exposant et m sa mantisse. Sa valeur est donnée par ( ) s.m e. r et p spécifient le nombre de bits de son exposant et de sa mantisse. Dans la norme IEEE 754, les simples sont définis par (r, p) = (8, 3) et les doubles par (r, p) = (, 5). sur les réels. Une linéarisation des contraintes nonlinéaires est ensuite effectuée afin d obtenir un problème linéaire mixte (MILP) sur les réels. Lors de ce processus, des variables binaires permettent de traiter les parties concaves tout en évitant l utilisation de sur-approximations trop lâches. Ce dernier ensemble de contraintes peut directement être résolu par les solveurs MILP disponibles sur les réels qui, eux, ne sont par limités par l arithmétique des nombres flottants. Les solveurs MILP efficaces utilisent des calculs en virgule flottante et peuvent donc perdre des solutions. Afin d obtenir un comportement correct de tel solveurs, des procédures d arrondi correct sont appliquées aux coefficients des relaxations [7, 4] et la méthode décrite dans [] est utilisée pour calculer un minimum correct à partir du résultat incorrect fourni par un solveur MILP. Les résultats préliminaires sont très prometteurs et montrent que la technique introduite ici peut faciliter le passage à l échelle des outils nécessitant un solveur de contraintes sur les flottants. Notre méthode repose sur une représentation de haut niveau des opérations sur les flottants et ne souffre donc pas des mêmes limitations que celle reposant sur un encodage en vecteur de bits. Cet encodage utilisé par CBMC génère des milliers de variables binaires additionnelles pour chacune des opérations sur les flottants du programme. Par exemple, une addition de deux variables flottantes codées sur 3 bits demande 554 variables binaires [6]. L approximation mixte proposée dans [6] réduit notablement le nombre de ces variables. Mais le système résultant reste encore coûteux en mémoire. Notons qu une simple addition avec seulement 5 bits de précision nécessite encore 035 variables additionnelles. Notre méthode génère aussi des variables additionnelles : des variables intermédiaires sont ajouter afin de décomposer les expressions complexes en en opérations élémentaires sur les flottants et quelques variables binaires permettent de gérer les différents cas de nos relaxations. Cependant, la quantité de variables additionnelles ainsi générées reste négligeable en comparaison de celle requise par le modèle à base de vecteurs de bits.. Un exemple illustratif Avant de détailler notre méthode, illustrons notre approche sur un exemple très simple. Considérons la contrainte suivante : z = x + y x () où x, y et z sont des variables de type flottant sur 3 bits. Sur les nombres réels, cette expression peut évidemment être réduite à z = y. Ce n est pas le cas pour les nombres flottants. Par exemple, sur les flottants et avec un mode d arrondi au plus proche n est pas égal à 0 8 mais à 0. Ce phénomène d absorption montre bien pourquoi les expressions sur les flottants ne peuvent pas être simplifiées de la même manière que les expressions sur les réels. Supposons que x [0.0, 0.0], y [0.0, 0.0] et z [0.0, ]. FPB, un algorithme de B-consistance [5] adapté aux flottants [5], propage les domaines de x et y vers le domaine de z en utilisant l arithmétique des intervalles. La propagation inverse n étant d aucune utilité ici, le processus de filtrage donne : x [0.0, 0.0], y [0.0, 0.0], z [0.0, 0.0] Ce résultat souligne les difficultés des algorithmes de filtrages classiques à traiter les occurrences multiples. Une consistance plus forte comme la 3Bconsistance [5] peut réduire le domaine de z à [0.0, ]. Par contre, la 3Bconsistance ne réussit pas à réduire le domaine de z lorsque x et y ont tous les deux plus de deux occurrences comme dans la contrainte z = x + y x y + x + y x. L algorithme introduit dans cet article construit d abord une relaxation conservative non linéaire sur les réels du problème initial sur les flottants. Appliqué à la contrainte, il produit les relaxations sur les réels suivantes : ( p ( p ))(x + y) tmp tmp ( + p (+ p ))(x + y) ( p ( p ))(tmp x) tmp tmp ( + p (+ p ))(tmp x) z = tmp où p est la taille de la mantisse de la variable flottante. tmp approxime le résultat de l opération x y à l aide de deux plans sur les réels qui capturent les résultats de l addition sur les flottants. tmp fait la même chose pour la soustraction. Certaines relaxations, comme la multiplication, contiennent des termes non-linéaires. Dans ce cas là, un processus de linéarisation des termes non-linéaires est appliqué afin d obtenir un programme linéaire. Une fois le système complètement linéaire, un solveur MILP réduit le domaine de chaque variable en en calculant successivement le minimum et le maximum. FPLP (Floating-point linear programming) est un outil qui implémente l algorithme précédemment esquissé. Un appel à FPLP sur la contrainte () donne le résultat suivant : x [0, 0], y [0, 0], z [0, ] qui est beaucoup plus précis que celui de FPB. Contrairement à la 3B-consistance, FPLP donne le même résultat avec z = x + y x y + x + y x.. Organisation de l article La suite de cet article est organisée comme suit : la section suivante introduit les relaxations non-linéaires sur les réels des contraintes sur les flottants. Le processus de linéarisation des relaxations est ensuite décrit avant de détailler l algorithme de filtrage. Les résultats expérimentaux sont présentés dans la section qui précède la conclusion. Relaxation des contraintes sur les flottants Cette section introduit les relaxations sur les réels des contraintes sur les flottants issues du problème initial. Ces relaxations sont la pierre angulaire du processus de filtrage décrit dans cet article. Elles doivent non seulement être correctes, i.e., préserver l ensemble des solutions du problème initial, mais aussi fines, i.e., inclure le moins possible de flottants non solution. La construction de ces relaxations repose sur deux techniques : l erreur relative et les opérations correctement arrondies. La première de ces techniques est communément utilisée pour analyser la précision du calcul. La seconde propriété est garantie par toute implémentation conforme au standard IEEE 754 de l arithmétique des flottants : une opération correctement arrondie est une opération dont le résultat sur les flottants est égal à l arrondi du résultat de l opération équivalente sur les réels. En d autre terme : soit x et y deux nombres flottants, et, respectivement, une opération sur les flottants et son équivalent sur les réels, si est correctement arrondie alors, x y = round(). La suite de cette section détaille d abord la construction de ces relaxations pour un cas particulier avant de la généraliser aux autres cas. Nous montrons ensuite comment les différents cas peuvent être simplifiés.. Un cas particulier Afin d expliquer comment obtenir ces relaxations, considérons d abord le cas où le mode d arrondi est vers et le résultat de l opération est un nombre flottant positif et normalisé. Un telle opération, dénotée, peut être n importe laquelle des quatre opérations de base de l arithmétique des flottants. Toutes les opérandes sont supposées être du même type, i.e., float, double ou long double. On a alors la propriété suivante : Proposition. Soient x et y, des nombres flottants dont la mantisse possède p bits. Supposons que le mode d arrondi soit fixé et que le résultat de x y soit un nombre positif normalisé strictement inférieur à max float, le plus grand des flottants, alors on a () x y () + p+ où une opération basique sur les nombres flottants et est l opération équivalente sur les nombres réels. Démonstration. Selon la norme IEEE 754, les opérations sont correctement arrondies et le mode d arrondi est fixé à. On a donc : x y (x y) + max float () (x y) +, le successeur de (x y) dans l ensemble des nombres à virgule flottante, peut être calculé par (x y) + = (x y) + ulp(x y) puisque, par définition, ulp(x) = x + x. Il résulte donc de () que x y (x y) + ulp(x y) La seconde inéquation peut être réécrite comme suit : x y + ulp(x y) En multipliant les deux parties de l inéquation par x y qui est un nombre positif on obtient : x y x y + ulp(x y) x y En multipliant chaque partie de l inéquation précédente par et en ajoutant à chaque membre, on obtient x y x y x y + ulp(x y) = ulp(x y) x y + ulp(x y) (3) Considérons maintenant ɛ, l erreur relative définie par ɛ = real value float value real value ɛ est la valeur absolue de la différence entre le résultat sur les réels et le résultat sur les flottants divisé par le résultat sur les réels. Dans notre cas, le résultat de x y étant un flottant positif normalisé, et sachant que x y, l erreur relative est donnée par : 0 ɛ = x y = x y Donc, grâce à (3), on a 0 ɛ ulp(x y) x y + ulp(x y) z, le résultat de l opération x y, est un nombre flottant binaire positif et normalisé qui peut s écrire z =.m z ez, où m z, sa mantisse, a p bits. Par ailleurs, ulp(z) = p+ ez. On a donc, 0 ɛ p+ ez m z ez + p+ = p+ ez m z + p+ La valeur de la mantisse pour un nombre flottant normalisé appartient à l intervalle [.0,.0[. La borne supérieure de l erreur relative ɛ est donnée par le minimum de m z + p qui est atteint lorsque m z =. Donc 0 ɛ p+ + p+ Puisqu on a On a et ɛ = x y 0 x y p+ + p+ p+ 0 x y () + p+ En multipliant chaque partie par et en ajoutant, on obtient finalement. Généralisation () x y + p+ Le tableau donne les relaxations pour les différents modes d arrondi et les différent cas, i.e., les nombres flottants positifs ou négatifs, normalisés ou non. À chaque cas est associée une approximation correcte et fine obtenue de façon similaire à celle détaillée dans la section précédente. Notez que certains cas particuliers permettent d améliorer la précision des relaxations. Par exemple, l addition avec un mode d arrondi vers ± peut être légèrement améliorée. La structure du problème offre aussi des possibilités d amélioration des approximations. Par exemple, x étant calculé exactement 3, cette expression peut directement être évaluée sur les réels. 3. S il n y a pas de dépassement de capacité. Mode d Négatif Négatif Positif Positif arrondi normalisé dénormalisé dénormalisé normalisé vers [( + p+ )z r, z r ] [z r min f, z r ] [z r min f, z r ] [ (+ p+ ) z r, z r ] vers + [z r, (+ p+ ) z r] [z r, z r + min f ] [z r, z r + min f ] [z r, ( + p+ )z r ] [ z r, (+ p+ ) z r ] vers 0 [z r min f, z r ] [z r, z r + min f ] [ (+ p+ ) z r, z r ] au plus près [( + p (+ p ) )z r, [z r min f, [z r min f [( p ( p ) )z r, ( p ( p ) )z r] z r + min f ] z r + min f ] ( + p (+ p ) )z r] Table Relaxations de x y pour chaque mode d arrondi, avec z r =..3 Simplification des relaxations Le principal problème des relaxations précédentes est que le processus de résolution doit traiter les différents cas. Ainsi, pour n opérations élémentaires, le solveur devra potentiellement traiter 4 n combinaisons de relaxations. Afin de diminuer substantiellement cette complexité, nous décrivons ici une combinaison des quatre cas liés à chaque arrondi en une unique relaxation. Considérons d abord le cas où le mode d arrondi est fixé à : Proposition. Soient x et y deux nombres flottants dont la taille de la mantisse est p. Supposons que le mode d arrondi est fixé et que le résultat de x y est tel que max float x y max float. Alors, on a : z r p+ z r min f x y z r où min f est le plus petit nombre flottant positif, et sont, respectivement, une opération arithmétique de base sur les flottants et son équivalent sur les réels, et z r =. Démonstration. La première étape consiste à combiner les approximations des nombres normalisés et dénormalisés. Si z r 0 alors + p+ z r z r. Donc, et + p+ z r min f z r min f + p+ z r min f + p+ z r Il s en suit que : + p+ z r min f x y z r, z r 0 De la même manière, lorsque z r 0, on a : ( + p+ )z r min f x y z r, z r 0 Mode d arrondi Approximation de x y vers [z r p+ z r min f, z r ] vers + [z r, z r + p+ z r + min f ] vers 0 au plus près [z r p+ z r min f, z r + p+ z r + min f ] [z r p ( p ) z r min f, z r + p ( p ) z r + min f ] Table Les relaxations simplifiées de x y pour chaque mode d arrondi.(avec z r = ). Ces deux approximations peuvent être réécrites comme suit : { z r p+ + z p+ r min f x y z r, z r 0 z r + p+ z r min f x y z r, z r 0 Pour combiner les approximations des cas positifs et négatifs, on utilise la valeur absolue : { z r p+ + z p+ r min f x y z r, z r 0 z r p+ z r min f x y z r, z r 0 Puisque max{ p+ + p+, p+ } = p+, on a z r p+ z r min f x y z r Le même raisonnement s applique aux autres cas. Le tableau donne les relaxations simplifiées pour chaque mode d arrondi. Notez que ces approximations définissent un espace concave. 3 Linéarisation des relaxations Les relaxations introduites dans les sections précédentes contiennent des termes non-linéaires qui ne peuvent pas être directement manipulés par un solveur MILP. Cette section décrit comment ces termes sont approximés par un ensemble de contraintes linéaires. 3. Linéarisation de la valeur absolue Les relaxations simplifiées précédentes contiennent des valeurs absolues. Elles peuvent être soit grossièrement approximées par trois inégalités ou implémentées grâçe à une décomposition classique plus fine basée sur une réécriture utilisant des big M : z = z p z n z = z p + z n 0 z p M b 0 z n M ( b) où b est une variable booléenne, z p et z n sont des variables réelles positives, et M est un grand nombre flottant tel que M max{ z, z }. La méthode sépare z p, les valeurs positives de z, de z n, ses valeurs négative
Related Search
Advertisements
Related Docs
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks