Home

Federica EU

1/22

Aniello Murano » 17.Communicating Sequential Processes (CSP)

Introduzione al CSP

Il Communicating Sequential Proceesses (CSP) è stato inventato nel 1978 da Sir Charles Antony Richard Hoare (anche noto come Tony Hoare o C.A.R. Hoare)
Hoare è nato nel Gennaio del 1934 ed è probabilmente meglio conosciuto per aver inventato nel 1960 il Quicksort, (l’algoritmo di ordinamento più usato al mondo!!!) e il linguaggio ALGOL 60.
Ha ricevuto nel 1980 il Turing Award per “i suoi contributi fondamentali alla definizione e alla progettazione di linguaggi di programmazione”.

Il CSP

Il CSP è un linguaggio formale per descrivere l’interazioni di processi concorrenti.
Il CSP fa parte di quella teoria matematica della concorrenza nota con il nome di algebra dei processi, o process calculi.
Il CSP è stato utilizzato in pratica come uno strumento di specifica e di verifica degli aspetti concorrenti di una notevole varietà di sistemi.
Le regole di CSP hanno ispirato il linguaggio di programmazione occam (il nome deriva da William of Ockham) oggi largamente utilizzato come linguaggio di programmazione parallela.
Tra le recenti estensioni di CSP troviamo JCSP (CSP for Java ) e Timed CSP che incorpora informazioni temporali per lavorare su sistemi real-time.
Un software (free) utilizzato per controllare modelli formali espressi in CSP è FDR2, sviluppato dalla Formal Systems Europe Ltd.
La ricerca sulla teoria del CSP è tuttora attiva, così come il lavoro di incrementare il campo di applicabilità pratica.

Concorrenza/Parallelismo

In informatica, la concorrenza concerne la condivisione di risorse tra più computazioni che vengono eseguite sovrapposte nel tempo.
L’efficienza della concorrenza dipende dalle tecniche utilizzate per coordinare l’esecuzione delle computazioni, scambiare i dati, allocare memoria e schedulare i processi nel tempo in modo da minimizzare il tempo e massimizzare i risultati (si veda per esempio la tecnica greedy).
I sistemi operativi sono sistemi concorrenti, progettati in modo da operare all’infinito, senza la possibilità di terminare in modo inatteso.
Ricordiamo che un sistema concorrente è anche nondetermini-stico, come abbiamo visto per IMPGC.

Esempi di Concorrenza/Parallelismo

Thread (di execution).
- I thread rappresentano un modo in cui un processo (programma) si può dividere in più task per essere eseguiti simultaneamente.
- I mulititread possono essere eseguiti in parallelo su più computer.
- I multitread si dividono in time slicing (un solo processore) e multiprocessing (più processori).
- I tread sono simili ai processi ma differiscono per il fatto che i primi condividono risorse mentre i secondi sono indipendenti tra loro.
Processi
- Un processo è una esecuzione di una istanza di un programma.
- Il sistema operativo mantiene i processi separati tra loro ed alloca ad ognuno le risorse richieste in modo che i processi non interferiscano tra loro ed evitare così fallimenti del sistema.
- Un sistema operativo multitasking passa tra processi dando l’impressione di una esecuzione simultanea.
- Comunicazione tra processi: chiamate a procedure remote, messaggi, ect.

Primitive di comunicazione

Inter-Process Communication (IPC) è un insieme di tecniche utilizzate per lo scambio di dati tra due o più tread di uno o più processi (indispensabile per un corretto funzionamento!!)
Le tecniche di IPC si compongono di metodi per:
- La comunicazione tramite variabili (condivisione di memoria).
- La comunicazione tramite messaggi.
- La sincronizzazione.
- Le chiamate a procedura remote
Ci sono molte API (Application Programming Interface) che possono essere usate per IPC:
- Common Object Request Broker Architecture (CORBA);
- Distributed Computing Environment (DCE);
- Message Bus (MBUS);
- anonymous pipes and named pipes;

Theads: shared variables

Calculi and Languages

Un semplice linguaggio:CSP

Il linguaggio CSP è una architettura parallela caratterizzata da:
- scambio di messaggi tra processi;
- possibilità per i thread di utilizzare memoria condivisa.
Lo scambio di messaggi avviene tramite Canali.
I canali permettono:
- uno scambio di valori tra processi;
- la sincronizzazione di processi.
Il numero dei canali è fisso:
- non è possibile creare o cancellare un canale durante l’esecuzione di un programma;
- è possibile avere canali dedicati a singoli processi.

Sintassi di CSP

Composizioni ben fondate

Una composizione parallela c0 k c1 è ben fondata se c0 e c1 non hanno una locazione comune.
Un comando è ben fondato se tutti i suoi sottocomandi lo sono.
Una restrizione cα nasconde il canale α in modo che possa essere utilizzato solo per comunicazioni interne a c.

Semantica di CSP

Come per IMPGC, utilizziamo una semantica operazionale basata su singoli passi non interrompibili. Legare solamente lo stato iniziale a quello finale (come per IMP) non è sufficiente in presenza di concorrenza.
Anche per CSP, una configurazione è data da un comando e uno stato o solamente da uno stato.
Si consideri allora la seguente configurazione di un comando:

<α ?X;c,σ>

Intuitivamente, questa rappresenta un comando che è pronto a ricevere un valore da associare a X tramite una comunicazione sincronizzata lungo il canale _.
Questo può avvenire se il comando è in parallelo con uno pronto ad eseguire un’azione complementare di output sul canale α.
La semantica di CSP deve esprimere questa dipendenza dall’ambiente. Questo può essere fatto sfruttando la teoria degli automi. Dunque la semantica di CSP è data tramite Labeled Transition Systems (LTS)!!

Label transition semantics

Comunicazioni interne

Si consideri la transizione indicata in figura 1.
In questo caso la transizione non viene etichettata poiché si tratta di comunicazione interna, senza effetti sull’ambiente.
Esistono anche transizione composte (dovute per esempio all’utilizzo di un canale α da più processi) come indicato in figura 2.
Questo cattura la possibilità che il primo componente riceve un valore dall’ambiente piuttosto che dal secondo componente.
Presentiamo adesso la semantica formale come estensione di quella di IMPGC dove ammettiamo comunicazione nelle guardie, e l’uso del comando vuoto E per uniformare le configurazioni.

Figura 1

Figura 2

Alcune semplificazioni nelle regole

Nelle regole di derivazione che daremo nelle prossime slide, utilizzeremo le seguenti semplificazioni:
- una configurazione σ può essere anche vista come una coppia <c, σ > dove c è il comando “nullo” (equivalente dello skip).
- utilizziamo il valore λ per indicare che una transizione può essere etichettata con α?X oppure <α!X oppure anche senza etichetta.

Regole per i comandi I

Regole per i comandi II

Regole per i comandi con guardia

Example: Distributore di cioccolata

Si consideri un distributore di cioccolata interagente con un cliente.
Si assuma che la macchina abbia due possibili stati:
- coin che rappresenta l’inserimento del costo della cioccolata;
- choc che rappresenta la consegna della cioccolata.
La proprietà che forza la macchia a ricevere i soldi prima di offre la cioccolata può essere scritta nel modo indicato in figura 1.

La possibilità che la macchia lavori per sempre si può esprimere con

V = coin → choc → V

Una persona che potrebbe scegliere contanti o carte prepagata per il pagamento potrebbe essere modellata nel modo seguente:

Person = (coin → STOP) □ (card → STOP)

I due processi precedenti possono essere messi in parallelo, in modo da interagire tra loro. Esercizio per gli studenti.

Dining philosophers problem

In informatica, il problema dei filosofi a cena è un classico problema di sincronizzazione di multi-processi
5 filosofi sono seduti ad un tavolo davanti ad un piatto di spaghetti con una forchetta ad ogni lato (dunque, 5 filosofi, 5 piatti e 5 forchette).
Si supponga che ciascuna filosofo ha bisogno di due forchette per mangiare e che esse siano prese una alla volta. Ciascun filosofo, dopo aver preso entrambe le forchette, mangia per un po’, poi posa le forchette e comincia a pensare e poi ciclicamente riprende le forchette.
Il problema è scrivere un algoritmo che evita starvation e deadlock.
- Un Deadlock si può avere se tutti i filosofi hanno una sola for-chetta e nessuno ne può prendere un’altra (catena di deadlock).
- Una Starvation si può verificare se un filosofo non può prendere entrambe le forchette.
La non disponibilità di forchette è analoga alla mancanza di risorse per un programma eseguito su un computer, dovuta alla scarsità di risorse. Una chiara situazione di concorrenza.