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.
2) 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. L'esame consiste in una selezione di esercizi e domande. Gli esercizi mirano a valutare la capacità degli studenti di applicare conoscenze teoriche e tecniche per modellare e risolvere problemi di Programmazione Concorrente. Particolare attenzione è dedicata alla valutazione della correttezza dei procedimenti seguiti, nonché all'originalità e all'efficacia dei metodi adottati.
Le domande sono strutturate per verificare la conoscenza e il grado di comprensione della teoria trattata nel corso. Una serie di esempi di prove è disponibile per gli studenti sul sito ufficiale del corso.
Programma del corso
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.