Correttezza: safety, liveness, fairness e LTL

1. Perché il testing non basta

Un programma sequenziale si controlla con i test: stesso input, stesso output, e se l'output è sbagliato si corregge e si rilancia. Un programma concorrente, con lo stesso input, può dare output diversi a seconda dello scenario, e ogni esecuzione ne segue probabilmente uno diverso: il debugging consueto non funziona. La correttezza di un programma concorrente, che spesso non termina, si definisce quindi con proprietà delle computazioni: condizioni che devono valere in ogni scenario possibile.

Testing, verifica, validazione

• Il testing cerca malfunzionamenti (failure) per scoprire i difetti (fault) che li causano, cioè le manifestazioni di un errore umano. Controlla una proprietà negli scenari selezionati.
• La verifica controlla che il sistema soddisfi la specifica in tutti gli scenari: «abbiamo costruito il sistema nel modo giusto?». Richiede tecniche formali.
• La validazione controlla che soddisfi le aspettative del committente: «abbiamo costruito il sistema giusto?».

I test di safety controllano invarianti con asserzioni; quelli di liveness controllano che il sistema progredisca, e sono più difficili da impostare. Entrambi coprono solo una parte degli scenari, e il codice di test altera i tempi e può mascherare il bug (gli heisenbug). Il testing rivela la presenza di errori, non la loro assenza. Per dimostrarne l'assenza servono il model checking e le dimostrazioni induttive di invarianti (capitolo 11).

2. Safety e liveness

Le safety si esprimono di solito in negativo («non voglio mai Y») e si verificano stato per stato: per falsificarle basta uno stato raggiungibile. Per la liveness gli stati non bastano, perché P falsa ora può diventare vera dopo: bisogna esaminare scenari interi, con teoria e strumenti più complessi. Per esempio, se due processi incrementano atomicamente n partendo da 0, «n vale 2» non è una safety (all'inizio vale 0) ma una liveness: prima o poi, in ogni scenario, n diventa 2.

3. Fairness

La fairness è una proprietà di liveness per cui qualcosa di buono accade infinitamente spesso: ogni processo viene attivato infinite volte e ottiene il suo turno, e un'azione che può essere eseguita prima o poi lo è. È un requisito sullo scheduling: l'interleaving lo decide la politica di scheduling, quindi lo stesso programma può soddisfare o no una liveness a seconda della politica assunta. Un'azione atomica è incondizionata se non ha guardie (un assegnamento), condizionata se ne ha una (await B: può essere eseguita solo quando B è vera), eleggibile quando il processo è arrivato a eseguirla.

Ogni grado include il precedente, e debole e forte differiscono sulle condizioni intermittenti. Se un processo esegue await (x pari) mentre un altro incrementa x di continuo, la condizione diventa vera infinite volte ma non resta mai vera: la fairness debole non garantisce che l'attesa finisca, quella forte sì. Nessuna delle tre dice quando.

Scenari equi

Uno scenario è (incondizionatamente) equo se, in ogni suo stato, un'istruzione continuamente abilitata prima o poi compare nello scenario. L'esempio delle slide:

integer n := 0; boolean flag := false
p1: while flag = false          q1: flag := true
p2:   n := 1 - n

Termina sempre? Solo negli scenari equi. Lo scenario p1 p2 p1 p2 … non termina, ma non è equo: q1, un assegnamento sempre abilitato, non viene mai scelto. Gli scenari non equi servono però a modellare i guasti: in un sistema distribuito un processo la cui macchina cade non esegue più nulla, e se Q cade prima di q1, P non termina. Assumere la fairness vuol dire escludere questo caso.

4. La logica temporale lineare

Dalla logica proposizionale

Nel calcolo proposizionale una proprietà è una formula costruita da proposizioni atomiche con i connettivi ∧, ∨, ¬, → e ↔, vera o falsa in un singolo stato. Per i programmi concorrenti le proposizioni atomiche sono di due tipi:

• una variabile booleana: wantp è vera in uno stato se in quello stato la variabile wantp vale true;
• un'etichetta: p4 è vera se il puntatore di controllo di P è su p4.

Se p4 e q4 sono le sezioni critiche, p4 ∧ q4 descrive uno stato con entrambi in CS, e la mutua esclusione chiede che ¬(p4 ∧ q4) sia vera in ogni stato di ogni scenario. Ma una formula proposizionale parla di un solo stato: non sa dire «in ogni stato» né «prima o poi».

Le logiche temporali

Una logica temporale aggiunge operatori temporali alla logica proposizionale o dei predicati; per i programmi la introdusse Amir Pnueli (The Temporal Logic of Programs, 1977). Le famiglie sono due. La LTL (Linear Temporal Logic) vede il tempo come una sequenza lineare e discreta di stati: una formula si valuta su una computazione, e il programma la soddisfa se vale in tutti i suoi scenari, quindi basta uno scenario sbagliato per falsificarla. È la garanzia che serve per la correttezza. Le logiche ramificate, come la CTL (Computation Tree Logic), vedono da ogni stato un albero di futuri e sanno dire che una proprietà vale in alcuni o in tutti gli scenari che partono da lì.

Gli operatori

Siano s₀, s₁, … gli stati di una computazione. In uno stato s_i:

L'inglese eventually non significa «eventualmente»: significa «prima o poi, di sicuro». Always serve per le safety, eventually per le liveness. Le proprietà di base delle slide:

• riflessività: □p → p e p → ◇p;
• dualità: ¬□p → ◇¬p (se non vale sempre, prima o poi è falsa) e ¬◇p → □¬p;
• sequenze: ◇□p, da un certo punto p resta vera per sempre; □◇p, p torna vera infinite volte;
• dall'until: ◇p = true U p e □p = ¬◇¬p. Anche la precedenza, «p prima di q», si scrive con l'until: ¬q U p.

LTL è anche un sistema deduttivo, con assiomi e regole di inferenza. Dalle slide: (◇□p ∧ ◇□q) → ◇□(p ∧ q) è un teorema, perché da un certo punto entrambe restano vere; (□◇p ∧ □◇q) → □◇(p ∧ q) è falsa, perché p e q possono alternarsi senza essere mai vere insieme.

La differenza tra until e weak until, valutata nello stato iniziale su tracce infinite scritte come «qualche stato, poi un ciclo per sempre» (calcolata con ltl-traces.cjs):

5. Specificare le proprietà in LTL

Safety: □p, dove p = ¬q e q descrive lo stato da evitare. Nella versione abbreviata del problema della sezione critica, in cui le sezioni critiche sono p3 e q3, la mutua esclusione è

□ ¬(p3 ∧ q3)

Liveness: ◇p, dove p descrive la situazione desiderata. Se P aspetta di entrare in p2 e la sezione critica è p3, l'assenza di starvation si scrive in due passi:

• p2 → ◇p3 vale per lo stato corrente: se ora P è in p2, prima o poi sarà in p3. L'implicazione è vera anche quando la premessa è falsa, perché a → b equivale a ¬a ∨ b: se P non chiede di entrare, la formula non pretende nulla;
• □(p2 → ◇p3) vale per tutti gli stati. Senza il □ la formula parlerebbe solo dello stato iniziale: se lì il processo non è in p2 sarebbe vera a vuoto, e un processo bloccato per sempre in p2 a una richiesta successiva la soddisferebbe. Con il □ ogni richiesta, in ogni giro del ciclo, deve essere prima o poi soddisfatta.

6. Overtaking e k-bounded overtaking

L'assenza di starvation può essere una garanzia molto debole. Nello scenario

tryp, tryq, CSq, tryq, CSq, …, CSq, CSp      -- Q entra 1000 volte prima di P

P chiede di entrare, Q entra e riesce mille volte, e solo alla fine entra P. Non è starvation, perché ◇CSp vale, ma di solito si vuole che un processo entri entro un tempo ragionevole. Quando un processo entra al posto di un altro che aspettava si parla di overtaking (sorpasso).

La proprietà di k-bounded overtaking chiede che, da quando P tenta di entrare nella sezione critica, un altro processo possa entrarci al più k volte prima di P. Per esempio tryp, tryq, CSq, tryq, CSq, tryq, CSq, CSp rispetta il 3-overtaking. Si esprime con il weak until. Per k = 1:

tryp → (¬CSq) W (CSq W ((¬CSq) W CSp))

Da tryp la formula ammette un intervallo senza Q in CS, uno con Q in CS, un altro senza, che può chiudersi solo con P in CS: Q ha al più un intervallo continuo in sezione critica prima di P. Serve il weak until perché ogni intervallo può anche durare per sempre: con l'until la formula imporrebbe anche che P prima o poi entri, cioè conterrebbe una liveness.

Il k-bounded overtaking è una safety: vieta un sorpasso di troppo, ma non obbliga P a entrare. Va quindi affiancato alla liveness □(tryp → ◇CSp). Lo mostrano tre tracce, con la formula richiesta in ogni stato (□(tryp → …)):

Come si evita l'overtaking illimitato: con un protocollo di ingresso che limita l'attesa. Nell'algoritmo di Peterson ognuno cede il turno all'altro, quindi k = 1. Il biglietto del fornaio serve i processi in ordine di arrivo (capitolo 4). Un semaforo forte sveglia i processi in coda in ordine FIFO (capitolo 5). Un lock con test-and-set invece non dà alcun limite.

Verifica le tue conoscenze