Especificação de Sistemas
Distribuídos
Alexandre Mota/Augusto Sampaio
{acm, acas}@cin.ufpe.br
Motivação

Lidar com tarefas simultaneamente
não é simples



Memória compartilhada ou troca de
mensagens
Deadlock, livelock e não-determinismo
Especificação muito longe da
implementação
Objetivo



Modelar sistema concorrente e/ou
distribuído usando uma linguagem de
especificação (CSP)
Analisar propriedades dessa
especificação
Detalhar (refinar) a especificação até
chegar em implementação
(JCSP/UML-RT)
CSP




Notação conveniente para modelar
sistemas concorrentes
Alto nível de abstração
Ferramentas para analisar
propriedades automaticamente
Possui biblioteca para Java (JCSP)
Exemplo de CSP

Considere o problema do jantar dos
filósofos, com 5 filósofos envolvidos
PHIL(0)
FORK(0)
FORK(1)
PHIL(1)
PHIL(4)
FORK(2)
FORK(4)
FORK(3)
PHIL(3)
PHIL(2)
Exemplo de CSP
PHIL(i) = sitdown.i -> pickup.i.inc(i) -> pickup.i.i ->
putdown.i.inc(i) -> putdown.i.i -> getup.i -> PHIL(i)
FORK(i) = pickup.i.i -> putdown.i.i -> FORK(i)
[] pickup.dec(i).i -> putdown.dec(i).i -> FORK(i)
PHILS = || i:{0..4} @ [{|...|}] PHIL(i)
FORKS = || i:{0..4} @ [{|...|}] FORK(i)
COLLEGE = PHILS [ |...| ] FORKS
ProBE



Será que nossa especificação CSP se
comporta como imaginamos?
Para saber isso, podemos animar seu
comportamento através de ProBE
Vamos exercitar o exemplo anterior
(dphil.csp) com o ProBE…
FDR

Será que nossa especificação CSP
obedece a requisitos essenciais sobre
sistemas concorrentes e distribuídos?


Dealock, Livelock e Não-determinismo
Vamos investigar nosso exemplo
usando o verificador de modelos
FDR…
Projeto 1




Escolher sistema concorrente para
ser especificado
A partir da modelagem, estudar as
seguintes propriedades clássicas:
deadlock, livelock e determinismo
Na presença indesejável, ajustar o
modelo
Resultado: modelo e análises básicas
JCSP





Biblioteca para Java que suporta CSP
Programação concorrente elegante
Possível usar memória
compartilhada/passagem de
mensagens
Todos os recursos de Java
Talvez requeira refinamento
Ou UML-RT…
Projeto 2





A partir do modelo em CSP, implementar
em JCSP
Adicionar à implementação requisitos nãofuncionais
Portanto, o projeto deve ser desafiador e
não meramente teórico
Pode usar dos conceitos usados nos
fundamentos
Resultado: documentação de descrição,
programa e análise com o Java PathFinder
Jantar Filósofos em JCSP
Jantar Filósofos em JCSP
Jantar Filósofos em JCSP
Java PathFinder

Java PathFinder (JPF) is a system to verify
executable Java bytecode programs. In its
basic form, it is a Java Virtual Machine
(JVM) that is used as an explicit state
software model checker, systematically
exploring all potential execution paths of a
program to find violations of properties
like deadlocks or unhandled exceptions
(JPF site)
Desenvolvendo o Sistema
ProBE, FDR
FDR
FDR
Análise
Projeto
Projeto
(CSP)
(CSP)
(CSP)
JPF
…
Implementação
(JCSP)
(JCSP)
(UML-RT)
(Java)
(CSP.Net)
(CSP.Net)
Análise automática de propriedades
{deadlock, livelock, determinismo}
Projeto baseado em Refinamento
Avaliação




Projeto CSP (A)
Projeto JCSP (B)
Prova (C)
Nota = ((A+B)/2+C)/2
Presença requisitada
Definir projeto até 03/10/07
Referências







Andrews, G.R. Multithreaded, Parallel, and
Distributed Programming. Addison-Wesley, 2000.
Roscoe, A.W. The Theory and Practice of
Concurrency. Prentice-Hall, 1998.
Hoare, C.A.R. Communicating Sequential Processes.
Prentice-Hall, 1985.
Welch, P. Communicating Sequential Processes for
Java. 2003.
CSP.Net
QuickStone. JCSP Network Edition. 2004.
QuickStone. xCSP Technology. 2004.