Chroniques de Rox* #2

Étude de cas: le filtre de Bloom

Ce billet fait partie d’une série écrite dans le cadre de mon travail de doctorat, et qui vulgarise la future chaîne de compilation Rox* (Rust-Oxide-F*) dont l’objectif est d’amener à Rust de la vérification déductive. Le contexte complet de ce projet est expliqué dans l’article initial. Le code de cette étude de cas est disponible ici.

Filtre de Bloom à compteur

À l’instar des autres moteurs de navigateur Internet, Servo optimise le rendu CSS des pages Web. Voilà comment ça marche : chaque élément du DOM (Document Object Model) est qualifié par des attributs, comme des classes et des identifiants. De l’autre côté, le style est déclaré par l’utilisateur en associant un sélecteur CSS (une combinaison d’attributs) avec un style particulier. Quand la page Web est rendue, Servo parcourt chaque élément du DOM et essaye de déterminer quel sélecteur CSS peut s’y appliquer. Or, trouver quel sélecteur CSS s’applique à un élément du DOM est cher, et pour optimiser cette étape les moteurs de navigateur Internet utilisent une structure de données auxiliaire appelée filtre de Bloom.

Un filtre de Bloom peut être vu comme un ensemble d’éléments. Vous pouvez y ajouter ou en enlever des éléments, et faire une requête pour savoir si un élément est dedans. Toutes ces opérations ont une complexité asymptotique constante et sont généralement très rapides (le filtre de Bloom peut être implémenté par un simple tableau), c’est donc presque trop beau pour être vrai. En effet, l’opération de requête n’est pas exacte :

  • si la requête retourne false, alors on est sûrs que l’élément requêté n’est pas dans le filtre;
  • si la requête retourne true, alors l’élément est probablement dans le filtre, mais peut-être pas. La probabilité des faux positifs peut être calculée de manière théorique à partir des paramètres du filtre.

Dans Servo, le filtre de Bloom est utilisé de la manière suivante pour chaque élément du DOM : d’abord, on remplit le filtre avec tous les attributs de l’élément du DOM. Puis, pour chaque attribut du sélecteur CSS contre lequel on veut le tester, on requête l’attribut dans le filtre. Si toutes les requêtes renvoient true, alors le sélecteur CSS correspond peut-être à l’élément du DOM, donc on poursuit avec une vérification plus coûteuse. Si au moins une des requêtes retourne false, alors le sélecteur ne peut pas correspondre à l’élément du DOM et l’on peut le rejeter rapidement.

L’implémentation du filtre de Bloom dans Servo est très simple : il s’agit d’un tableau de compteurs qui sont tous des octets. Pour ajouter un élément, on calcule deux index du tableau à partir du hash de l’élément du DOM, et l’on incrémente les compteurs à ces deux index. Le retrait d’un élément est similaire mais décrémente les compteurs. La requête retourne true si et seulement si les deux index ont des compteurs dont la valeur n’est pas nulle. Cependant, cette implémentation simple possède des cas limites ambigus : et si les deux index d’un même élément sont les mêmes? Que se passe-t-il en cas d’overflow ou d’underflow d’un des compteurs? Et si l’on retire un élément qui n’était pas dans le filtre au départ?

Je voulais m’assurer que tous ces cas limites étaient pris en compte dans l’implémentation de Servo, et j’ai ainsi traduit le cœur logique du filtre de Bloom en F*. La propriété qui doit être préservée par toutes les opérations du filtre est : pour chaque élément inséré dans le filtre, la requête pour cet élément doit retourner true. En effet, si cette propriété est préservée par toutes les opérations qui manipulent le filtre, alors elle est toujours vraie. Cependant, il faut se rappeler exactement de tous les éléments qui ont été ajoutés au filtre.

Pour cela, j’ai du quitter l’univers de Rust et me plonger dans F* où j’ai défini une structure de données fantôme, qui représentera l’ensemble exact des éléments que contient le filtre à tout moment. Cette structure de donnée est « fantôme » car elle n’est pas destinée à être implémentée ou exécutée; elle est un artefact de preuve. Étant donné un filtre de Bloom et un ensemble fantôme des éléments qu’il contient, j’ai pu m’atteler à la preuve de la préservation de l’invariant.

Celle-ci représente environ 500 lignes de code F* et m’a pris deux semaines. Elle a été développé manuellement et minutieusement car elle est pleine d’invariants récursifs que Z3 ne peut pas trouver tout seul. Finir la preuve m’a donné trois informations intéressantes sur le fonctionnement du filtre de Bloom :

  1. Afin de prouver la présevration de l’invariant de départ, j’ai en fait du prouver un invariant beaucoup plus fort : « la valeur de chaque compteur dans le filtre est soit MAX_U8, soit est égale à la somme de toutes les fois qu’un élément dont le hash correspond au compteur a été ajouté (moins les fois où il a été retiré), et compté deux fois si les deux index du hash tombent au même endroit ».
  2. Lorsqu’un compteur atteint MAX_U8, celui-ci entre dans un état absorbant où toute requête renvoie toujours true. Cela augmente le taux de faux positifs global du filtre.
  3. Si l’on retire du filtre un élément qui n’était pas vraiment dedans, alors il est possible de casser l’invariant et donc la correction du filtre.

Cette troisième propriété est très intéressante puisqu’elle ajoute une précondition sur la fonction remove du filtre : l’élément retiré doit avoir été ajouté auparavant. En conséquence, le code qui appelle remove doit respecter cette précondition. Dans Servo, le filtre est mis à jour de manière incrémentale au long de la traversée de l’arbre du DOM à l’aide d’un algorithme non-trivial qui a été abondamment commenté par son développeur. Il serait donc intéressant de poursuivre cette étude de cas et de prouver que le mécanisme de mise à jour incrémentale ne viole jamais la précondition du filtre pendant la traversée du DOM.