Reasoning about concurrent loops and recursion with rely-guarantee rules

Questo articolo presenta regole di raffinamento generali, verificate meccanicamente, per il ragionamento su programmi ricorsivi e cicli while in sistemi concorrenti utilizzando l'approccio rely-guarantee, senza assumere l'atomicità della valutazione delle espressioni.

L'essenziale

Immagina di dover scrivere una ricetta per un team di chef che lavorano in una cucina condivisa e caotica. Tutti stanno tagliando, mescolando e assaggiando contemporaneamente. Il problema è che, mentre lo Chef A legge un passaggio della ricetta, lo Chef B potrebbe intrufolarsi e spostare un ingrediente, cambiare la temperatura o nascondere uno strumento. Questo è il mondo della programmazione concorrente: più programmi che girano contemporaneamente, che si intralciano a vicenda nei loro dati.

Questo articolo di Hayes, Meinicke e Jones è come un nuovo libro di regole ultra-rigoroso per scrivere queste ricette, in modo che siano garantite per funzionare, anche nel caos. Si concentrano su due tipi specifici di istruzioni di cucina: i cicli (fare qualcosa ripetutamente) e la ricorsione (una ricetta che chiama se stessa per risolvere una parte più piccola del problema).

Ecco la suddivisione delle loro "regole della cucina" usando analogie semplici:

1. Il patto "Rely-Guarantee" (Affidamento-Garanzia)

In una cucina normale, potresti semplicemente fidarti del fatto che nessuno toccherà la tua pentola. In questo articolo, gli autori dicono: "La fiducia non basta. Abbiamo bisogno di un contratto."

• La Condizione di Rely (La lista del "Non toccare"): Prima di iniziare il tuo compito, assumi che gli altri chef rispettino certe regole. Per esempio: "Mi affido al fatto che nessuno aggiunga sale alla mia zuppa mentre la sto assaggiando."
• La Condizione di Guarantee (La lista del "Prometto"): In cambio, prometti che anche tu seguirai delle regole. "Garantisco che non lancerò mai il mio cucchiaio contro il muro."
• La Magia: Se tutti rispettano i propri contratti di "Rely" e "Guarantee", l'intera cucina funziona senza problemi, anche se tutti lavorano contemporaneamente.

2. Il problema delle assunzioni "Atomiche"

Molti vecchi libri di regole assumevano che quando uno chef legge un passaggio della ricetta, lo faccia istantaneamente, come un magico scatto di dita. Assumevano che lo chef leggesse "Aggiungi 2 uova" e le aggiungesse prima che chiunque altro potesse nemmeno battere ciglio.

Gli autori dicono: "No, non è così che funzionano le cucine reali."
Nella realtà, leggere "Aggiungi 2 uova" richiede tempo. Mentre lo chef sta prendendo le uova, un altro chef potrebbe spostare il cartone. Questo articolo costruisce regole che tengono conto di questa realtà disordinata. Non assumono che tutto accada istantaneamente; assumono che tutto richieda un po' di tempo e possa essere interrotto.

3. Domare il ciclo "While" (Il mescolare senza fine)

Un ciclo "while" è come uno chef che mescola una pentola "finché la salsa non si addensa".

• Il Vecchio Problema: In una cucina condivisa, uno chef potrebbe mescolare, controllare la salsa e decidere che non è ancora densa. Ma mentre sta camminando verso il fornello, un altro chef potrebbe aggiungere acqua, rendendola di nuovo liquida. Il primo chef potrebbe continuare a mescolare per sempre, o fermarsi quando non dovrebbe.
• La Nuova Regola (Terminazione Anticipata): Gli autori introducono un trucco astuto chiamato "Early Termination" (Terminazione Anticipata).
  • Immagina che lo chef abbia un timer (una "variante"). Ogni volta che mescola, il timer scende.
  • Di solito, lo chef deve mescolare per far scendere il timer.
  • Il Colpo di Scena: Se un altro chef accidentalmente aggiunge acqua (interferenza), il timer potrebbe scendere più velocemente del previsto, o la salsa potrebbe improvvisamente diventare abbastanza densa da far sì che il ciclo dovrebbe fermarsi.
  • La nuova regola permette al ciclo di fermarsi in anticipo se l'ambiente (gli altri chef) aiuta a finire il lavoro, invece di costringere il ciclo a fare tutto il lavoro da solo. È come dire: "Se la salsa è già densa perché qualcun altro ha aiutato, puoi smettere subito di mescolare."

4. Domare la Ricorsione (La ricetta che chiama se stessa)

La ricorsione è come uno chef che dice: "Per fare questo grande stufato, devo prima fare una piccola partita di brodo. Per fare questo brodo, devo prima fare un pochino di fondo..."

• La Sfida: In una cucina condivisa, se lo Chef A sta facendo il brodo, lo Chef B potrebbe rubare la pentola del fondo.
• La Soluzione: Gli autori hanno creato una "scala" matematica (una relazione ben fondata). Immagina che lo chef stia scendendo una scala per risolvere problemi sempre più piccoli.
  • La Regola: Puoi scendere la scala solo se sei sicuro di non rimanere bloccato.
  • Il Trucco dell' "Uscita Anticipata": Proprio come per i cicli, se gli altri chef ti aiutano a raggiungere il fondo della scala più velocemente (risolvendo un sottoproblema per te), ti è permesso fermare la discesa in anticipo. Non devi compiere ogni singolo passo tu stesso se l'ambiente ti aiuta a finire.

5. L' "Aczel Trace" (La telecamera di sicurezza della cucina)

Per dimostrare che le loro regole funzionano, gli autori utilizzano un concetto chiamato Aczel trace.

• Immagina una telecamera di sicurezza che registra la cucina.
• La telecamera registra due tipi di movimenti: Movimenti del programma (ciò che fa lo chef che stai osservando) e Movimenti dell'ambiente (ciò che fanno gli altri chef).
• Le regole degli autori assicurano che, indipendentemente da come la telecamera registra il caos, se i contratti di "Rely" e "Guarantee" sono rispettati, il piatto finale sarà perfetto.

Riassunto

Questo articolo fornisce un nuovo modo robusto per scrivere istruzioni per programmi informatici che girano contemporaneamente.

1. Niente Magia: Smette di assumere che le cose accadano istantaneamente.
2. Contratti: Utilizza "Rely" e "Guarantee" per gestire l'interazione tra i programmi.
3. Flessibilità: Permette ai cicli e alle funzioni ricorsive di terminare in anticipo se l'ambiente aiuta a completarle, evitando che rimangano bloccati in cicli infiniti o falliscano a causa delle interferenze.

Gli autori hanno già testato queste regole utilizzando un assistente alla prova informatica, Isabelle/HOL, che agisce come un insegnante di matematica super severo, controllando ogni singolo passaggio per garantire che la logica sia impeccabile. Non hanno solo ipotizzato; hanno dimostrato che funziona.

Sommario tecnico

Sintesi Tecnica: Ragionamento su Cicli Ricorsivi e Ricorsione con Regole Rely-Guarantee

Definizione del Problema

La verifica di programmi concorrenti, in particolare quelli che coinvolgono strutture ricorsive e cicli while, affronta sfide significative quando si deve gestire l'interferenza da parte di thread paralleli. Le tradizionali regole di verifica di tipo Hoare per i cicli si basano su invarianti e espressioni di variante per dimostrare la correttezza e la terminazione. Tuttavia, in un contesto concorrente, l'interferenza può invalidare gli invarianti del ciclo, aumentare le espressioni di variante o interrompere l'esecuzione dei guard (guardie), rendendo invalide le normali regole sequenziali.

Inoltre, molti approcci Rely-Guarantee (RG) esistenti assumono che l'valutazione delle espressioni sia atomica. Questa assunzione non riflette la realtà delle implementazioni dei linguaggi di programmazione, dove le espressioni possono comportare molteplici accessi a variabili condivise che possono essere intercalati con transizioni dell'ambiente. Questa assunzione di atomicità rompe la catena formale di ragionamento per espressioni complesse e limita l'applicabilità delle regole di verifica.

Metodologia

Gli autori sviluppano un framework per il ragionamento su programmi ricorsivi e cicli while all'interno di un contesto Rely-Guarantee, utilizzando un linguaggio a spettro ampio basato su un reticolo distributivo completo di comandi. La metodologia si fonda sui seguenti componenti chiave:

1. Semantica delle Tracce di Aczel: Il modello semantico utilizza insiemi di tracce di Aczel, che registrano sequenze di transizioni del programma ($\pi$) e dell'ambiente ($\epsilon$). Ciò consente un trattamento composizionale dell'interferenza senza assumere l'atomicità della valutazione delle espressioni o dei comandi di assegnazione.
2. Condizioni Rely-Guarantee: Il framework impiega condizioni di rely ($r$) per vincolare il comportamento dell'ambiente e condizioni di guarantee ($g$) per vincolare il comportamento del programma. La garanzia di un thread deve implicare la condizione di rely di tutti i thread paralleli.
3. Teoria dei Punti Fissi: I programmi ricorsivi sono definiti come punti fissi su un reticolo di comandi. Gli autori sviluppano leggi per il ragionamento su questi punti fissi, utilizzando specificamente l'induzione ben fondata con espressioni di variante e relazioni per dimostrare la terminazione.
4. Terminazione Anticipata (Early Termination): Un'innovazione metodologica centrale è lo sviluppo di versioni per la "terminazione anticipata" delle leggi sia per la ricorsione che per i cicli. A differenza degli approcci standard che richiedono che la variante sia strettamente ridotta dal corpo della funzione prima di qualsiasi chiamata ricorsiva, queste leggi permettono al corpo della funzione di ridurre la variante o di stabilire una condizione (un caso base) che assicuri che non vengano effettuate ulteriori chiamate ricorsive. Questo è cruciale per la concorrenza, dove l'interferenza potrebbe ridurre la variante in modo tale da impedire al corpo della funzione di ridurla, pur garantendo comunque la terminazione.
5. Valutazione Non-Atomica delle Espressioni: L'approccio gestisce esplicitamente la valutazione non-atomica delle espressioni. Utilizza un metodo composizionale per stabilire le postcondizioni per espressioni complesse analizzando le loro sotto-espressioni, evitando la necessità di restrizioni sintattiche come il "singolo riferimento critico" tipico delle teorie che assumono l'atomicità.

Contributi Chiave

Il documento presenta diversi contributi specifici alla teoria della verifica di programmi concorrenti:

• Regole di Raffinamento Generali per la Ricorsione: Il Teorema 5 ("recursion-early") fornisce una regola per introdurre la ricorsione che accoglie l'interferenza. Utilizza una relazione ben fondata e un'espressione di variante, consentendo di dimostrare la terminazione anche se la variante è ridotta dall'ambiente piuttosto che dal corpo della funzione, a patto che venga stabilito un caso base.
• Regole di Raffinamento Generali per i Cicli While: Il Teorema 6 ("intro-while") deriva una legge per introdurre i cicli while basata sulla legge della ricorsione. Include una condizione di "terminazione anticipata" ($p_X$) che permette al ciclo di uscire se la guardia viene valutata come falsa a causa dell'interferenza, anche se il corpo del ciclo non ha strettamente diminuito la variante.
• Gestione delle Espressioni Non-Atomiche: Il framework fornisce regole di inferenza (ad esempio, il Teorema 2 per i condizionali, il Teorema 3 per le chiamate a funzione) che consentono il ragionamento composizionale su espressioni e guardie sotto interferenza senza assumere la valutazione atomica.
• Verifica Formale: Tutti i lemmi e i teoremi presentati nel documento sono stati verificati meccanicamente utilizzando il dimostratore di teoremi Isabelle/HOL.
• Terminazione Equa (Fair Termination): Il documento affronta la terminazione equa, definendo un comando fair che proibisce sequenze infinite contigue di transizioni dell'ambiente, e dimostrando come provare che un comando esegue solo un numero finito di transizioni sotto esecuzione equa.

Risultati ed Esempi

Il documento dimostra l'utilità delle leggi sviluppate attraverso due esempi primari:

1. Ricerca Ricorsiva Parallela: Viene sviluppato un algoritmo di ricerca ricorsiva per trovare un valore $i$ in un intervallo $[0, N)$ che soddisfi un predicato $P$. L'implementazione utilizza una strategia divide-and-conquer con chiamate ricorsive parallele. La prova utilizza la legge "recursion-early" per gestire il caso in cui un thread concorrente possa aver già trovato una soluzione (impostando un flag found), permettendo alle chiamate ricorsive di terminare anticipatamente senza ulteriore elaborazione.
2. Aggiornamento Atomico con CAS: Un esempio di implementazione di una specifica atomica per aggiornare una variabile $m$ a $\min(m, lo)$ utilizzando un'istruzione Compare-And-Swap (CAS). Il ciclo tenta ripetutamente la CAS. La versione "early termination" della legge del ciclo è essenziale qui: se l'interferenza diminuisce $m$ al di sotto di $lo$ tra il controllo della guardia e l'esecuzione della CAS, la CAS potrebbe non riuscire a diminuire $m$ (la variante). Tuttavia, il ciclo termina perché la guardia ($lo < m$) diventa falsa. La legge standard del ciclo fallirebbe nel provare la terminazione in questo scenario, ma la legge proposta ha successo riconoscendo la condizione di uscita anticipata.

Significato e Rivendicazioni

Gli autori affermano che il loro lavoro fornisce regole di raffinamento generalizzate e meccanicamente verificate per il ragionamento sulla ricorsione e sui cicli in presenza di concorrenza. Il significato di questo lavoro risiede nel:

• Rimozione delle Assunzioni di Atomicità: Non assumendo che la valutazione delle espressioni sia atomica, le regole sono applicabili a una gamma più ampia di scenari di programmazione realistici ed evitano di rompere la catena formale di ragionamento presente nelle teorie che si basano sull'atomicità.
• Gestione dell'Interferenza nelle Prove di Terminazione: Le leggi di "terminazione anticipata" affrontano una lacuna specifica nella verifica concorrente in cui l'interferenza può invalidare gli argomenti di terminazione standard. Ciò consente la verifica di programmi in cui le azioni dell'ambiente contribuiscono alla condizione di terminazione.
• Sviluppo Composizionale: L'approccio supporta lo sviluppo composizionale di programmi concorrenti a variabili condivise, permettendo ai thread di essere progettati e verificati indipendentemente in base alle loro condizioni di rely e guarantee.
• Rigore Formale: I risultati non sono semplici proposte teoriche, ma sono stati formalizzati e verificati all'interno del dimostratore di teoremi Isabelle/HOL, garantendo la loro correttezza logica.

Il documento posiziona il lavoro come un'estensione delle precedenti ricerche algebriche Rely-Guarantee, mirando specificamente alle complessità introdotte dalla ricorsione, dai cicli e dalla valutazione non-atomica delle espressioni nei sistemi concorrenti. Non pretende di sostituire altre logiche come la Concurrent Separation Logic (CSL), ma offre un metodo composizionale alternativo, notando in particolare che mentre la CSL supporta il ragionamento sulla libertà da race, la RG è progettata per lo sviluppo di programmi "racy" (programmi in cui le race sono gestite tramite condizioni di rely/guarantee).