Metodi Formali per la Concorrenza

(Ovvero, tutto ciò che volete sapere sui sistemi distribuiti e non avete mai osato dimostrare)

Laurea in Informatica - Università di Padova
Anno Accademico 2009/2010

Paolo Baldan
Silvia Crafa

Obiettivi del corso

Il corso si propone di illustrare vari modelli e strumenti proposti in letteratura per la descrizione formale di sistemi concorrenti e distribuiti e per la verifica di proprietà di tali sistemi. Il corso non si focalizzerà solo sulle basi teoriche ma discuterà anche l'uso di alcuni tool come il "Edinburgh Concurrency Workbench". Il corso dà luogo al conseguimento di 6 CFU.

Programma di massima del corso

Il corso, della durata di 48 ore, svilupperà i seguenti temi:
  1. Introduzione alla concorrenza e mobilità: dagli automi ai sistemi reattivi e concorrenti.
  2. Il "calculus of communicating systems" (CCS), un calcolo minimale per la descrizione di sistemi concorrenti
  3. Equivalenza di processi: Sistemi di transizione e bisimulazione
  4. Proprietà dei processi: La logica di Hennessy-Milner e strumenti per la verifica
  5. Dal CCS ai calcoli per sistemi con mobilità (pi-calcolo, calcolo degli ambienti, ecc.) e per i web-services.
  6. L'uso dei tipi per ragionare sui sistemi distribuiti
Altri possibili approfondimenti riguardano:

Orario del corso

Il corso fa parte del Corso di Laurea Specialistica in Informatica, Università di Padova, ed è collocato nel II trimestre dell'Anno Accademico 2009/10, con inizio il 11.01.2010 e termine il 12.03.2010, con il seguente orario (modifiche all'orario potranno poi essere concordate con i partecipanti al corso):
Giorno Orario Aula
Lunedì 9.30 - 11.30 1BC/45
Martedì 9.30 - 11.30 1BC/45
Venerdì 9.30 - 11.30 1BC/45

Diario del corso

Indicazione dei temi discussi durante le lezioni e degli esercizi svolti in classe e assegnati per casa (la numerazione si riferisce al testo adottato).
  1. Introduzione e note storiche
  2. CCS: Introduzione informale
  3. CCS: definizione formale (con Esercizi 2.1, 2.2, 2.3). Esercizi: 2.7, 2.8, 2.9, 2.10 per casa
  4. Discussione degli esercizi per casa. Esercizio 2.11. Esercizio: Terminazione del CCS finito (senza il costrutto di costante). Value passing CCS. Esercizio 2.12 (Per casa: contatore con CCS value passing, corrispondenza tra CCS e CCS value passing)
  5. Equivalenze comportamentali: proprietà desiderate Equivalenze comportamentali: alcune equivalenze non completamente soddisfacenti (iso di LTS, tracce, tracce complete). Bisimulazione. La bisimilarita` forte ~.
    (Esercizi per casa: 3.3, 3.4, 3.5).
  6. Discussione esercizi
  7. Proprietà della bisimilarità forte (massima bisimulazione, equivalenza). String bisimulation (Es. 3.9). Esercizio 3.11 (Proprietà del parallelo) e Esercizio 3.12.
    Esercizi per casa: String bisimulation (Es. 3.9). Relazione tra tracce (complete) e bisimilarita` (Es. 3.11).
    La bisimilarità forte è una congruenza.
  8. Formalizzazione della bisimulazione come gioco.
    Esercizi per casa: Es. 3.15. Bisimulazione up-to.
  9. Altre equivalenze: simulation equivalence, ready simulation equivalence.
    Esercizi per casa:
    - Provare che il preordine di simulazione è un preordine, una congruenza, implica la trace inclusion.
    - Provare che il preordine di simulazione ready è un preordine, una congruenza, implica la trace inclusion,e la complete trace inclusion.
    - Provare le inclusioni strette tra le varie equivalenze discusse (simulation equivalence, ready equivalence, trace equivalence, complete trace equivalence, bisimulation equivalence)
    - Provare che la weak bisimilarity coincide con la strong bisimilarity definita sul LTS weak
  10. Esercizi
  11. Introduzione alla weak bisimilarity. Fair abstraction from divergence e non osservabilità della divergenza. Esercizio: buffer fifo con capacità 2. Esercizio 3.26. Proprieta` di congruenza della bisimilarità debole.
    Esercizi per casa: 3.27, 3.28, 3.29.
  12. Conguenza osservazionale.
    Esercizi per casa:
    - Formulazione dei 5 filosofi di Dijkstra che evita il deadlock
    - dimostrare che la chiusura contestuale della bisimilarità debole è la più grande congruenza che raffina la bisimilarità debole
    - dimostrare che la suddetta relazione è la congruenza osservazionale (**)
  13. Bisimilarità come massimo punto fisso.
    Esercizi per casa:
    - Verificare che se F è il funzionale della bisimulazione, allora le relazioni F(n)(Proc x Proc) sono tutte equivalenze
    - Dimostrare che se D è un reticolo completo numerabile e F : D -> D una funzione monotona allora il minimo punto fisso si ottiene come supnF(n)(0), dove 0 è il minimo del reticolo.
  14. Logica di Hennessy-Milner. Teorema di Hennessy-Milner. Esercizi
  15. Logica di Hennessy-Milner con ricorsione
  16. Semantica formale della logica di Hennessy-Milner con ricorsione ed esercizi
  17. Mutua esclusione in CCS
  18. Dal CCS al pi-calcolo
  19. Sintassi e semantica a riduzioni. Esempi.
  20. LTS per il pi-calcolo
  21. Bisimuazione forte e bisimulazione up to congruenza strutturale
  22. Sistema di tipi semplici. Subtyping per distinguere capabilities di lettura e scrittura sui canali. Uso dei tipi per ragionare sui processi
  23. L'uso dei tipi nelle reti aperte: provare una proprieta' di secrecy in presenza di componenti untrusted.

Modalità d'Esame e Appelli

L'esame consiste nello svolgimento di alcuni esercizi assegnati durante l'anno e in un'attività di approfondimento finale, che lo studente poi dovrà presentare in forma seminariale.

Più precisamente, la prova finale consiste nello svolgimento di due esercizi e, a scelta, nella realizzazione di un mini-progetto o nell'approfondimento di un argomento tra quelli elencati nel seguito (temi alternativi, concordati con il docente sono comunque possibili). Il tutto andrà presentato in forma seminariale, in un tempo pari ad un'ora circa.

I temi d'esame si possono trovare qui.

Riferimenti bibliografici

Si utilizzerà il seguente libro

Per le lezioni sul pi-calcolo sono disponibili i seguenti appunti.

Un testo molto utile per consultazione è

Alcuni riferimenti per la parte sul pi-calcolo:

Link Utili