Corso di Teoria della Concorrenza (dott. Gorla) - AA 2009-2010

Il corso di Teoria della Concorrenza è incentrato sulla semantica formale e matematica dei linguaggi di programmazione concorrenti. Il corso è strutturato in due parti. Una parte iniziale descrive le nozioni preliminari di ogni linguaggio concorrente (esecuzione di processi paralleli, semantica basata sull'interleaving, sincronizzazione, comunicazione, non-determinismo, simulabilità di programmi) e ne presenta un opportuno modello matematico. La seconda parte aggiunge a tali concetti meccanismi più avanzati di programmazione, quali creazione e scambio di nomi, sistemi di tipo per la verifica di proprietà di programmi, crittografia, distribuzione.

Il corso integra parti di didattica a problematiche di ricerca relativamente recenti e ancora aperte. La prima parte verte sul CCS; la seconda parte verte sul pi-calcolo.

Orario delle lezioni

Le lezioni si svolgeranno secondo il seguente orario:

Testi consigliati

Per la parte sul CCS:

• dispense
• R. Milner. Communicating and Mobile Systems. Cambridge University Press, 1999. Il testo è disponibile in biblioteca; verranno usati i capitoli 1, 2 (saltare sez. 2.3), 3, 4 (saltare sezioni 4.1, 4.4, 4.5 e 4.6), 5 (senza prop. 5.2, es 5.3, lemma 5.4 e 5.5, teor. 5.6, def. 5.17, prop. 5.18, prop. 5.23), 6 (senza sez. 6.3) e 7 (sez. 7.2 e 7.3).
• R. Cleaveland and S. Smolka. Process Algebra. In Encyclopedia of Electrical Engineering, John Wiley & Sons, 1999. Disponibile on-line all'indirizzo http://www.cs.umd.edu/~rance/publications/papers/ee99.ps.gz. Saranno presentate a lezione le sezioni 3.2, 4.1 e 4.2.
• R. Cleaveland and O. Sokolsky. Equivalence and Preorder Checking for Finite-State Systems. In "Handbook of Process Algebra," pp. 391-424, Elsevier, 2001. Disponibile on-line all'indirizzo http://www.cis.upenn.edu/~sokolsky/PAhandbook.pdf. Sarà presentata a lezione la sezione 3.1.

Per la parte sul pi-calcolo, sono disponibili le dispense del docente, che contengono tutto e solo il materiale esposto a lezione. Per eventuali letture di approfondimento, si riportano di seguito anche i riferimenti e, se possibile, i link agli articoli 'classici' sul tema.

• dispense
• J. Parrow. An Introduction to the pi-Calculus. In Handbook of Process Algebra, pages 479-543. Elsevier, 2001. Disponibile on-line alla pagina web http://user.it.uu.se/~joachim/intro.ps
• R. Milner. The Polyadic pi-Calculus: A Tutorial. In Logic and Algebra of Specification. Springer-Verlag, 1993. Disponibile on-line alla pagina http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps
• D. Sangiorgi, D. Walker. The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, 2001. Questo è attualmente il libro più completo sul pi-calcolo (N.B.: il libro può risultare troppo complesso per studenti della laurea specialistica; è più che altro rivolto a dottorandi e ricercatori)
• Altri articoli consigliati dal docente nel corso delle lezioni

Programma del Corso

Il programma segue la divisione del corso in due parti:

• La prima parte è svolta studiando il CCS (Calculus of Communicating Systems [Milner:1980]). In tale ambito saranno affrontati i seguenti temi:
  • non-determinismo
  • ricorsione
  • sistemi di transizione etichettati
  • composizione parallela ad interleaving
  • sincronizzazione
  • restrizione
  • bisimulazione: versione strong e weak, assiomatizzazioni, caratterizzazione logica, verifica algoritmica.

• La seconda parte è incentrata sul pi-calcolo. In tale ambito saranno affrontati i seguenti temi:
  • creazione e passaggio di nomi e relativa modifica delle connessioni tra processi
  • semantica a riduzioni e semantica etichettata
  • bisimulazione e relative proprietà di congruenza
  • variante poliadica (sistema di tipi per assicurare correttezza delle comunicazioni e codificabilità nel pi-calcolo di base)
  • variante asincrona e codificabilità delle comunicazioni sincrone
  • variante higher-order e codificabilità nel calcolo di base
  • Turing-completezza del pi-calcolo tramite codifica del lambda-calcolo
  • pi-calcolo come modello per linguaggi ad oggetti

Modalità di esame

Ci sono varie modalità per sostenere l'esame:

• 1^ parte: esonero
• 2^ parte: svolegimento di tesine su argomenti di ricerca di difficoltà ragionevole concordati con il docente da esporre nel corso delle lezioni agli altri studenti del corso (modalità consigliata a chi intende svolgere la propria tesi su questi argomenti)
• sostenere un esame orale su tutti gli argomenti svolti a lezione (N.B.: questa modalità è indicata agli studenti che non seguono le lezioni).

Link ad articoli per eventuali tesine

• http://www.cs.unibo.it/~zavattar/Publication/icalp03.ps. Un lavoro che confronta ricorsione e replicazione in calcoli di processo. TESINA GIA' ASSEGNATA
• http://www.cs.unibo.it/~sangio/DOC_public/pi.ps.gz. Un 'classico' che estende il sistema di tipi visto a lezione con nozioni di sottotipaggio. TESINA GIA' ASSEGNATA
• http://www.cs.unibo.it/~zavattar/Publication/tcs00.ps. Un articolo che compara l'espressività di tre diversi modi di modellare output asincroni in un calcolo di processo stile CCS.
• http://lucacardelli.name/Papers/Mobility%20and%20Security.A4.pdf. Un bel lavoro di survey su un calcolo che è andato molto di moda qualche anno fa per modellare sistemi distribuiti e mobili. Questo articolo si presta molto bene a due tesine: la prima sulle prime tre parti e la seconda sulle parti IV e V.
• http://lucacardelli.name/Papers/Brane%20Calculi.pdf. Un lavoro curioso sull'uso di calcoli di processo per finalità biologiche (oggi vanno molto di moda!). TESINA GIA' ASSEGNATA