Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

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:

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 1

Figura 2

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.

Solution for n Dining Philosophers


Verifying the philosophers’ problem


Esercitazione

Esercizio per gli studenti: esempio pag. 331 di Winskel.

  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion