Un cadre d’IA produit un protocole de consensus plus rapide
En termes simples
Le consensus permet à plusieurs ordinateurs de conserver les mêmes données même si certaines machines tombent en panne. L’article présente AI-greement, un ensemble d’outils qui fournit à un agent de programmation des connaissances sur les protocoles de consensus, une structure commune pour les construire et une aide à la vérification de preuves de sûreté.
Avec ces outils, les chercheurs ont développé A-greement pour un magasin clé-valeur répliqué. Dans des tests sans panne avec 5 % d’écritures, sa latence moyenne des requêtes était inférieure à celle des solutions comparées. Ces essais ne montrent toutefois pas comment il se comporterait dans toutes les situations.
La recherche
Un agent de programmation doté d’IA peut-il aider à concevoir des protocoles de consensus, où une modification qui accélère les requêtes peut aussi compliquer la reprise ou compromettre la correction ?
L’article examine si des connaissances propres au domaine, une structure d’implémentation et des vérifications formelles peuvent aider les agents à produire un protocole pratique tout en prenant en compte ces exigences liées.
AI-greement fournit aux agents de programmation des connaissances sur le consensus, une structure d’implémentation réutilisable et des outils Lean pour développer et vérifier des protocoles candidats.
Avec AI-greement, un agent de programmation a produit A-greement. Les chercheurs l’ont comparé à quatre protocoles de consensus en mesurant le temps d’aboutissement des requêtes selon différentes charges, différents nombres de réplicas et différentes topologies réseau.
Dans six déploiements avec 5 ou 9 réplicas, A-greement affichait une latence moyenne inférieure à celle de la solution de comparaison ayant la meilleure moyenne, pour les charges avec 50 % et 5 % d’écritures.
Chaque protocole a été évalué avec la même charge de travail et le même déploiement, ce qui étaye l’existence d’une différence de performance dans ces conditions. Avec 50 % d’écritures, la latence p99 d’A-greement était supérieure à celle de SwiftPaxos.
Les moyennes de latence mises en avant couvrent six déploiements comptant 5 ou 9 réplicas et excluent ceux qui en comptent 13 ou 17, où certaines solutions de référence ont atteint la saturation. La preuve en Lean établit la sûreté du modèle encodé ; les chercheurs doivent vérifier que celui-ci correspond au protocole et à l’implémentation visés.
Analyse
Détails
- Auteurs de l’article original
- Clément Burgelin, Rachid Guerraoui, Zicong Hong, Yinan Hu, Anne-Marie Kermarrec
- Soumis à arXiv
- Licence
- CC BY 4.0