Recursive Mutexes in Separation Logic

Sintesi Tecnica: Mutex Ricorsivi nella Logica di Separazione

Definizione del Problema
Sebbene la logica di separazione concorrente meccanizzata abbia fatto progressi tali da permettere la verifica di programmi reali in linguaggi come C++ e Rust utilizzando strumenti come VST, BRiCk e RustBelt, rimane una lacuna nella verifica formale delle librerie di concorrenza standard. Nello specifico, i mutex ricorsivi (comuni in C++ e Java) mancano di specifiche di logica di separazione consolidate. A differenza dei mutex standard, che un thread non può acquisire se li possiede già, i mutex ricorsivi permettono a un singolo thread di acquisire lo stesso lock più volte. Questa capacità abilita pattern di codice idiomatici in cui una funzione che detiene un lock può chiamare in sicurezza un'altra funzione che tenta di acquisire lo stesso lock (ad esempio, transfer che chiama update_a in Figura 1). Le specifiche dei mutex standard non riescono a supportare questa trasparenza e incapsulamento, costringendo spesso gli sviluppatori a creare funzioni alternative senza lock o a eseguire analisi di casi complessi sull'ownership del lock.

Metodologia
Gli autori propongono una nuova specifica di logica di separazione per i mutex ricorsivi che tratta l'acquisizione e il rilascio del lock in modo uniforme, indipendentemente dallo stato di ownership corrente del thread chiamante. La metodologia introduce due componenti primarie:

1. Handle Frattionari e Predicati Specifici per il Thread:

   • Un mutex ricorsivo $\gamma$ con invariante $P$ è associato a un handle frazionario $\ell \mapsto_q \text{rmutex}(\gamma, P)$.
   • Fondamentalmente, ogni thread $t$ che interagisce con il mutex possiede il proprio predicato: $\text{holds}(\gamma, t, n, P)$. Qui, $n$ rappresenta il numero di volte che il thread $t$ ha acquisito il mutex.
   • L'esclusione mutua è garantita dalla regola secondo cui se due thread detengono il mutex, almeno uno deve avere un conteggio pari a zero ($n_1 = 0 \lor n_2 = 0$).
   • Per evitare che un singolo thread possa "doppio-contare" le risorse, la logica impone che un thread non possa detenere due predicati $\text{holds}$ simultaneamente; pertanto, $\text{holds}(\gamma, t, n_1, P) * \text{holds}(\gamma, t, n_2, P) \vdash \text{False}$.

2. Transizioni di Stato e Borrowing (Prestito):

   • Lock/Unlock: L'acquisizione del lock incrementa il conteggio $n$ del thread ($n \to n+1$), e il rilascio decrementa $n$ ($n \to n-1$).
   • Regola di Borrowing: Un thread può accedere all'invariante protetto $P$ se e solo se il suo conteggio $n > 0$. La regola permette a un thread di scambiare $\text{holds}(\gamma, t, n, P)$ (dove $n>0$) con le risorse effettive $P$ più un retainer $\text{held}(\gamma, t, n)$ che traccia il conteggio ma non concede l'accesso a $P$.
   • Gestione degli Argomenti Quantificati: Per affrontare le problematiche in cui gli invarianti del lock contengono variabili quantificate esistenzialmente (ad esempio, $\exists v. x \mapsto v$), gli autori introducono una tupla di argomenti $a$ passati al predicato $\text{holds}$. Ciò assicura che, quando un thread effettua il borrow di $P$, mantenga una conoscenza specifica sulle risorse (ad esempio, valori specifici di variabili) invece di ricuantificare e perdere tale informazione al ritorno allo stato dell'invariante.

Contributi Chiave

• Specifica Unificata: Il documento fornisce una specifica che consente ai client di determinare se detengono il mutex verificando esclusivamente se il loro conteggio $n$ è maggiore di zero, senza dover distinguere tra acquisizione "iniziale" e acquisizione "ricorsiva".
• Ragionamento Idiomatico: Le specifiche consentono prove per pattern di codice in cui le funzioni chiamano altre funzioni che acquisiscono lo stesso lock, rispecchiando l'uso standard di C++ senza richiedere varianti "senza-lock" speciali delle funzioni.
• Verifica Formale della Concorrenza in C++: Il lavoro dimostra l'applicazione di queste specifiche per verificare la libreria di concorrenza C++ (specificamente std::recursive_mutex) utilizzando il framework BRiCk.

Risultati
Gli autori hanno applicato con successo queste specifiche per verificare l'esempio in Figura 1, dove una funzione transfer chiama update_a e update_b mentre detiene lo stesso mutex ricorsivo. La verifica conferma che:

• La funzione transfer può utilizzare in sicurezza update_a anche se entrambi acquisiscono lo stesso mutex.
• L'invariante (la somma di balance_a e balance_b) è preservata attraverso l'operazione.
• La logica gestisce correttamente lo stato dell'invariante sia che il thread detenessse inizialmente il lock, sia che non lo detenesse, preservando i valori specifici delle variabili (come $a$ e $b$) attraverso lo stack delle chiamate.

Significatività
Il documento sostiene che queste specifiche rendono il ragionamento sui mutex ricorsivi "più trasparente e meglio incapsulato" rispetto all'uso di normali mutex. Separando le operazioni di acquisizione del lock (incremento di $n$) e di borrowing dell'invariante (accesso a $P$ quando $n>0$), l'approccio supporta i comuni pattern di ingegneria del software presenti nei linguaggi mainstream. Questo lavoro è presentato come un passo verso l'obiettivo più ampio di verificare l'intera libreria standard del C++, mirando a evidenziare principi di ragionamento che siano pratici per la programmazione concorrente nel mondo reale. Gli autori osservano che le loro attuali specifiche coprono anche altri componenti della libreria standard come std::atomic e std::vector.