Linguaggi per il Global Computing
Laurea Magistrale in Informatica - Università di Padova
Anno Accademico 2020/2021
Obiettivi del corso
L'enorme diffusione dei sistemi concorrenti, distribuiti e mobili
rende inadeguati i paradigmi di specifica e programmazione classici ed
apre sfide complesse e affascinanti. Appare necessario un
ripensamento, che parta dalle stesse fondamenta e che adotti un
approccio rigoroso, formale, disciplinato. Il corso si propone di
avvicinare lo studente a tematiche di interesse in questo
ambito. Parte dai fondamenti oramai classici dei linguaggi
concorrenti, che pongono al centro dello studio i concetti di
processo, le metodologie di composizione, i meccanismi di
comunicazione (come il Calculus of Communicating Systems ed il
Pi-Calculus) per poi illustrare le ricadute sui linguaggi per la concorrenza e la distribuzione quali ad esempio
Google Go,
Erlang,
Elixir,
Clojure,
Jolie,
Rust,
e le corrispondenti tecniche di programmazione.
Il corso dà luogo al conseguimento di 6 CFU.
Programma di massima del corso
Il corso, della durata di 48 ore, svilupperà i seguenti temi:
- Il "calculus of communicating systems" (CCS), un linguaggio
minimale per la descrizione di sistemi concorrenti.
Equivalenza di processi: Sistemi di transizione e bisimulazione
- Logica di Hennessy-Milner e strumenti per la verifica. Mutua
esclusione, deadlock, fairness. Proprietà di safety e
liveness. Sistemi con topologia dinamica e mobilità:
pi-calcolo. Strumenti di verifica (Concurrency
Workbench, Caal,
PseuCo).
-
Dai linguaggi di specifica ai linguaggi di
programmazione:
Google Go,
Erlang,
Elixir,
Clojure,
Rust,
Jolie,
ORC.
Orario del corso
Il corso fa parte del Corso di Laurea Magistrale in Informatica,
Università di Padova, ed è collocato nel II semestre
dell'Anno Accademico 2020/2021
, con il
seguente orario (se necessario modifiche all'orario potranno poi
essere valutate con i partecipanti al corso). Le lezioni si svolgeranno in modo duale (in presenza e trasmesse a distanza via Zoom).
Giorno |
Orario |
Aula |
Lunedì |
14.30 - 16.00 |
2BC/60 |
Martedì |
14.30 - 16.00 |
2BC/60 |
Modalità d'Esame e Appelli
L'esame si compone di due parti: esercizi ed
approfondimento/progetto (vedi sotto), da preparare off-line e poi
presentare in forma orale/seminariale.
- ESERCIZI
Dovreste svolgere due esercizi nella sezione
Esercizi di
questa pagina
- APPROFONDIMENTO/PROGETTO
Potete scegliere tra varie
possibilità che comprendono un mini-progetto di
specifica/implementazione/verifica formale di proprietà
oppure lo studio di tool di verifica sofisticati oppure un
approfondimento su tematiche relative a modelli formali,
tecniche di verifica, linguaggi di programmazione in qualche
modo connessi ai temi del corso. Anche in questo caso, alcuni
suggerimenti si trovano
nella pagina
dell'esame.
In entrambi i casi, le liste di suggerimenti non sono
esaustive. E' possibile proporre temi di approfondimento
differenti che rispondano ad interessi personali (anche esercizi
diversi, ad esempio scelti dal libro). Una volta effettuata la
scelta, si consiglia di contattare il docente per la definizione
dei dettagli (esercizi e approfondimenti sono spesso descritti in
modo sommario).
Riferimenti bibliografici e materiale didattico
Il corso ha un Moodle che verrà utilizzato per comunicazione e distribuzione di parte del materiale. Per la parte fondazionale si utilizzerà il seguente libro
-
L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba
"Reactive systems"
Cambridge University Press, 2007
(Chap. 1-7, except 6.4)
Il materiale relativo ai linguaggi di programmazione discussi a lezione è fornito tramite il moodle.
Link Utili per fini didattici
- Caal
Una versione
web del concurrency workbench. Funziona nei più comuni
browser.
- PseuCo
Uno strumento interattivo per la definizione e simulazione di
processi scritti in un linguaggio concorrente (stile Go
semplificato), che ha una immediata traduzione in CCS.
- Edimburgh
Concurrency Workbench
Uno strumento interattivo per la definizione, simulazione, prova
di proprietà di processi scritti in CCS (ed in varie estensioni
di questo).
- Sono disponibili i binari per Linux
- Può essere usato in emacs (consigliato),
seguendo le istruzioni specificate
qui.
- syntax highlighting per cwb (fatto utilizzando il package generic-x) cwb-highlight.el
- uDrawGraph (sostituto di daVinci)
Programma che permette la visualizzazione di transition graph in modo grafico nel Concurrency Workbench.
- scaricare la versione precompilata per Linux
- inserire la directory corrispondente in qualsiasi posizione
- settare la variabile di ambiente UDG_HOME al path della directory suddetta
- Bisimulation game and CCS
simulator
Permette di visualizzare e simulare il comportamento di un
processo dato il suo transition graph nel formato prodotto da
Concurrency Workbench e di giocare con le equivalenze
comportamentali.
- richiede di avere Java > 5 e il pacchetto graphViz
- usare la distribuzione fornita e aggiornare il file
properties.txt (indicando il path al binario dot di
graphViz)
- Concurrency Workbench of the new century
Offre funzionalità simili all'Edimburgh Concurrency
Workbench. Supporta vari linguaggi tra cui CCS, CCS con
priorità, timed CCS, CSP, Basic Lotos.
-
TAPAS
un tool con interfaccia grafica per lo studio di processi CCSP
(linguaggio che fonde le primitive di CCS e CSP). Fornisce anche
altri plugin per calcoli stocastici e con code mobility.
- SLMC (spatial
logic model checker). Un tool per la verifica di
proprietà spaziali di processi.
- Mobility Workbench
Simile ai Concurrency Workbench, ma supporta calcoli per la
mobilità come il pi-calcolo.
Alcuni strumenti avanzati
- CADP (Construction and Analysis of Distributed Processes)
- MCRL2 ( micro Common Representation Language 2)
- PAT (Process Analysis Toolkit An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems)