Une approche simple du raisonnement autour de la programmation concurrentielle consiste à définir son comportement comme un ensemble de tous les entrelacements possibles des actions atomiques de threads individuels. Cependant, le raisonnement en termes d'entrelacements est trop difficile, non seulement pour les humains, mais aussi les ordinateurs, car le nombre d'entrelacements possibles croît rapidement.

Les modèles concurrentiels sans entrelacement, tels que les langages et les structures d'événements pomset, abordent ce problème en proposant des représentations plus compactes pour l'ensemble des comportements du programme. Au cours de ces dernières années, il y a eu un regain d'intérêt pour les modèles de concurrence sans entrelacement, par exemple, dans le contexte de modèles de mémoire relaxés, de vérification de modèle de programmes concurrents et de tests de mutation basés sur le modèle.

L'objectif de ce projet est de développer une théorie mécanisée des modèles de concurrence sans entrelacement dans l'assistant de preuve Coq. La bibliothèque a pour vocation d'aider les chercheurs intéressés à prouver de façon formelle les propriétés de ces modèles et développer de nouvelles applications de la théorie.

Référentiel de projet