Programmation, Concurrence, Mémoire faible, Vérification, Logique de séparation, OCaml

Multicore OCaml ajoute au langage de programmation OCaml le support de la concurrence à mémoire partagée. Ce langage étendu obéit à un modèle faible de la mémoire dont une sémantique opérationnelle a été publiée. On peut alors se demander de quels principes de raisonnement on dispose pour s'assurer de la correction d'un programme écrit en Multicore OCaml. Pour y répondre, on instancie Iris, un descendant moderne de la Logique de Séparation Concurrente, pour Multicore OCaml. On obtient une logique de programme de bas niveau, dont les règles de raisonnement exposent les détails techniques du modèle mémoire. Au-dessus de cette logique, on construit Cosmo, une logique de plus haut niveau dans laquelle on jouit de règles plus simples, au prix d'une légère limitation concernant les programmes qu'on peut vérifier. Cosmo offre des raisonnements naturels à propos des variables non-atomiques si elles sont exemptes de courses de données; à propos des variables atomiques; et à propos de la synchronisation en deux temps (acquisition/relâchement, ou «release/acquire») que ces dernières réalisent. La synchronisation entre fils d'exécution est transcrite de façon concise par un mécanisme de vues de la mémoire, qui permet de s'abstraire du modèle sous-jacent. On illustre l'emploi de cette logique de programme par plusieurs études de cas. On vérifie plusieurs implémentations de verrous vis-à-vis d'une spécification classique. On spécifie et vérifie également une structure de données concurrente élaborée et réaliste: une file concurrente multi-écrivains et multi-lecteurs. Dans chacun de ces cas, la spécification de la structure de données considérée décrit son comportement de synchronisation indépendamment de son implémentation et du modèle mémoire sur laquelle cette implémentation repose. On parvient à ce résultat par l'emploi combiné de vues et de «triplets logiquement atomiques». Ainsi, cette approche de la vérification est modulaire vis-à-vis du modèle mémoire: une application qui utilise ces structure de données comme seul moyen de synchronisation peut être vérifiée sans aucune connaissance du modèle mémoire de Multicore OCaml.