Recursive Mutexes in Separation Logic

Résumé Technique : Mutex Récursifs en Logique de Séparation

Énoncé du Problème
Bien que la logique de séparation concurrente mécanisée ait progressé au point de vérifier des programmes réels dans des langages tels que le C++ et le Rust à l'aide d'outils comme VST, BRiCk et RustBelt, une lacune subsiste dans la vérification formelle des bibliothèques de concurrence standards. Plus précisément, les mutex récursifs (communs en C++ et Java) manquent de spécifications de logique de séparation établies. Contrairement aux mutex standards, qu'un thread ne peut acquérir s'il les détient déjà, les mutex récursifs permettent à un seul thread d'acquérir le même verrou plusieurs fois. Cette capacité permet des modèles de code idiomatiques où une fonction détenant un verrou peut appeler en toute sécurité une autre fonction qui tente également d'acquérir le même verrou (par exemple, transfer appelant update_a dans la Figure 1). Les spécifications des mutex standards échouent à supporter cette transparence et cette encapsulation, forçant souvent les développeurs à créer des fonctions alternatives sans verrou ou à effectuer des analyses de cas complexes sur la propriété du verrou.

Méthodologie
Les auteurs proposent une nouvelle spécification de logique de séparation pour les mutex récursifs qui traite l'acquisition et la libération de verrou de manière uniforme, quel que soit l'état de propriété actuel du thread appelant. La méthodologie introduit deux composantes primaires :

1. Handles Fractionnaires et Prédicats Spécifiques au Thread :

   • Un mutex récursif $\gamma$ avec un invariant $P$ est associé à un handle fractionnaire $\ell \mapsto_q \text{rmutex}(\gamma, P)$.
   • Crucialement, chaque thread $t$ qui interagit avec le mutex possède son propre prédicat : $\text{holds}(\gamma, t, n, P)$. Ici, $n$ représente le nombre de fois que le thread $t$ a acquis le mutex.
   • L'exclusion mutuelle est imposée par la règle selon laquelle si deux threads détiennent le mutex, au moins l'un d'eux doit avoir un compte de zéro ($n_1 = 0 \lor n_2 = 0$).
   • Pour empêcher un thread de "double-compter" les ressources, la logique impose qu'un thread ne puisse pas détenir deux prédicats $\text{holds}$ simultanément ; ainsi, $\text{holds}(\gamma, t, n_1, P) * \text{holds}(\gamma, t, n_2, P) \vdash \text{False}$.

2. Transitions d'État et Emprunt (Borrowing) :

   • Verrouillage/Déverrouillage : L'acquisition du verrou incrémente le compte $n$ du thread ($n \to n+1$), et la libération le décrémente ($n \to n-1$).
   • Règle d'Emprunt : Un thread peut accéder à l'invariant protégé $P$ si et seulement si son compte $n > 0$. La règle permet à un thread d'échanger $\text{holds}(\gamma, t, n, P)$ (où $n>0$) contre les ressources réelles $P$ plus un détenteur $\text{held}(\gamma, t, n)$ qui suit le compte mais n'accorde pas l'accès à $P$.
   • Gestion des Arguments Quantifiés : Pour traiter les problèmes où les invariants de verrou contiennent des variables existentiellement quantifiées (par exemple, $\exists v. x \mapsto v$), les auteurs introduisent un tuple d'arguments $a$ passé au prédicat $\text{holds}$. Cela garantit que lorsqu'un thread emprunte $P$, il conserve des connaissances spécifiques sur les ressources (par exemple, des valeurs spécifiques de variables) plutôt que de re-quantifier et perdre cette information lors du retour à l'état d'invariant.

Contributions Clés

• Spécification Unifiée : Le papier fournit une spécification qui permet aux clients de déterminer s'ils détiennent le mutex uniquement en vérifiant si leur compte $n$ est supérieur à zéro, sans avoir besoin de distinguer entre une acquisition "première fois" et une acquisition "récursive".
• Raisonnement Idiomatique : Les spécifications permettent de prouver des modèles de code où des fonctions appellent d'autres fonctions qui acquièrent également le même verrou, reflétant l'usage standard du C++ sans nécessiter de variantes spéciales "sans verrou" des fonctions.
• Vérification Formelle de la Concurrence C++ : Le travail démontre l'application de ces spécifications pour vérifier la bibliothèque de concurrence C++ (spécifiquement std::recursive_mutex) en utilisant le framework BRiCk.

Résultats
Les auteurs ont appliqué avec succès ces spécifications pour vérifier l'exemple de la Figure 1, où une fonction transfer appelle update_a et update_b tout en détenant le même mutex récursif. La vérification confirme que :

• La fonction transfer peut réutiliser en toute sécurité update_a même si les deux acquièrent le même mutex.
• L'invariant (la somme de balance_a et balance_b) est préservé à travers l'opération.
• La logique gère correctement l'état de l'invariant, que le thread détenait initialement le verrou ou non, en préservant les valeurs spécifiques des variables (comme $a$ et $b$) à travers la pile d'appels.

Signification
Le papier affirme que ces spécifications rendent le raisonnement sur les mutex récursifs "plus transparent et mieux encapsulé" qu'en utilisant des mutex normaux. En séparant les opérations d'acquisition du verrou (incrémentation de $n$) et d'emprunt de l'invariant (accès à $P$ quand $n>0$), l'approche soutient les modèles d'ingénierie logicielle courants trouvés dans les langages mainstream. Ce travail est présenté comme une étape vers l'objectif plus large de vérifier l'intégralité de la bibliothèque standard C++, visant à mettre en lumière des principes de raisonnement pratiques pour la programmation concurrente réelle. Les auteurs notent que leurs spécifications actuelles couvrent également d'autres composants de la bibliothèque standard comme std::atomic et std::vector.