Daily Arxiv

Cette page résume et organise les publications en intelligence artificielle du monde entier.
Les contenus sont synthétisés grâce à Google Gemini et le service est proposé à but non lucratif.
Les droits d'auteur des articles appartiennent à leurs auteurs ou institutions respectives ; en cas de partage, il suffit d'en mentionner la source.

Détection automatisée des violations d'atomicité dans les systèmes à grande échelle

Created by
  • Haebom

Auteur

Hang He, Yixing Luo, Chengcheng Wan, Ting Su, Haiying Sun, Geguang Pu

Contour

Dans cet article, nous proposons Clover, un framework hybride pour la détection des violations d'atomicité dans les programmes pilotés par interruptions. Clover intègre l'analyse statique et un agent de modèle de langage à grande échelle (LLM) pour détecter les violations d'atomicité lorsque l'ordre d'exécution des opérations sur des ressources partagées est perturbé par des interruptions asynchrones. L'analyse statique extrait les fragments de code critiques et les informations opérationnelles, un agent expert utilise les connaissances spécifiques au domaine pour détecter les violations d'atomicité, et un agent juge les vérifie. Les résultats d'évaluation sur RaceBench 2.1, SV-COMP et RWIP montrent que Clover atteint une précision/rappel de 92,3 %/86,6 %, soit 27,4 à 118,2 % de mieux que les approches existantes en termes de score F1.

Takeaways, Limitations

•
Takeaways:
◦
Nous présentons une nouvelle approche du problème de détection des violations d'atomicité en tirant parti des agents LLM.
◦
Il s’avère efficace pour l’analyse de programmes réels en permettant d’obtenir une précision et un rappel améliorés par rapport aux méthodes existantes.
◦
Nous démontrons l’utilité d’une approche hybride d’analyse statique et d’agents LLM.
•
Limitations:
◦
Les performances d’un agent LLM peuvent dépendre du modèle utilisé et des données de formation.
◦
La conception et le développement d’agents experts peuvent s’avérer difficiles lorsque des connaissances complexes et spécifiques à un domaine sont requises.
◦
En raison des limitations de l’ensemble de données d’évaluation, les performances de généralisation pour divers programmes du monde réel nécessitent une validation supplémentaire.
👍
Made with Slashpage