Multi-Agent Smart Solver (MASS)

Systerel présente le nouveau venu dans la famille Systerel Smart Solver : Multi-Agent Smart Solver (MASS). MASS permet de bénéficier des apports des clusters de calcul pour réduire significativement la durée de preuve perçue par l’utilisateur.

Systerel Smart Solver est basé sur la technologie SAT. Après un bref rappel de cette technologie, cet article présentera les résultats obtenus avec MASS, une approche de déploiement de Systerel Smart Solver sur des clusters de calcul.

SAT, vous avez dit SAT ? Pour des applications industrielles ?

SAT est une abréviation pour Boolean SATisfiability problem, encore appelé propositional SATisfiability problem.

Résoudre un problème SAT revient à déterminer face à une formule booléenne s’il existe une assignation de ses variables qui rend cette formule vraie (évaluable à TRUE, on parle alors de formule satisfiable) ou si au contraire, quelle que soit l’assignation considérée, la formule s’évalue toujours à FALSE (la formule est dite unsatisfiable).

Un problème SAT est un probléme de décision NP-complet. Il n’existe pas à ce jour d’algorithme connu qui sache trouver efficacement une solution à tout problème SAT.

Notre solution Systerel Smart Solver a fait le choix de la technologie SAT en dotant son moteur de preuve d’heuristiques pertinentes pour la plupart des problèmes industriels de nos clients, en particulier dans le domaine de la signalisation ferroviaire. Notre moteur permet d’étudier les propriétés de sécurité de systèmes complexes et critiques tels que des postes de manoeuvre de signalisation (urbain comme grande ligne) ou des pilotages automatiques de métro (Zone Controler d’un CBTC).

Systerel travaille en permanence à améliorer les performances de son moteur pour accompagner les besoins de l’industrie. Un critère de performance concerne les temps de preuve perçus par l’utilisateur. En effet, la complexité des systèmes critiques augmente. Le moteur de preuve doit donc évoluer pour pouvoir traiter des modèles de plus en plus conséquents. De plus, plus les temps de preuve sont courts, plus la preuve contribue à réduire les plannings de mise en service de systèmes critiques.

Naturellement, la course à la performance doit préserver la qualité de la démonstration de la sûreté de fonctionnement.

Un premier axe consiste à rendre les solveurs plus performants tout en maintenant du déterminisme. Les solveurs SAT étant mathématiquement chaotiques, le déterminisme s’obtient parfois au détriment de la performance brute. C’est cependant impératif pour offrir une maintenance industrielle. C’est donc un critère fort dans les choix de conception de Systerel Smart Solver. Notre portfolio qui met en collaboration plusieurs solvers respecte ces choix.

Un autre axe consiste à distribuer la preuve quand des groupes de propriétés peuvent être analysées séparément. Multi-Agent Smart Solver (MASS) apporte une première réponse dans cette direction. MASS distribue les analyses sur plusieurs agents, chaque agent pouvant exploiter plusieurs coeurs d’une machine et ainsi faire tourner un portfolio.

Afin de faciliter l’adoption de MASS, Systerel s’est donné plusieurs contraintes :

  • pouvoir déployer cette solution sur des clusters propriétaires
  • pouvoir déployer cette solution sur des clusters accessibles dans un cloud loué
  • améliorer les temps de preuve perçus

Des premiers chiffres prometteurs

La première version de MASS a été testée sur des cas industriels réels. Les expérimentations menées permettent de conclure sur plusieurs points importants pour l’utilisateur :

  • le passage à l’échelle de la solution,
  • l’accélération obtenue,
  • la flexibilité supplémentaire offerte pour désengorger des serveurs de preuve.

Avant de présenter les résultats, abordons quelques concepts utilisés pour caractériser les gains de peformance :

  • Wall clock time : le temps perçu par l’utilisateur entre le début et la fin des analyses,
  • Total time : la somme des temps de chaque analyse ; le Total time serait le Wall clock time d’un cluster constitué d’un seul agent,
  • Acceleration : le facteur d’accélération par rapport à une approche mono agent ; Acceleration=Total time/Wall clock time,
  • Cluster load : le taux d’usage des agents, i.e. Acceleration / nn est le nombre d’agents du cluster ; ce taux est une mesure d’efficacité de la distribution ; plus il est proche de 1, plus les agents du cluster ont contribué à faire avancer la preuve.

Dans nos expérimentations et mesures, les analyses ont d’abord été distribuées selon l’ordre défini par les cas réels afin de calculer l’Acceleration apportée par les multiples agents de MASS comparée à la solution mono machine. De cet ordre et des mesures initiales associées, un ordre amélioré a été étudié afin de confirmer la capacité à proposer dans le futur des heuristiques sur l’ordre permettant une accélération maximale. A cette fin, cet ordre amélioré a été comparé à l’ordre initial.

Des expérimentations ont également été menées sur des clusters dotés d’agents différents (des machines HPC de Systerel à 40 coeurs totalisant 320GB de RAM et des machines Google Cloud à 60 coeurs totalisant 240GB de RAM).

Enfin, nous avons pu mesurer l’apport d’une nouvelle stratégie appelée Réduction ajoutée à Systerel Smart Solver.

Les résultats sont les suivants :

Résultats

Ces résultats illustrent plusieurs choses :

  • L’ordre initial donne une Cluster load proche de 80% et une accélération ressentie au niveau utilisateur d’un facteur ~7.9.
  • L’ordre amélioré permet d’utiliser le cluster à 99.9% et donne ainsi une accélération linéaire quasiment égale au nombre d’agents du cluster.
  • La stratégie de réduction appliquée à l’ordre initial réduit de plus de 20% le Total time et monte le Cluster load à 94%
  • Les fermes de machines HPC de Systerel sont plus performantes que le cluster Google utilisé mais entre les deux types de cluster, la différence perçue est d‘1/4 de journée. A cette échelle, le recours à des clusters loués pour lisser des besoins de calcul ponctuellement est une option crédible et très flexible.

Avec cette première version, des analyses qui prenaient plus de 12 jours sont désormais accessibles en un peu plus d’une journée.

Ressources

En travaillant les données de consommation des ressources mesurées, il est visible qu’il est possible de réduire encore le Wall clock time. En déployant 20 agents au lieu de 10, le Wall clock time serait encore descendu en conséquence.

En résumé,

  • un run de MASS selon l’ordre initial accélère le temps de preuve dans un rapport 8
  • par l’expérience et la mise au point sur des exemples plus petits, il est possible d’améliorer encore cette accélération significativement
  • le passage à l’échelle sur des clusters loués dans le commerce permet d’envisager une extension de la capacité de preuve voire de ne pas investir sur des machines dédiées

De nouvelles fonctionnalités à venir

Cette première version de MASS offre déjà des gains significatifs. Mais ce n’est qu’une première étape.

La distribution permet intrinsèquement une reprise sur erreur en cas de coupure des serveurs sans perdre tout ce qui a déjà été analysé.

Par une couche légère de configuration, nos équipes peuvent mettre en place un reporting (par mail par exemple) de la progression de la preuve.

Nos équipes peuvent également aider à organiser les analyses, les retravailler pour en casser la complexité pour bénéficier sur les runs ultérieurs d’ordres optimisés.

La roadmap de MASS prévoit une dimension graphique, à travers une IHM de suivi. Elle intègre aussi des fonctionnalités d’apprentissage afin de proposer des ordres optimisés d’analyse sur des familles d’analyse et de compétition entre analyses (e.g. pour permettre à des stratégies incompatibles d’être lancées et arrêtées dès que la meilleure a convergé).

Pour en savoir plus, contactez-nous.

Commentaires