Synthèse quantitative pour des programmes concurrents

Nous présentons une méthode algorithmique pour la synthèse quantitative, consciente de la performance, de programmes concurrents. L'entrée consiste en un programme partiel non déterministe et un modèle de performance paramétrique. Le non-déterminisme permet au programmeur d'omettre quel (le cas échéant) construct de synchronisation est utilisé à un emplacement particulier du programme. Le modèle de performance, spécifié comme un automate pondéré, peut capturer des architectures système en assignant des coûts différents à des actions telles que le verrouillage, le changement de contexte et les accès à la mémoire et au cache. Le problème de la synthèse quantitative consiste à résoudre automatiquement le non-déterminisme du programme partiel afin que la correction soit garantie et que la performance soit optimale. Comme c'est standard pour la concurrence en mémoire partagée, la correction est formalisée "sans spécification", en particulier comme liberté de course ou liberté de blocage. Pour la performance dans le pire des cas (au cas moyen), nous montrons que le problème peut être réduit à des jeux de graphes à 2 joueurs (avec des transitions probabilistes) avec des objectifs quantitatifs. Bien que nous montrions, en utilisant des méthodes de théorie des jeux, que le problème de synthèse est NEXP-complet, nous présentons une méthode algorithmique et une implémentation qui fonctionne efficacement pour des programmes concurrents et des modèles de performance d'intérêt pratique. Nous avons implémenté un outil prototype et l'avons utilisé pour synthétiser des programmes concurrents à états finis qui présentent différents motifs de programmation, pour plusieurs modèles de performance représentant différentes architectures.