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.
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 sugli argomenti del corso (*);
2. a seguire, prova orale, centrata sulla discussione della prova scritta.
(*) 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.