💻 computer science

Reasoning about concurrent loops and recursion with rely-guarantee rules

Cet article présente des règles de raffinement générales, vérifiées mécaniquement, pour le raisonnement sur les programmes récursifs et les boucles while dans les systèmes concurrents en utilisant l'approche rely-guarantee, sans supposer l'atomicité de l'évaluation des expressions.

Auteurs originaux : Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

Publié 2026-06-12

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez d'écrire une recette pour une équipe de chefs travaillant dans une cuisine partagée et chaotique. Tout le monde est en train de hacher, de remuer et de goûter en même temps. Le problème est que, pendant que le Chef A lit une étape de la recette, le Chef B pourrait s'immiscer, déplacer un ingrédient, changer la température ou même cacher un ustensile. C'est le monde de la programmation concurrente : plusieurs programmes s'exécutent en même temps, perturbant les données les uns des autres.

Ce document de Hayes, Meinicke et Jones est comme un nouveau manuel de règles ultra-strict pour écrire ces recettes afin de garantir qu'elles fonctionnent, même dans le chaos. Ils se concentrent sur deux types spécifiques d'instructions de cuisine : les boucles (faire quelque chose encore et encore) et la récursion (une recette qui s'appelle elle-même pour résoudre une partie plus petite du problème).

Voici la décomposition de leurs « règles de cuisine » en utilisant des analogies simples :

1. Le pacte « Rely-Guarantee » (Dépendance-Garantie)

Dans une cuisine normale, vous pourriez simplement faire confiance au fait que personne ne touchera à votre casserole. Dans ce document, les auteurs disent : « La confiance ne suffit pas. Nous avons besoin d'un contrat. »

La condition de Dépendance (La liste des « Ne pas toucher ») : Avant de commencer votre tâche, vous supposez que les autres chefs respecteront certaines règles. Par exemple : « Je compte sur le fait que personne n'ajoutera de sel à ma soupe pendant que je la goûte. »
La condition de Garantie (La liste des « Je promets ») : En retour, vous promettez que vous suivrez aussi des règles. « Je garantis que je ne lancerai jamais ma cuillère contre le mur. »
La Magie : Si tout le monde respecte ses contrats de « Dépendance » et de « Garantie », toute la cuisine fonctionne sans accroc, même si tout le monde travaille en même temps.

2. Le problème des hypothèses « Atomiques »

De nombreux anciens manuels de règles supposaient que lorsqu'un chef lit une étape de la recette, il le fait instantanément, comme un claquement de doigts magique. Ils supposaient que le chef lit « Ajouter 2 œufs » et les ajoute avant que quiconque ne puisse cligner des yeux.

Les auteurs disent : « Non, ce n'est pas ainsi que fonctionnent les vraies cuisines. »
En réalité, lire « Ajouter 2 œufs » prend du temps. Pendant que le chef tend la main vers les œufs, un autre chef peut déplacer la boîte. Ce document construit des règles qui tiennent compte de cette réalité désordonnée. Ils ne supposent rien qui se passe instantanément ; ils supposent que tout prend un peu de temps et peut être interrompu.

3. Dompter la boucle « While » (Le mélange interminable)

Une boucle « while » est comme un chef remuant une casserole « jusqu'à ce que la sauce épaississe ».

L'ancien problème : Dans une cuisine partagée, un chef peut remuer, vérifier la sauce et décider qu'elle n'est pas encore épaisse. Mais pendant qu'il marche vers la cuisinière, un autre chef pourrait ajouter de l'eau, la rendant à nouveau liquide. Le premier chef pourrait continuer à remuer indéfiniment, ou s'arrêter quand il ne le devrait pas.
La nouvelle règle (Terminaison précoce) : Les auteurs introduisent une astuce ingénieuse appelée « Terminaison précoce » (Early Termination).
- Imaginez que le chef possède un minuteur (un « variant »). Chaque fois qu'il remue, le minuteur descend.
- Habituellement, le chef doit remuer pour que le minuteur descende.
- Le rebondissement : Si un autre chef ajoute accidentellement de l'eau (interférence), le minuteur pourrait descendre plus vite que prévu, ou la sauce pourrait soudainement devenir assez épaisse pour que la boucle doive s'arrêter.
- La nouvelle règle permet à la boucle de s'arrêter plus tôt si l'environnement (les autres chefs) aide à terminer le travail, plutôt que de forcer la boucle à faire tout le travail elle-même. C'est comme dire : « Si la sauce est déjà épaisse parce que quelqu'un d'autre a aidé, vous pouvez arrêter de remuer immédiatement. »

4. Dompter la Récursion (La recette qui s'appelle elle-même)

La récursion est comme un chef qui dit : « Pour faire ce gros ragoût, je dois d'abord préparer un petit lot de bouillon. Pour faire ce bouillon, je dois préparer un tout petit peu de fond... »

Le défi : Dans une cuisine partagée, si le Chef A prépare le bouillon, le Chef B pourrait voler la marmite de fond.
La solution : Les auteurs ont créé une « échelle » mathématique (une relation bien fondée). Imaginez que le chef descend une échelle pour résoudre des problèmes de plus en plus petits.
- La règle : Vous ne pouvez descendre l'échelle que si vous êtes sûr de ne pas rester coincé.
- L'astuce de l'« Sortie précoce » : Tout comme pour les boucles, si les autres chefs vous aident à atteindre le bas de l'échelle plus rapidement (en résolvant un sous-problème pour vous), vous êtes autorisé à descendre l'échelle plus tôt. Vous n'avez pas à effectuer chaque étape vous-même si l'environnement vous aide à terminer.

5. L'« Aczel Trace » (La caméra de surveillance de la cuisine)

Pour prouver que leurs règles fonctionnent, les auteurs utilisent un concept appelé « trace d'Aczel ».

Imaginez une caméra de surveillance enregistrant la cuisine.
La caméra enregistre deux types de mouvements : les mouvements du programme (ce que le chef que vous observez fait) et les mouvements de l'environnement (ce que les autres chefs font).
Les règles des auteurs garantissent que peu importe la façon dont la caméra enregistre le chaos, si les contrats de « Dépendance » et de « Garantie » sont respectés, le plat final sera parfait.

Résumé

Ce document fournit une nouvelle façon robuste d'écrire des instructions pour des programmes informatiques qui s'exécutent simultanément.

Pas de magie : Il cesse de supposer que les choses se passent instantanément.
Contrats : Il utilise la « Dépendance » et la « Garantie » pour gérer les interactions entre les programmes.
Flexibilité : Il permet aux boucles et aux fonctions récursives de s'arrêter plus tôt si l'environnement les aide à finir, évitant ainsi qu'elles ne restent bloquées dans des boucles infinies ou qu'elles n'échouent à cause d'une interférence.

Les auteurs ont déjà testé ces règles à l'aide d'un assistant de preuve informatique (Isabelle/HOL), qui agit comme un professeur de mathématiques extrêmement strict, vérifiant chaque étape pour s'assurer que la logique est irréprochable. Ils n'ont pas seulement deviné ; ils ont prouvé que cela fonctionne.

Résumé technique : Raisonnement sur les boucles récursives et la récursion avec les règles de Rely-Guarantee

Énoncé du problème

La vérification des programmes concurrents, particulièrement ceux impliquant des structures récursives et des boucles while, présente des défis importants lorsqu'il s'agit de gérer l'interférence de threads parallèles. Les règles traditionnelles de vérification de Hoare pour les boucles reposent sur des invariants et des expressions de variante pour prouver la correction et la terminaison. Cependant, dans un contexte concurrent, l'interférence peut invalider les invariants de boucle, augmenter les expressions de variante ou perturber l'évaluation des gardes de boucle, rendant ainsi invalides les règles séquentielles standards.

De plus, de nombreuses approches de Rely-Guarantee (RG) existantes supposent que l'évaluation des expressions est atomique. Cette hypothèse ne reflète pas la réalité des implémentations de langages de programmation, où les expressions peuvent impliquer plusieurs accès à des variables partagées qui peuvent être entrelacés avec des transitions d'environnement. Cette hypothèse d'atomicité brise la chaîne de raisonnement formel pour les expressions complexes et limite l'applicabilité des règles de vérification.

Méthodologie

Les auteurs développent un cadre pour raisonner sur les programmes récursifs et les boucles while dans un contexte de Rely-Guarantee, en utilisant un langage à large spectre basé sur un treillis distributif complet de commandes. La méthodologie est fondée sur les composantes clés suivantes :

Sémantique de trace d'Aczel : Le modèle sémantique utilise des ensembles de traces d'Aczel, qui enregistrent des séquences de transitions de programme ( $\pi$ ) et d'environnement ( $\epsilon$ ). Cela permet un traitement compositionnel de l'interférence sans supposer l'atomicité de l'évaluation des expressions ou des commandes d'assignation.
Conditions de Rely-Guarantee : Le cadre emploie des conditions de dépendance (rely conditions, $r$ ) pour contraindre le comportement de l'environnement et des conditions de garantie (guarantee conditions, $g$ ) pour contraindre le comportement du programme. La garantie d'un thread doit impliquer la condition de dépendance de tous les threads parallèles.
Théorie des points fixes : Les programmes récursifs sont définis comme des points fixes sur un treillis de commandes. Les auteurs développent des lois pour raisonner sur ces points fixes, en utilisant spécifiquement l'induction bien fondée avec des expressions de variante et des relations pour prouver la terminaison.
Terminaison précoce (Early Termination) : Une innovation méthodologique centrale est le développement de versions de "terminaison précoce" des lois pour la récursion et les boucles. Contrairement aux approches standards qui exigent que la variante soit strictement réduite par le corps de la fonction avant tout appel récursif, ces lois permettent au corps de la fonction de soit réduire la variante, soit d'établir une condition (un cas de base) qui garantit qu'aucun appel récursif ultérieur ne sera effectué. Ceci est crucial pour la concurrence, où l'interférence peut réduire la variante d'une manière qui empêche le corps de la fonction de la réduire, tout en assurant la terminaison.
Évaluation non-atomique des expressions : L'approche gère explicitement l'évaluation non-atomique des expressions. Elle utilise une méthode compositionnelle pour établir les postconditions d'expressions complexes en analysant leurs sous-expressions, évitant ainsi le besoin de restrictions syntaxiques comme la "référence critique unique" présente dans les théories supposant l'atomicité.

Contributions clés

Le papier présente plusieurs contributions spécifiques à la théorie de la vérification de programmes concurrents :

Règles de raffinement générales pour la récursion : Le Théorème 5 ("recursion-early") fournit une règle pour introduire la récursion qui accepte l'interférence. Il utilise une relation bien fondée et une expression de variante, permettant de prouver la terminaison même si la variante est réduite par l'environnement plutôt que par le corps de la fonction, à condition qu'un cas de base soit établi.
Règles de raffinement générales pour les boucles while : Le Théorème 6 ("intro-while") dérive une loi pour introduire les boucles while basée sur la loi de récursion. Elle inclut une condition de "terminaison précoce" ( $p_X$ ) qui permet à la boucle de sortir si la garde est évaluée à faux en raison de l'interférence, même si le corps de la boucle n'a pas strictement diminué la variante.
Gestion des expressions non-atomiques : Le cadre fournit des règles d'inférence (par exemple, le Théorème 2 pour les conditionnels, le Théorème 3 pour les appels de fonctions) qui permettent un raisonnement compositionnel sur les expressions et les gardes sous interférence sans supposer une évaluation atomique.
Vérification formelle : Tous les lemmes et théorèmes présentés dans le papier ont été vérifiés mécaniquement à l'aide du prouveur de théorèmes Isabelle/HOL.
Terminaison équitable (Fair Termination) : Le papier traite de la terminaison équitable, définissant une commande fair qui interdit les séquences infinies de transitions contiguës de l'environnement, et montre comment prouver qu'une commande effectue un nombre fini de transitions sous une exécution équitable.

Résultats et exemples

Le papier démontre l'utilité des lois développées à travers deux exemples principaux :

Recherche récursive parallèle : Un algorithme de recherche récursive est développé pour trouver une valeur $i$ dans une plage $[0, N)$ satisfaisant un prédicat $P$ . L'implémentation utilise une stratégie de type "diviser pour régner" avec des appels récursifs parallèles. La preuve utilise la loi "recursion-early" pour gérer le cas où un thread concurrent aurait déjà trouvé une solution (en réglant le drapeau found), permettant aux appels récursifs de terminer prématurément sans traitement supplémentaire.
Mise à jour atomique avec CAS : Un exemple d'implémentation d'une spécification atomique pour mettre à jour une variable $m$ vers $\min(m, lo)$ en utilisant une instruction Compare-And-Swap (CAS). La boucle tente répétitivement le CAS. La version de la loi de boucle pour "terminaison précoce" est essentielle ici : si l'interférence diminue $m$ en dessous de $lo$ entre la vérification de la garde et l'exécution du CAS, le CAS peut échouer à diminuer $m$ (la variante). Cependant, la boucle se termine car la garde ($lo < m$) devient fausse. La loi de boucle standard échouerait à prouver la terminaison dans ce scénario, mais la loi proposée réussit en reconnaissant la condition de sortie précoce.

Signification et revendications

Les auteurs affirment que leur travail fournit des règles de raffinement générales, vérifiées mécaniquement pour raisonner sur la récursion et les boucles en présence de concurrence. La portée de ce travail réside dans :

Suppression des hypothèses d'atomicité : En ne supposant pas que l'évaluation des expressions est atomique, les règles sont applicables à un éventail plus large de scénarios de programmation réalistes et évitent de briser la chaîne de raisonnement formel des théories reposant sur l'atomicité.
Gestion de l'interférence dans les preuves de terminaison : Les lois de "terminaison précoce" comblent une lacune spécifique dans la vérification concurrente où l'interférence peut invalider les arguments de terminaison standards. Cela permet la vérification de programmes où les actions de l'environnement contribuent à la condition de terminaison.
Développement compositionnel : L'approche soutient le développement compositionnel de programmes à variables partagées, permettant aux threads d'être conçus et vérifiés indépendamment sur la base de leurs conditions de dépendance (rely) et de garantie (guarantee).
Rigueur formelle : Les résultats ne sont pas de simples propositions théoriques mais ont été formalisés et vérifiés dans le prouveur de théorèmes Isabelle/HOL, garantissant leur validité logique.

Le papier se positionne comme une extension des recherches algébriques précédentes sur le Rely-Guarantee, ciblant spécifiquement les complexités introduites par la récursion, les boucles et l'évaluation non-atomique des expressions dans les systèmes concurrents. Il ne prétend pas remplacer d'autres logiques comme la Logique de Séparation Concurrente (CSL), mais offre une méthode de raisonnement compositionnel alternative, notant particulièrement que si la CSL supporte le raisonnement sur l'absence de races, le RG est conçu pour le développement de programmes "racy" (programmes où les races sont gérées via des conditions de dépendance/garantie).