Sumários

Aula 1 11/02

Objectivos da disciplina e tópicos do programa: parte I e parte II. Métodos de avaliação. Bibliografia recomendada.
Breve introdução à programação concorrente: processos e interação. Paralelismo e Concorrência

CPAPF: Cap 1., 3.1.1, 3.2.1 3 3.3.1. Ler ainda 3.2.2 e 3.3.2

Aula 2 18/02

Modelo abstracto de processos: sistemas de transição. Estados e Ações. Sucessores de um estado. Estados atingíveis. Determinismo e Não determinismo. Tipos de Sistemas de transição. Processos Concorrentes.

ITC: 2.1 e 2.2

Aula 3 20/02

CCS sequencial: operadores prefixo e escolha.Semântica das expressões por sistemas de transições. Regras de inferência.

RS: 2.1-2.2 ; ITC: 3.1.1 e 3.1.2 ;

Aula 4 27/02

Nomes de processos e definições recursivas. Expressões guardadas. O operador composição paralela. Acções de entrada e de saída. Ações complementares. Sincronização. O operador de restrição. Regras de inferência.

ITC3.2-3.4, RS: 2.2 , Regras do CCS

Aula 5 3//03

Exemplos com composição paralela e restrição. O CCS completo: operador de renovação. O CCS regular. Exemplos de buffers e protocolos.

Aula 6 05/03

Equivalência de comportamentos de Processos. Traços. Critérios para a equivalência: relações de equivalência, de congruência e sensíveis a deadlocks. Isomorfismo e equivalência de traços.

RS: 3.1, 3.2; ITC 2.3.1-2

Aula 7 10/03

Bissimulação (forte). Bissimilaridade. Prova da bissimilaridade de dois processos. Jogo de bissimulação. Propriedades da bissimilaridade.

Bibliografia
RS: 3.3, 3.5
Para jogos de bissimulação: CAAL (sintaxe do CCS diferente do pseuco.com)

Para quem quiser saber mais sobre bissimulações (facultativo): "Introduction to Bisimulation and Coinduction", D. Sangiori 2012, CUP

Exemplos de Bissimulação Forte. Bissimulação fraca. Bissimilaridade fraca. Prova da bissimilaridade fraca de dois processos. Propriedades da bissimilaridade fraca

Bibliografia:
R.S 3.3, 3.4,3.5 (CAAL)

Continuação da aula anterior: Exemplos de bissimulação fraca. Jogos de bissimilaridade fraca. Propriedades da bisimilaridade fraca. Bisimilaridade fraca não é uma congruência. Congruência para a escolha. Congruência Observável. Minimização de Sistemas de Transição

Bibliografia:
R.S 3.4, 3.5 (CAAL)
Exemplos: exemplos caal

Expressividade do CCS. Escrita de programas imperativos em CCS: Algoritmo de Peterson para a exclusão mútua.
CCS com passagem de valores (CCS_vp). Regras para substituir variáveis por valores e calculo de valores. Parâmetros em nomes de processos e regra da recursão. Representação de escrita e leitura em células de memória, Programas funcionais e imperativos em CSS_vp. CCS_vp embebido em CCS.

Bibliografia:
R.S 7

PseuCo: linguagem para processos concorrentes. Comunicação por partilha de variáveis e passagem de mensagens: canais síncronos e assíncronos. Comunicação por passagem de mensagens: canais síncronos e assíncronos. Memória partilhada. Data Races. Prevenir data races: locks.

PseuCo (cont. da última aula): Propriedades Data Races. Prevenir data races analisando o grafo de programa. Locks e Monitores em PseuCo. Monitores e Condições. Semáforos: definição, invariante e propriedades. Exemplos usando semáforos implementados com um monitor.

Bibliografia:
CPAPF: Cap. 1- 3
Pseuco.com
TACAS

Monitores em PseuCo: exemplo da construção de um canal. Semáforos. Exemplos usando semáforos implementados com um monitor: rendezvous, mutex,multiplex e barreiras.

Bibliografia:
Pseuco.com
Little Book of Semaphores Cap.1-3
CPAPF: Cap. 1- 3
TACAS