RacerD devient Open source : Détection rapide de course statique à échelle

La programmation concurrente est ardue. Il est difficile pour les humains de penser au grand nombre d’interactions potentielles entre les processus, ce qui rend les programmes concurrents difficiles à corriger en premier lieu. De plus, les erreurs concurrentes sont difficiles à déboguer et même à reproduire après avoir été observées, et cela requiert beaucoup de temps à corriger.

Chez Facebook, ils ont travaillé sur le raisonnement automatisé de la concurrence dans leur travail avec l’analyseur statique Infer. RacerD, le nouveau détecteur de course open source, recherche des courses de données – des accès mémoire asynchrones, où l’on peut écrire des programmes Java, et cela sans exécuter le programme analysé. RacerD utilise un raisonnement symbolique pour couvrir rapidement de nombreux chemins à travers une application.

Les courses de données sont l’une des formes les plus élémentaires d’erreur de la concurrence, et les supprimer peut aider à simplifier la tâche intellectuelle pour comprendre un programme concurrent. RacerD est en production depuis 10 mois sur leur base de code Android et il a détecté plus de 1000 problèmes multithreads qui ont été résolus par les développeurs de Facebook avant que le code n’atteigne la production. Il a contribué à la conversion d’une partie du fil d’actualités dans l’application Android de Facebook, d’un modèle mono-thread vers un modèle multithread. Ils sont ravis de dire que RacerD est maintenant open source, en tant qu’outil sur leur plate-forme d’analyse statique Infer, qui va vérifier les bogues de concurrence dans le code Java qui utilise des verrous ou des annotations @ThreadSafe. Cet article parle de ce que fait RacerD, des défis qu’ils ont rencontrés pour faire fonctionner un détecteur de course efficace à grande échelle ainsi que des décisions de conception qu’ils ont prises pour faire face à ces défis.

A quel point est-ce difficile ?

La concurrence implique différents threads ou activités dont les exécutions se chevauchent dans le temps.

La raison principale qui fait que la concurrence soit difficile est que lorsqu’il y a deux flux d’instructions comme celui-ci, il y a un nombre incroyable de programmes d’exécution potentiels, trop nombreux à explorer pour un humain ou même pour un ordinateur. Pour avoir une idée de l’ampleur du défi, disons qu’un programme voulait examiner chacune des différentes manières dont deux threads de 40 lignes de code peuvent interagir simultanément («entrelacements», dans le jargon). Même en considérant ces interactions à un rythme fulgurant de 1 milliard d’interactions par seconde, l’ordinateur devrait travailler pendant plus de 3,4 millions d’années ! D’autre part, RacerD fait son travail en moins de 15 minutes, pour des programmes beaucoup plus grands que 80 lignes.

Ce calcul est réalisé en utilisant le fait que le nombre d’entrelacements pour 2 threads avec n instructions chacun est le coefficient binomial C(2n, n). C’est une quantité qui croît extrêmement vite. Par exemple, si vous étendez le nombre d’instructions à seulement 150 par thread, vous obtenez plus de 10⁸⁸ entrelacements, ce qui est supérieur au nombre estimé d’atomes dans l’univers connu (10⁸⁰).

La conclusion inévitable est que, même si les ordinateurs sont puissants, on ne peut pas explorer toutes les possibilités par la force brute.

Lancement du projet

Faire une analyse d’accès à échelle rapide et utile semblait être un problème insurmontable, bien au-delà des connaissances en analyse statique, à leur connaissance.

En 2015, l’un d’entre eux avait énoncé l’objectif global comme suit.

« Je veux toujours comprendre la concurrence, de manière évolutive. Je voudrais avoir des analyses que je pourrais déployer avec une grande vitesse et une faible friction (par exemple, pas d’annotations ou de conseils de preuves) et produire des rapports de haute qualité utiles aux programmeurs écrivant des programmes concurrents sans trop perturber leur flux de travail. Ensuite, cela pourrait évoluer vers de nombreux programmeurs et de nombreux programmes. Peut-être que je demande trop, mais c’est ce que je voudrais trouver. »

Tout au long de l’année 2016, ils ont fait des recherches sur ce problème à l’intérieur de Facebook, créant des algorithmes pour découvrir des preuves de liberté de course, certifiant qu’aucune erreur de course de données ne pouvait survenir dans un programme basé sur la théorie de la logique de séparation concurrente. Cette logique leur permet d’éviter d’énumérer les entrelacements et semble donc prometteuse pour aborder la question de l’échelle.

À la fin de l’année 2016, leur parcours a un peu changé lorsque les ingénieurs travaillant sur le fil d’actualités pour Android à New York ont ​​contacté leur équipe pour demander de tirer parti de leur travail. Ils se lançaient dans un projet majeur : la conversion d’une partie de l’application fil d’actualités Android d’un modèle séquentiel vers un modèle multithread. C’était risqué car la transformation pourrait introduire des erreurs de concurrence. Et ils ont demandés le type d’analyse sur lequel l’équipe travaillait, sauf qu’ils le voulaient le jour d’avant et que ce n’était pas prêt.

Le délai technique qu’ils avaient en tête pour créer leur outil de preuve de la liberté de la course des données était d’environ 1 an pour le lancement d’une preuve de concept, et ensuite il fallait plus de temps pour affiner l’expérience des développeurs. Mais leurs ingénieurs Android avaient des besoins immédiats et urgents, ils étaient sur le point de se lancer dans une partie du fil d’actualité concurrent, et ceci représentait une opportunité en or pour développer un analyseur efficace. Ils avaient donc décidé de pivoter leur recherche, en détournant leur attention de l’objectif idéal prouvant finalement qu’aucune course ne pouvait se produire dans une vastes étendue de code vers l’objectif pratique pour aider les gens dans l’immédiat à trouver rapidement et automatiquement de nombreuses courses dans le code existant avec un signal élevé. Ils ont fait équipe avec Jingbo Yang et Benjamin Jaeger, ingénieurs Android dans le bureau de Facebook à New York, pour déterminer une spécification d’un MVP (modèle-vue-présentation), un produit minimum viable pour RacerD qui répondrait aux besoins de leurs développeurs. Le MVP inclus ce qui suit.

1. Signal élevé : détecter les courses avec un faible taux de faux positifs
2. Interprocédural : possibilité de suivre les courses de données impliquant de nombreux appels de procédure imbriqués.
3. Ne pas se fier aux annotations manuelles pour spécifier quels verrous protègent les bits de données.
4. Rapide, capable de générer des rapports en 15 minutes sur les modifications apportées à une base de code de millions de lignes, afin d’intercepter les régressions de concurrence lors de la révision de code.
5. Traitement précis du verrouillage à gros grain, tel qu’utilisé dans la plupart des codes de produit, mais pas de traitement précis de la synchronisation complexe à grain fin (la minorité, et en changeant moins fréquemment).

Le MVP était essentiel pour déterminer sur quoi se concentrer et sur quoi ne pas se concentrer. Par exemple, l’une des premières étapes techniquement les plus simples de l’analyse statique de concurrence consiste à exiger que les champs soient protégés par des annotations, puis à demander à l’analyseur de vérifier ces annotations. Même si c’est facile pour le concepteur d’analyse, cela déplace l’effort de l’analyseur vers l’humain et aurait été inacceptable pour le travail de rendu du fil d’actualités multithread : L’équipe du fil d’actualités devait refactoriser plusieurs milliers de lignes de code, et ils avaient besoin de comprendre où se trouvait les problèmes de concurrence éventuels quant ils le faisaient fonctionner. Il aurait fallu beaucoup plus de programmeurs pour le faire manuellement, même trop – c’est mieux que l’ordinateur effectue cette recherche.

Ce pivot était important pour convertir un problème insoluble en un problème qu’ils pourraient faire évoluer progressivement.

Dans le reste de cet article, vous allez plonger dans certaines des considérations techniques qui ont conduit leur travail. Mais, vous allez d’abord entrer dans la conception et la théorie de l’analyseur, puis passer à la perspective de l’utilisateur final.

Considérations et décisions de design

L’objectif de RacerD est de trouver des courses de données. Sa conception est basée sur les idées suivantes :

1. Ne pas faire l’analyse du programme complet ; être compositionnel.
2. Ne pas explorer les entrelacements; Verrouillage de la piste et informations sur le thread.
3. Ne pas tenter une analyse d’alias générale et précise; utiliser une analyse de propriété agressive pour l’anti-aliasing des ressources allouées.

La première décision est essentiellement une requête imposée par la nécessité d’exécuter RacerD dans un modèle de déploiement « rapide » sur lequel il empêche les régressions au moment de la révision du code. Dans une analyse de composition, les résultats d’analyse des éléments sont réalisés sans connaître l’ensemble. Cela ouvre la voie sur l’analyse de fragment de code (par exemple, le changement de code en cours de révision) sans connaître le contexte dans lequel il s’exécutera. Ceci est utile pour vérifier le code des problèmes de sécurité du thread avant de le placer dans un contexte concurrent. Il est également assez simple de paralléliser une analyse de composition et de l’adapter au grand code, ce qui est important compte tenu de la taille des bases de code sur Facebook.

Les deux décisions suivantes proviennent de l’observation de la difficulté pour équilibrer la précision et l’évolutivité dans l’histoire de l’analyse de programme pour la concurrence. Leur analyse diffère de la plupart des travaux antérieurs dans la mesure où ils ne cherchent pas à prouver une certaine absence de courses, mais plutôt (dans certaines circonstances) à prouver leur présence; ils favorisent la réduction des faux positifs par rapport aux faux négatifs. Cela présente des défis différents, mais permet aussi de faire des compromis qui ne seraient pas justifiés si l’objectif était de montrer l’absence de courses.

Plus tôt, ils ont discuté de la difficulté de calcul pour explorer les entrelacements dans l’analyse de programme. La théorie de la logique de séparation concurrente montre qu’ils peuvent aller étonnamment loin avec un raisonnement purement séquentiel; cela implique de prendre l’extrême mesure de ne pas explorer l’ensemble des entrelacements, mais de suivre les propriétés qui sont exactes à l’intérieur et à l’extérieur du verrouillage. RacerD suit cette idée en utilisant une simple abstraction booléenne pour déterminer si un verrou doit être conservé au moment d’un accès et si un accès doit avoir lieu sur le thread principal. C’est génial pour trouver des bogues avec une grande confiance.

L’analyse d’alias précise est un problème classiquement difficile même pour les programmes séquentiels. Parce qu’ils se concentrent sur la recherche de courses définies, ils peuvent s’en passer sans une analyse précise pour dire à quel moment les paires arbitraires d’accès peuvent être des alias. Mais, Ils utilisent un raisonnement de propriété compositionnelle qui leur donne une quantité minimale mais importante d’informations anti-alias. Une cellule qui est possédée ne peut pas être accessible à partir d’un autre thread, et ne peut donc pas être impliqué dans une course. Après avoir éliminé les accès aux cellules possédées, ils signalent les accès conflictuels entre les cellules avec des chemins d’accès syntaxiques identiques (par exemple, x.f.g). Cela peut délaisser les courses qui peuvent se produire via des chemins d’accès distincts qui font référence à la même mémoire, mais cela simplifie énormément l’analyse et leur permet de se concentrer sur la recherche de courses probables. (La documentation de RacerD contient une liste complète de ses limitations.)

Le raisonnement RacerD

Pour illustrer certaines des principales caractéristiques du raisonnement de RacerD, il y existe quelques exemples, en commençant par les threads et les verrous.

Threads et serrure

Le premier exemple est motivé par un commentaire du fichier Components.java dans la base de code Litho github.com/facebook/litho :

// Ce [champ] est écrit uniquement par le thread principal avec le verrou maintenu, lu en même temps à partir du thread principal

// aucun verrou n’est maintenu, ou lu à partir d’un autre thread avec le verrou maintenu.

Ce commentaire indique un modèle dans lequel les informations de thread sont utilisées pour limiter la quantité de synchronisation requise. Voici quelques exemples de code pour illustrer cette idée.

@ThreadSafe
class RaceWithMainThread {
  int i;

  void protected_write_on_main_thread_OK() {
    OurThreadUtilsassertMainThread();
    synchronized (this) {
      i = 99;
     }
  }

  void unprotected_read_on_main_thread_OK() {
    int x;
    OurThreadUtilsassertMainThread();
    x = i;
  }

  void protected_read_off_main_thread_OK() {
    int x;
    synchronized (this) {
      x = i;
    }
  }
}

Ici, @ThreadSafe est considéré comme une instruction vers l’analyseur pour vérifier toutes les méthodes non-privées d’un thread pour les courses potentielles entre eux. Si l’on exécute RacerD sur ce code, il n’y a pas de problème.

$ infer --racerd-only -- javac RaceWithMainThreadjava

..

Aucun problème n'a été trouvé

La lecture non protégée et l’écriture protégée ne s’affrontent pas car on sait qu’elles sont sur le même thread, comme cela est dûment consigné dans leurs résumés.

$ infer-report
 ... protected_write_on_main_thread_OK() Accesses { ProtectedBy(both Thread and Lock) -> { Write to &thisRaceWithMainThreadi at at [line 51] } }  ... unprotected_read_on_main_thread_OK() Accesses { ProtectedBy(Thread) -> { Read of &thisRaceWithMainThreadi at at [line 58] } }  ...

D’un autre côté, si on inclut des méthodes supplémentaires, on obtient des courses potentielles.

void protected_write_off_main_thread_Bad() {
  int i;
  synchronized (this) {
    i = 99;
  }
}

void unprotected_read_off_main_thread_Bad() {
  int x;
  x = i;
}

RaceWithMainThreadjava:77: error: THREAD_SAFETY_VIOLATION  Read/Write race Non-private method `RaceWithMainThread.unprotected_read_off_main_thread_Bad` reads from `RaceWithMainThread.i` Potentially races with writes in methods `{ void RaceWithMainThread.protected_write_off_main_thread_Bad(),  void RaceWithMainThread.protected_write_on_main_thread_OK() }`   75. void unprotected_read_off_main_thread_Bad() {  76. int x;  77. >  x = i;  78. }  79.  RaceWithMainThreadjava:58: error: THREAD_SAFETY_VIOLATION  Read/Write race Non-private method `RaceWithMainThread.unprotected_read_on_main_thread_OK` reads from `RaceWithMainThread.i` Potentially races with writes in method `void RaceWithMainThread.protected_write_off_main_thread_Bad()`  56. int x;  57. OurThreadUtilsassertMainThread();  58. >  x = i;  59. }  60. 

Concurrence à grain fin

Pour le prochain exemple, il y a la concurrence à granularité fine.

Si on exécute ceci :

@ThreadSafe
public class DCL {
  private Object o;

  public Object LazyInit(){
   if (o == null) {
     synchronized (this){
       if (o == null) {
         o = new Object();
       }
     }
   }
   return o;
  }
}

RacerD trouve un bug :

DCLjava:36: error: THREAD_SAFETY_VIOLATION  Read/Write race Non-private method `DCL.LazyInit` reads from `DCL.o` Potentially races with writes in method `Object DCL.LazyInit()`  35. }  36. >  return o;  37. }

Ce bogue est en fait un bogue classique en Java, appelé  » verrouillage à double contrôle ». Le correctif est de marquer o volatile, puis RacerD ne rapporte pas.

RacerD a attrapé les bogues de cette forme qui ont ensuite été corrigés avant d’atteindre la production dans le code Facebook. Cependant, il y a des bogues reliés qu’il ne trouve pas. Si on supprime l’instruction interne ‘if’ tout en maintenant le volatile, alors on a encore une course. Mais Infer ne rapporte pas : un faux négatif.

Rappelez-vous au-dessus de la détermination à aller après des erreurs de verrouillage à gros grain et non à grain fin. La sémantique de ‘volatile’ est assez compliquée, donc si vous marquez un champ volatile, on suppose que vous savez ce que vous faites et que vous ne rapportez aucune course. Ils ont pris la décision dans RacerD de ne pas y rapporter les courses ‘volatile’ : traiter les ‘volatile’ avec précision le ferait. C’est une heuristique incroyablement efficace, car c’est presque toujours sur la partie volatile du verrouillage à double vérification que les gens se trompent, et non les gardes.

Ce n’est pas que le traitement précis des ‘volatile’ est impensable, mais c’est plutôt qu’ils ont décidé qu’il y a des éléments plus prioritaires dans le développement d’un analyseur pour servir les développeurs. Cette décision illustre le 5e point dans la spécification MVP ci-dessus, qui évite d’abord la concurrence à granularité fine. Ce compromis a été pris pour faire progresser et il peut être revisité.

Pour la facilité d’exposition, tous les exemples montrés ici impliquent des courses entre une ou deux procédures qui accèdent directement aux données en question. En pratique, les courses se produisent souvent entre deux procédures qui accèdent aux données indirectement via une chaîne d’appels profonde. En effet, le raisonnement interprocédural était l’une des premières demandes des ingénieurs de Facebook, car souvent la racine de l’arborescence utilisée dans la représentation d’une interface utilisateur appartient à une classe mais des changements surviennent sur plusieurs couches dans la pile des appels d’une classe différente.

La propriété

Le suivi de la propriété dans ce domaine abstrait a aidé à faire passer l’analyse à un niveau élevé. Le problème principal est qu’il pourrait avoir des accès identiques mais qui ne courent pas parce qu’ils impliquent un nouvel objet alloué.

Voici une classe qui montre les problèmes de base :

@ThreadSafe
class Ownership {

  int x;
  Ownership oo = new Ownership();

  void unprotected_owned_write() {
    Ownership o = new Ownership();
    ox = 88;
  }

  void unprotected_unowned_write() {
    Ownership o = oo;
    ox = 99;
  }
}

Dans le premier cas, l’écriture o.x = 88 est à un champ d’un nouvel objet alloué, et aucun processus ne peut courir avec lui. Dans le second cas, l’écriture o.x = 99 est en fait une écriture dans un champ de l’objet oo, et il peut courir avec d’autres processus; en particulier, il y a auto-course si cette méthode est exécutée en parallèle avec elle-même.

RacerD suit la propriété, et il est agressif sur la suppression des accès aux objets possédés. Par exemple, le résumé de unprotected_owned_write() n’enregistre aucun accès.

Il faut être clair sur le fait que si l’approche de la suppression des accès possédés est importante pour l’objectif principal de la limitation des faux positifs, elle peut également conduire à des faux négatifs. Considérez :

@ThreadSafe
public class PointerTransferringBuffer {

  A contents;

  public void m0() {
    A newa = new A();
    synchronized(this){
      contents = newa;
    }
    newadata = 88;
  }

  public void m1() {
    A transferreda;
    ThreadUtilsassertMainThread();
    synchronized(this){
      transferreda = contents;
    }
    //assertMainThread rules out the self race
    transferredadata = 99;
  }
}

Ici, les assignations newa.data = 88 et transfera.data = 99 sont en course les unes avec les autres, mais RacerD ne parvient pas à le signaler; la raison est que les accès à newa.data sont supprimés du résumé de m0().

D’un autre côté, si l’affectation à newa.data est supprimée du programme et non seulement du résumé, alors vous avez un programme sûr présentant le phénomène du transfert de propriété. Il n’est pas impossible pour les techniques automatisées de traiter avec précision des exemples comme celui-ci. En effet, la logique de séparation concurrente démontre des programmes comme celui-ci, et les outils basés sur celui-ci (par exemple, Smallfoot) peuvent certifier la liberté de la course. Le langage de programmation Rust a également des règles de typage pour gérer le transfert de propriété. Cependant, le coût dans ces cas est sur le niveau supplémentaire d’annotations, ce qui en effet indique l’analyseur des informations sur les objets qui sont transférés.

Des exemples de transfert de propriété comme celui-ci se produisent dans le code Java de Facebook, par exemple dans ComponentTree.java de github.com/facebook/litho, mais ils ont tendance à apparaître dans un framework plutôt que dans un code produit (pour la majorité). Ici, leur priorité a été de servir la majorité en premier (illustrant encore le 5^e point du MVP), mais ils prévoient d’intégrer le transfert de propriété dans une future version de leur analyseur.

Le déploiement

RacerD est implémenté comme une analyse de programme spécialisée utilisant le framework d’analyse Infer.AI. Le framework fournit une API dans l’infrastructure d’analyse de composition en arrière-plan d’Infer, basée sur une interprétation abstraite. Vous décrivez un «domaine abstrait», des valeurs symboliques que l’analyse doit suivre, un moyen de transformer ces valeurs par des instructions de programme, et un moyen de faire une spécification ou un «résumé» d’une procédure indépendante de son programme. Ceci fait apparaître une analyse de programme qui fonctionne de manière compositionnelle et qui peut (souvent) évoluer vers un gros code.

Infer est utilisé sur Facebook dans un déploiement en mode batch et en tant que robot participant à la révision de code. Dans les développeurs de déploiement par lots, souvent ceux qui sont spécifiquement intéressés à détecter les erreurs de sécurité des threads avant de placer le code dans un contexte concurrent, exécutent RacerD sur une classe et résolvent autant d’avertissements que possible. Dans le déploiement de la révision de code, Infer fonctionne dans le cadre du système d’intégration continue (CI) de Facebook. Pour chaque changement de code soumis par un développeur, le CI exécute Infer aux côtés d’autres tâches de compilation et de test. Ce déploiement s’applique à tous les développeurs Android, qu’ils envisagent ou non la concurrence, et vise à intercepter les régressions de threads: Infer ne signale que les bogues introduits par chaque changement de code.

Tout compte fait, des centaines de classes ont été vérifiées dans le déploiement en mode batch, et plus de 1000 problèmes d’analyseur ont été traités en batch et CI combinés (avec la majorité étant CI). Les problèmes abordés se divisent entre les changements non-fonctionnels où les annotations sont ajoutées aux hypothèses de threads de document et aux changements fonctionnels qui évitent les courses, chaque catégorie ayant connu des corrections numérotées par centaines.

Pour qu’Infer soit efficace dans le cadre du CI, l’analyse doit signaler les problèmes rapidement et utiliser efficacement les ressources. On a trouvé que l’analyse de la composition était essentielle pour répondre à ces exigences. Avec une analyse de l’ensemble du programme, la seule façon évidente d’analyser un changement de code est de réanalyser toute l’application. Sur une machine beaucoup plus puissante que celles utilisées dans le CI, lancer Infer sur l’application Facebook Android prend environ 130 minutes. Sur les changements de code, Infer peut fonctionner beaucoup plus rapidement.

Sur un graphique qui montre la distribution des durées d’exécution d’Infer sur un code modifié sur une période d’une semaine, on peut voir qu’un changement de code moyen est analysé en moins de 12 minutes, jusqu’à 10 fois plus vite que l’analyse de l’application entière ! Ceci est possible grâce à la combinaison de l’analyse compositionnelle et du cache distribué du système de construction Buck de Facebook, un cache sur lequel Infer se faufile.

Conclusion

Le raisonnement sur la concurrence a été étudié pendant plus de 40 ans et a connu de nombreux progrès de recherche. Cependant, une grande partie du travail n’a pas été déployée jusqu’à un déploiement dans lequel il peut aider les programmeurs dans leurs tâches quotidiennes.

RacerD démontre qu’une analyse de concurrence statique peut être développée et appliquée efficacement à la vitesse et à l’échelle exigées par le modèle de développement de Facebook, dans lequel une grande base de code subit de fréquentes modifications. L’analyse a un haut degré d’automatisation, quand la relation entre les threads, les verrous et la mémoire est découverte plutôt qu’être spécifiée par une personne ; cela signifie qu’il peut immédiatement évoluer vers de nombreux programmeurs à faible friction. Sans ces caractéristiques – vitesse, échelle et faible friction – l’application supportant le fil d’actualités, où plus de 1 000 problèmes ont été traités avant que le code ne soit placé dans un contexte concurrent, n’aurait pas été viable.

La concurrence en général reste un problème fondamental et difficile, mais ces résultats donne de l’espoir : avec suffisamment d’innovation, plus de techniques et d’outils pourraient être développés pour aider les programmeurs à relever les défis de l’ingénierie des systèmes concurrents.