Specifiche di Sistemi Concorrenti

Concorrenza e Comunicazione

Data la sempre crescente complessità dei sistemi dinamici e distribuiti è diventata di primaria importanza la conoscenza di tecniche e strumenti atti ad analizzare, modellare e verificare se tali sistemi possiedono tutte le caratteristiche che da essi ci aspettiamo. In altre parole assegnare un significato a un sistema è esattamente ciò che è osservabile di esso e osservare un sistema è esattamente comunicare con esso.

Detti sistemi sono formati da molte componenti, ognuna delle quali partecipa insieme e indipendentemente con le altre componenti, ma mantenendo nello stesso tempo la propria identità. Tali componenti sono chiamate agenti e compiono attività computazionali indipendenti tra loro e che possono sovrapporsi nel tempo; quindi si dice che le loro esecuzioni procedono in concorrenza.

La singola esecuzione di un programma viene definita processo, perciò i sistemi concorrenti sono composti da processi multipli che agiscono contemporaneamente; se oltre a ciò gli agenti interagiscono tra di loro possiamo parlare di comunicazione.

I protocolli e i servizi di network rivestono un ruolo di fondamentale importantanza nell'informatica moderna e rappresentano i più comuni esempi di sistemi concorrenti.

Come si può intuire i sistemi concorrenti sono più complessi e articolati rispetto a quelli sequenziali:

La comunicazione tra le diverse componenti avviene di solito tramite le due seguenti tecniche di base:

Possiamo inoltre affermare che esistono due modi di esecuzione per un sistema concorrente:
Esecuzione asincrona o interleaved
In ogni istante di tempo, solo una componente alla volta effettua un'attività.
Esecuzione sincrona
In ogni momento, tutte le componenti effettuano una certa attività.

Nei sistemi molto complessi si può avere il problema dell' esplosione degli stati perché risulta enorme il numero degli stati nella struttura globale. Oltre a questo problema, esistono altri comportamenti che creano difficoltà nell'analisi della concorrenza e che devono essere individuati:

Nondeterminismo
Si ha quando un sistema può comportarsi in due o più modi differenti nonostante riceva un unico input. I sistemi paralleli hanno spesso questo comportamento a causa della comunicazione tra processi.
Deadlock
In questo caso, si arriva in uno stato in cui nessuna componente del sistema può procedere (non ci sono azioni che possono essere eseguite). Solitamente questo fenomeno si verifica perché un gruppo di componenti attendono reciproci messaggi oppure perchè competono per condividere le risorse presenti nell'ambiente.
Nel modello a stati finiti di un processo, uno stato di deadlock è semplicemente uno stato senza transizioni in uscita.
Livelock
E' presente quando un network (cioè una rete di processi paralleli) comunica internamente per un tempo infinito senza che qualsiasi componente comunichi con l'esterno. Per un osservatore può apparire simile alla situazione di deadlock, ma la presenza di attività interne crea ulteriori problemi. Il comportamento di livelock più comune è quello della divergenza per la quale un programma esegue una sequenza infinita di azioni interne.

Verificare la correttezza di un sistema tramite lo studio (ed eventualmente la risoluzione) di questi problemi è molto importante perché evita malfunzionamenti anche molto dannosi che si possono ritrovare a livello pratico.

Una proprietà è un attributo di un programma che risulta valido in qualunque possibile esecuzione del programma stesso. Nei programmi concorrenti le proprietà più interessanti si dividono in due categorie :

Safety
Si garantisce che niente di "cattivo" avviene durante l'esecuzione del programma quindi non si raggiunge mai uno stato non corretto;
Liveness
Si asserisce che qualcosa di "buono" prima o poi avviene, cioè nel futuro dell'esecuzione si raggiunge uno stato voluto.

Le più importanti proprietà di Safety sono:

-
correttezza dello stato finale: nel sistema gli stati finali (cioè senza transizioni in uscita) non presentano alcun tipo di ambiguità o errore.
-
assenza di deadlock: si evita che il sistema raggiunga una situazione nella quale non può più procedere.
-
mutua esclusione: si impedisce che la stessa risorsa sia utilizzata da due processi nello stesso istante. In questo modo si evita il fenomeno negativo dell'interferenza, cioè l'aggiornamento scorretto dello stato in cui si trova la risorsa condivisa; tali errori sono molto difficili da individuare nei sistemi reali anche dopo test molto estesi.

Le più importanti proprietà di Liveness sono:

-
terminazione: stabilisce che un programma prima o poi termina in uno stato finale. Questo è vero in generale per i programma sequenziali, ma nel caso della concorrenza si trovano frequentemente sistemi che non terminano.
-
Progresso: si asserisce che, in qualunque stato si trovi il sistema, un'azione specificata sarà sempre eseguita. Da questa definizione si intuisce che il progresso è l'opposto di starvation, cioè la situazione in cui un'azione non è mai eseguita.

Oltre a safety e liveness, si possono anche osservare sistemi con un comportamento divergente. In questi casi il sistema può raggiungere uno stato in cui esegue un numero infinito di azioni che però non sono visibili dall'esterno. Si intuisce facilmente che se c'è questa caratteristica, allora non è detto che si raggiunga lo stato finale.

Altri comportamenti interessanti sono dati dalle proprietà cicliche che indicano la ripetizione periodica e infinita della stessa sequenza di azioni.

Quando si parla di sistema reattivo ci riferiamo ad un sistema che non lavora isolatamente, ma interagisce con altri nello svolgimento dei propri compiti e reagisce alle loro richieste. Perciò, di solito questi sistemi mostrano un'esecuzione concorrente dove le componenti possono competere per risorse condivise oppure coordinano le loro attività per ottenere un obiettivo comune.

Possiamo affermare che un processo è il comportamento di un sistema. La Teoria dei Processi studia proprio questi comportamenti ed è suddivisa in due attività principali:

  1. Il Modelling è l'attività di rappresentare processi attraverso strutture matematiche o per mezzo delle espressioni di un linguaggio di descrizione per i sistemi. Con esso si crea il modello del sistema reale che ci interessa, cioè una sua rappresentazione semplificata. In genere, questa fase è immediatamente seguita dall'implementazione dei processi che compongono il sistema.
  2. La Verifica consiste nel dimostrare le proprietà che questi processi forniscono al sistema. Per esempio si può verificare se due processi sono uguali e quindi se due sistemi si comportano nello stesso modo.
Lo stato di un processo è determinato dal valore delle variabili esplicite ed implicite che esso assume in un certo momento. Perciò l'esecuzione di un processo trasforma lo stato attraverso una serie di istruzioni le quali sono composte da una o più azioni atomiche che sono indivisibili.

Ogni azione di un processo può essere un'interazione con i processi vicini ed allora si parla di comunicazione, oppure le parti agiscono indipendentemente e quindi si ha la concorrenza.

Esistono molti tipi differenti di sistemi concorrenti: circuiti sincroni e asincroni, programmi con variabili condivise o che comunicano con lo scambio di messaggi, protocolli handshake. In quest'ultimo caso, definiamo l'handshake come un'azione indivisibile nella quale un valore è simultaneamente emesso da una componente e ricevuto da un'altra.

Semantiche delle Algebre di processi

Per studiare un sistema concorrente in modo matematico, sono state introdotte delle strutture algebriche con cui si può descrivere in maniera relativamente facile il modello che ci interessa. Questi formalismi sono detti algebre di processi e simulano la maggior parte dei comportamenti del sistema considerato.

Nelle applicazioni di queste algebre, la specifica e l'implementazione sono espresse come due processi distinti, ma la correttezza dei programmi si basa su una certa equivalenza di comportamento tra essi.

Ci sono tre differenti semantiche che permettono di interpretare un'algebra di processi:

Per la semantica operazionale, in questo testo verranno descritti i diagrammi di transizione LTS in cui assumono notevole importanza le azioni che permettono al sistema di passare da uno stato all'altro. Invece, dal punto di vista algebrico, si mostrano le leggi per gli operatori più usati nella pratica ed in particolare viene descritto il calcolo CCS di Milner.

La semantica denotazionale è quella meno utilizzata nella teoria della concorrenza e qui verrà ignorata.

Equivalenze comportamentali e Logiche

Per confrontare due o più sistemi concorrenti, gli studiosi hanno introdotto molte equivalenze comportamentali. Ognuna di esse confronta due sistemi in base ad una certa categoria di comportamenti e per questo motivo si trovano diverse relazioni che legano le equivalenze tra loro. In particolare, assume notevole importanza il concetto di bisimulazione.

La nozione chiamata equivalenza di osservazione si riferisce a processi che esternamente seguono gli stessi cammini, ma possono differire nel comportamento interno.

Con la Logica possiamo definire un gran numero di proprietà che possono essere verificate o meno dai sistemi studiati. Due concetti generali che permettono di trattare una formula sono i seguenti:

Soddisfacibilità
Una formula è soddisfacibile (o realizzabile) se esiste almeno un modello (ad esempio un LTS) in cui vale la proprietà che essa descrive.
Validità
Una formula è valida se essa è soddisfacibile in tutti i modelli esistenti.
Se si vuole verificare la soddisfacibilità di una formula in un modello predeterminato, utilizziamo una tecnica chiamata Model Checking.

Morpheus 2004-02-10