Sumários
Aula 1 12/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 Exclusão Mútua. Propriedades de seguranças e vivacidade. Locks. Objectos concorrentes. Semáforos e Monitores.
Breve introdução à programação concorrente: processos e interação. Paralelismo e Concorrência Exclusão Mútua. Propriedades de seguranças e vivacidade. Locks. Objectos concorrentes. Semáforos e Monitores.
Bibliografia
CPAPF: Cap 1., 3.1.1, 3.2.1 3 3.3.1. Ler ainda 3.2.2 e 3.3.2
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.
Bibliografia
ITC: 2.1 e 2.2
CCS sequencial: operadores prefixo e escolha. Nomes de processos e definições recursivas. Semântica das expressões por sistemas de transições. Regras de inferência. Expressões guardadas.
Bibliografia
ITC: 3.1.1 e 3.1.2 ; RS: 2.1-2.2
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. O CCS completo: operador de renovação. O CCS regular. Exemplos de buffers e protocolos.
Bibliografia
ITC3.2-3.4, RS: 2.2 , Regras do CCS
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. Bisimulação (forte). Bisimilaridade. Prova da bisimilaridade de dois processos. Jogo de bisimulação. Propriedades da bisimilaridade.
Bibliografia
RS: 3.1, 3.2 e 3.3
Bisimulação fraca. Bisimilaridade fraca. Prova da bisimilaridade fraca de dois processos. 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
RS: 3.4-3.6
Para quem quiser saber mais sobre bisimulações (facultativo): "Introduction to Bisimulation and Coinduction", D. Sangiori 2012, CUP
Para quem quiser saber mais sobre bisimulações (facultativo): "Introduction to Bisimulation and Coinduction", D. Sangiori 2012, CUP
Aula 7 21/03
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. PseuCo: linguagem para processos concorrentes. Comunicação por partilha de variáveis e passagem de mensagens: canais síncronos e assíncronos.
Aula 8 26/03
PseuCo (cont): Comunicação por passagem de mensagens: canais síncronos e assíncronos. Memória partilhada. Data Races. Prevenir data races: mutex/. Locks e Monitores em PseuCo. Semáforos. Exemplos usando semáforos implementados com um monitor.