Panoramica sulla Programmazione Concorrente. Il modello Interleaving. Correttezza: proprietà di Safety, Liveness, Fairness. Linguaggi: Java e Promela. Il problema della Sezione Critica. Metodi formali di verifica: prove induttive e la logica LTL. Algoritmi avanzati per la S.C. Semafori e loro implementazione. Il problema dei filosofi a cena. Il concetto di Monitor. Il problema dei lettori-scrittori. Comunicazione tramite canali. Introduzione al model checking.
1. Mordechai Ben-Ari. Principles of Concurrent and Distributed Programming, 2/e. Addison-Wesley, 2006.
2. Note del docente.
Obiettivi Formativi
- Conoscenze. Il corso mira a trasmettere agli studenti i principi alla base della programmazione, specifica e verifica dei sistemi concorrenti, come dettagliati nel programma.
- Competenze. Questo scopo viene perseguito mediante l'introduzione di un modello di riferimento (interleaving). Padroneggiando questo modello, è possibile descrivere e ragionare sugli algoritmi di sincronizzazione fondamentali.
- Capacità. Analizzare la correttezza degli algoritmi concorrenti; scrivere e ragionare sulla correttezza di programmi concorrenti concreti.
Prerequisiti
Familiarità con i concetti fondamentali della programmazione sequenziale; qualche elemento di logica proposizionale.
Metodi Didattici
Lezioni frontali o a distanza.
Altre Informazioni
Ricevimento su appuntamento.
Modalità di verifica apprendimento
L'esame consiste di parti:
1. prova scritta, con svolgimento di esercizi teorici e di programmazione, che possono avere come oggetto uno qualsiasi degli argomenti del programma (*);
2. a seguire, prova orale, centrata principalmente sulla discussione della prova scritta.
Nella prova scritta verrà valutata la comprensione dei modelli, delle primitive linguistiche e degli algoritmi concorrenti visti a lezione, la capacità di analizzare problemi di gestione delle risorse e sincronizzazione tra processi concorrenti, la capacità di applicare le conoscenze acquisite per la risoluzione di problemi nuovi. Per accedere alla prova orale è necessario superare la prova scritta.
Nella prova orale verrà valutata la conoscenza degli argomenti presentati, l'acquisizione del linguaggio tecnico adeguato al contesto, la capacità di mettere in relazione fra loro argomenti diversi del programma.
La votazione riportata nella prova scritta incide maggiormente (90%) sulla votazione finale.
(*) numerosi esempi di prove scritte sono resi disponibili per gli studenti attraverso la piattaforma di e-learning.
Programma del corso
Panoramica sulla Programmazione Concorrente: sistemi, linguaggi e modelli.
Un modello astratto: esecuzione di comandi atomici e il modello interleaving. Stati, transizioni, diagramma degli stati, computazioni.
Correttezza: proprietà di Safety e Liveness. L'assunzione di Fairness.
Linguaggi di programmazione e specifica: concorrenza in Java.
Il problema della Sezione Critica: l'algoritmo di Dekker.
Metodi formali di verifica: prove induttive di invarianti; la logica LTL e il ragionamento deduttivo; prova deduttiva di correttezza dell'algoritmo di Dekker.
Semafori e loro implementazione. Il problema dei filosofi a cena. Prove di correttezza. Semafori in Java.
Il concetto di Monitor e sue proprieta'. Il problema dei lettori-scrittori. Prove di correttezza. Monitor in Java.
Comunicazione tramite canali. Implementazioni.
Canali sincroni in Java.