CAPITOLO 4 " ESTENSIONI AUTO-STABILIZZANTI PER SISTEMI DI MESSAGE-PASSING "
Nozioni fondamentali
Il concetto di programma di auto-stabilizzazione distribuito, introdotto da Dijkstra, richiede che se eseguito a partire da un arbitrario stato iniziale alla fine raggiunga uno stato legittimo e da lì rimanga sempre in stati legittimi.
In altre parole, la proprietà "il programma è in uno stato legittimo" è una proprietà che da stabilità al sistema.
Lo stato di iniziale arbitrarietà rappresenta la situazione immediatamente seguente ad un errore o ad una riconfigurazione di un sistema dinamico.
Questo contrasta con la situazione che si ha con un normale programma nel quale il comportamento corretto è dato dallo stato iniziale soddisfacendo particolari proprietà.
Progettare programmi di auto-stabilizzazione è difficile, perché un processo non può sempre distinguere un arbitrario stato iniziale da uno stato legittimo, cosa che avviene durante un normale calcolo. Per esempio un flag, che è ordinariamente settato eseguendo qualche azione, potrebbe essere vero senza che l'azione avvenga realmente.
Così, il ragionamento, che è corretto per programmi ordinari, potrebbe non essere appropriato quando si considera l'auto-stabilizzazione.
Malgrado le difficoltà, sono stati realizzati molti algoritmi auto-stabilizzanti. Tuttavia, in generale un approccio più applicabile richiede la separazione dell'auto-stabilizzazione dall'originale progetto dell'algoritmo.
In questo capitolo si cercherà di mostrare che è possibile trasformare, in modo uniforme, un esistente algoritmo in una versione auto-stabilizzante.
Per mostrare ciò, noi definiamo il concetto di un programma, che è un'estensione auto-stabilizzante di un altro programma, e che caratterizza le proprietà che possono eventualmente essere contenute in ciascuna estensione.
Dijkstra ha per primo dimostrato il concetto di auto-stabilizzazione attraverso un esempio che identificava gli stati legittimi come quelli che possedevano un privilegio. Le sue soluzioni sono così esempi di auto-stabilizzazione per una forma di mutua esclusione (o equivalentemente per un token ring con un singolo token).
I risultati successivi seguono Dijkstra in quello che ha trattato e creano programmi di auto-stabilizzazione da una semplice linea di partenza.
Un esempio è il lavoro di Lamport sulla mutua esclusione auto-stabilizzante, che
differisce da quelli precedenti in quanto gli algoritmi sono creati aggiungendo istruzioni a programmi già esistenti. Esso è anche tra i pochi risultati che forniscono una precisa semantica per l’ auto-stabilizzazione, infatti Lamport definì un comportamento di malfunzionamento transitorio(momentaneo) come un'esecuzione in cui ogni processo inizialmente assegna valori arbitrari sia alle sue variabili sia al contatore di locazione e successivamente procede in accordo con il suo programma. Lamport definì un algoritmo essere auto-stabilizzante per una certa proprietà, quando la proprietà alla fine è soddisfatta malgrado il malfunzionamento iniziale.
4.3 UN SISTEMA DI MESSAGE-PASSING
I precedenti risultati sull'auto-stabilizzazione impiegano generalmente un modello di calcolo a memoria condivisa. Al contrario, il modello usato in questo capitolo è quello di un sistema di message-passing asincrono.
Un sistema di message-passing è un insieme di processi (che partono da "0" fino ad "n-1") che sono connessi da canali di comunicazione FIFO.
Le connessioni interprocessuali sono descritte da un insieme E di coppie ordinate di processi prestabiliti. I processi possono cambiare valore solo con l'invio o il ricevimento di messaggi sul canale, e si assume inoltre che alla fine ogni messaggio in un canale è ricevuto.
Tuttavia, il sistema è asincrono nel caso non ci siano limiti nè sul tempo di consegna del messaggio nè sulla capacità del canale e nè sulla relativa velocità dei processi.
Quello che non è usuale, circa un sistema di auto-stabilizzazione, è che nello stato iniziale di ciascun sistema, gli stati del processo, il contatore delle locazioni e i canali possono avere valori arbitrari, cioè non sono fatte assunzioni circa questi valori.
Da notare che, sebbene esistano le simulazioni di message-passing da una memoria condivisa, esse non sono auto-stabilizzanti.
In questi tipi di trasmissione si possono averi diversi problemi tra i quali si può presentare un fault di "messaggio apparentemente inviato".
Questo fault nasce da uno stato iniziale, in cui un canale, tra più processi vicini, è vuoto e gli stati locali del processo si trovano, per qualche fault, nello stato di attendere un messaggio di ack dagli altri processi cioè ciascun processo attende una risposta di un messaggio che è stato apparentemente inviato.
In tale situazione, un sistema che è deadlock-free (libero da deadlock), quando l'esecuzione comincia in un normale stato iniziale, potrebbe trovarsi bloccato (deadlock) perché ogni processo, pensando di aver spedito un messaggio e trovandosi pertanto nello stato di attesa di un ack, attende indefinitamente un messaggio che confermi la sua avvenuta ricezione, anche se il messaggio non è stato inviato da nessun processo. I diversi stati in cui si può trovare un processo sono illustrati nella figura 1.
Diversamente da una variabile condivisa, un canale non può essere letto da un
trasmettitore così che il trasmettitore non riesce a scoprire quando questa situazione (il fault) è avvenuta.
Un altro problema può essere causato da uno stato iniziale in cui i messaggi sono già presenti nei canali. Questi messaggi, e altri messaggi generati come il risultato del loro ricevimento (cioè una serie di messaggi di ack), possono impedire il raggiungimento di un globale stato legittimo. Pertanto il messaggio nocivo, cioè il messaggio già presente sul canale ad inizio trasmissione, deve essere cancellato dal sistema.
4.4 IL MODELLO SEMANTICO E LE SUE DIFFICOLTÀ
Noi adottiamo le definizioni usuali del modello di esecuzione interleaving in un sistema concorrente: uno stato locale di un processo è un assegnazione di valori a variabili locali e al contatore di locazione.
Uno stato globale di un sistema di processi è il prodotto cartesiano degli stati locali dei suoi processi costituenti più i contenuti del canale.
La semantica del programma di operazioni è un insieme di passi atomici e dei loro cambiamenti di stato; una sequenza di esecuzione di un programma è un'infinita sequenza di stati globali in cui ciascun elemento segue dal suo predecessore dall’esecuzione di un singolo passo atomico del programma .
Un programma è espresso come un insieme di istruzioni, ciascuna composta da una condizione (chiamata "guardia") e una sequenza di comandi che implicano passi atomici. Quando il controllo di una istruzione è esatto, le sequenze associate di comandi possono essere eseguite. Si assume inoltre che ogni istruzione, il cui controllo rimane esatto, è alla fine selezionata per l'esecuzione.
Il nostro scopo è quello di mostrare come un programma di auto-stabilizzazione può essere derivato da un programma esistente, forniamo pertanto la definizione di un programma auto-stabilizzante ed una sua estensione auto-stabilizzante.
Supponiamo che P sia un programma e che sem(P) (semantica di P) denoti l'insieme di tutte le possibili sequenze di esecuzione di P.
Gli stati legali di P possono essere definiti in due modi: come gli stati che soddisfano un predicato (chiamato specifica di P) o come gli stati raggiungibili da un normale stato iniziale. Per la definizione di una estensione auto-stabilizzante, noi facciamo riferimento alla seconda definizione.
I normali stati iniziali di P sono quegli stati in cui il contatore di locazione di ciascun processo è 0 e tutti i canali sono vuoti.
La semantica legale di P (per esempio la semantica intesa dal programmatore), denotata da legsem(P), è definita come essere una sequenza di esecuzione legale, ed ogni stato in cui una sequenza è definita è uno stato legale.
Da notare che, in generale, non tutti gli stati globali sono legali, questo finche` ci sono alcune combinazioni di valori che non possono nascere in qualche sequenza legale di esecuzione. La sequenza illegale di esecuzione è quella con lo stato iniziale che non è legale.
Una terza classe di sequenze di esecuzione sono gli stati iniziali che sono legali ma non sono normali stati iniziali, per esempio gli stati che di solito si hanno solo alla metà di una sequenza d’esecuzione.
Alcune sequenze sono chiaramente suffissi di sequenze legali. Da notare che un suffisso di una sequenza può essere la sequenza stessa.
DEFINIZIONE 1 : Il programma P è auto-stabilizzante se e solo se ciascuna sequenza in sem(P) ha un suffisso non vuoto che è identico al suffisso di qualche sequenza in legsem(P).
Una estensione di un programma esistente è tipicamente (ma non necessariamente) derivata dal programma originale arricchito con nuove variabili e nuove tipologie di messaggi.
Dobbiamo perciò distinguere fra variabili e tipologie di messaggio che sono comuni al programma originario (e le sue estensioni) e quelle che invece sono singole. Per arrivare a questa distinzione assumiamo che, per convenzione, ciascun messaggio sia composto da un "campo tipo" (type field).
DEFINIZIONE 2 : Il programma Q è una estensione del programma P se e solo se la progettazione del legsem(Q) sull'insieme di variabili e tipologie di messaggio di P è identica al legsem(P).
DEFINIZIONE 3 : Il programma Q è una estensione auto-stabilizzante del programma P se e solo se Q è auto-stabilizzante ed è una estensione di P.
Quando, iniziati in normali stati iniziali, P e Q hanno le stesse possibili esecuzioni. Da Notare che non è richiesta nessuna relazione fra l'illegale computazione di P e quella di Q.