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. Il modello Linda. Introduzione al model checking.
Mordechai Ben-Ari. Principles of Concurrent and Distributed Programming, 2/e. Addison-Wesley, 2006.
Obiettivi Formativi
Il corso mira a trasmettere agli studenti i principi alla base della programmazione, specifica e verifica dei sistemi concorrenti. Questo scopo viene perseguito mediante l'introduzione di un modello di riferimento, nel quale descrivere alcuni algoritmi di sincronizzazione fondamentali ed analizzare la loro correttezza.
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
Prova scritta; discussione della prova scritta.
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: Java e Promela.
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.
Algoritmi avanzati per la S.C.: l'algoritmo del fornaio. Prove di correttezza.
Semafori e loro implementazione. Il problema dei filosofi a cena. Prove di correttezza.
Il concetto di Monitor e sue proprieta'. Il problema dei lettori-scrittori. Prove di correttezza.
Comunicazione tramite canali. Implementazioni.
Il modello Linda.
Introduzione alla specifica e alla verifica automatica: LTL, Promela e il model-checking con SPIN.