Introdução a CSP

Prévia do material em texto

Introdução	a	CSP	
	
Disciplina:	Métodos	formais	2016.2	
Sidney	Nogueira	
(sidney.ufrpe@gmail.com)	
Roteiro	
•  Concorrência,	paralelismo	e	distribuição	
•  Visão	geral	de	CSP	
•  Comunicação	
•  Eventos	e	canais	
•  Operador	de	prefixo	
•  Recursão	
•  Operadores	de	escolha	externa	
•  Exemplos	
Concorrência	
(um	processador)	
CPU	
Cache	
Memória	
Um	único	processador	e		
uma	memória	
Distribuição	
(processadores	conectados	pela	rede)	
Vários	
processadores	e	
memórias.	
Comunicação	
acontece	por	
passagem	de	
mensagens.	
CSP	
•  CommunicaMng	SequenMal	Processes		
•  É	uma	linguagem	de	especificação	formal	projetada	
para	modelar	aplicações	concorrentes	e	distribuídas	
de	forma	simples	e	elegante	
•  Usa	troca	de	mensagens	para	modelar	comunicação		
–  mas	é	possível	simular	comparMlhamento	de	memória	
•  Concebida	por	Tony	Hoare	[85]	e	atualizada	por	Bill	
Roscoe	[97]	
	
CSP	
•  Baseada	em	uma	sólida	teoria	
•  Possui	várias	ferramentas	para	simulação	e	
verificação	de	refinamento	de	forma	automaMca	
–  FDR,	PAT,	Probe,	gCSP,	Casper,	ProB,	etc	
•  Inspirou	linguagens	de	programação:	Occam,	Go,	
Limbo	
•  Inspirou	bibliotecas	para	programação	distribuída	
–  Java	(JCSP,	JTJ)	
–  Scala	(CSO)	
–  C++	(C++CSP2)	
	
CSP	
•  Livro	Communica9ng	Sequen9al	Processes	de	Tony	
Hoare	(1985)	era	o	3o	livro	mais	citado	da	Ciência	da	
Computação	em	2006		
•  Usada	no	mundo	industrial,	exemplos:	
–  Daimler-Benz	Aerospace:	verificação	do	arquitetura	do	
INMOS	T9000	Transputer		
–  Praxis:	verificação	da	segurança	de	smart	cards		
		
CSP	
•  Possui	notação	matemáMca	(uMlizada	nos	livros	e	
arMgos)	
•  Possui	notação	ASCII	uMlizada	por	ferramentas	
–  Exemplo:	CSPM	para	FDR	
•  Vamos	usar	a	notação	CSPM	
Elementos	básicos	de	CSP	
•  A	linguagem	é	composta	por:	
–  Eventos	
–  Processos	
–  Operadores	sobre	processos	
–  Estruturas	de	dados	baseadas	no	paradigma	funcional	
•  É	considerada	uma	álgebra	de	processos	pois	os	
operadores	possuem	propriedades	algébricas:	
–  AssociaMvidade,	comutaMvidade,	distribuMvidade,	
idenMdade,	etc	
Elementos	básicos	de	CSP	
•  Especificação	de	uma	ATM	em	CSPM	
channel incard, outcard: CARD 
channel pin: PINs 
channel req, dispense: WA 
 
 
 
ATM1 = incard?c -> pin!fpin(c) -> 
 req?n -> dispense!n -> 
 outcard.c -> ATM1 
 
Processo	 Evento	
Operador	de	
prefixo	
Declaração	de	
eventos	e	canais	
Processos	
•  Processos	correspondem	a	componentes	de	um	
sistema	distribuído	
•  Cada	processo	possui	seu	próprio	estado	
–  Semelhante	a	um	objeto	
•  Processos	comunicam-se	com	outros	
Comunicação	
•  Realizada	através	de	eventos	de	comunicação	
•  Eventos	são	atômicos,	instantâneos	
•  A	comunicação	ocorre	através	da	sincronização	
entre	dois	ou	mais	processos:	
–  Mesmo	evento	ocorre	em	dois	processos	ao	mesmo	
tempo	
•  Isto	vai	ficar	mais	claro	quando	vermos	o	operador	
de	paralelismo	
Ambiente	
•  Suponha	P1	é	um	processo	CSP,	seu	ambiente	é	
formado	por	todos	os	outros	processos	com	os	quais	
ele	interage	através	do	operador	de	paralelismo.	
–  Ex:	o	ambiente	de	P1	é	P2	e	P3	na	expressão	P1	||	P2	||	
P3	
•  Quando	só	temos	um	processo	P	seu	ambiente	é	
formado	por	um	processo	que	existe	implicitamente	
		
	P	||	Ambiente	
Canal	e	comunicação	
•  Declaração	de	canal	
–  channel ch: T	
•  Expressões	de	comunicação	
–  ch?var para	recebimento	de	dados	(“entrada”)	
–  ch!exp para	“envio”	(”saída”)	de	dados	
–  ch.exp		similar	ao	anterior	
•  ch?(1+x)	é	errado,	porém	ch!(x+1)	ou	ch.(x+1)	são	
corretos	
Comunicação	restrita	
•  A	declaração	a	seguir	é	muito	custosa	para	analisar		
(muitas	possibilidades)	
–  channel ch: Int 
•  Uma	forma	alternaMva	e	mais	restrita	seria	usar	um	
subconjunto	dos	inteiros	
–  channel ch: {1..10} 
Comunicação	restrita	
•  Outra	forma	de	diminuir	o	custo	é	dizer	na	
comunicação	um	subconjunto	
–  Exemplo:	ch?x:{0,1,2} só	permite	a	leitura	de	3	
valores	apesar	do	Mpo	do	canal	ser	inteiro	
•  Outras	possibilidades	
–  ch?x:{x<=10} 
–  ch?x?y:{(x-1)..(x+1)} 
–  ... 
Eventos e alfabetos	
•  αP	denota	o	alfabeto	de	um	processo	P	:	conjunto	de	
todos	os	eventos	comunicados	pelo	processo	
–  Exemplo:	αATM1	=	{req.20,	req.10,	req.30,...,	dispense.10,	
dispense.30,	...}	
•  Σ	denota	o	alfabeto	de	uma	especificação:	a	união	
dos	alfabetos	de	todos	os	processos	(Events	em	FDR)	
Eventos e alfabetos	
•  A	escolha	de	eventos	deve	ser	cuidadosa	para	não	
tornar	o	modelo	analisável	(explosão	de	estados)	
•  Exemplo:	channel tecla : X	pode	ser	
subsMtuido	por	channel tecla quando	o	valor	
da	tecla	pressionada	for	irrelevante	
Eventos	
•  Denotam	acontecimentos	do	mundo	real	relevantes	
para	o	modelo	
•  Exemplos:	
–  Chamadas	de	métodos	
–  Fatos/ações	percepxveis	(computador	travou,	
pressionamento	de	uma	tecla,	etc.)	
–  Sinais	de	sincronização	(espere,	conMnue,	etc)	
Canais	
•  A	diferença	básica	de	canais	para	eventos	é	que	
canais	comunicam	dados	
•  Assim	
–  channel ev (É	um	evento)	
–  channel ch: {0..10}	(É	um	canal)	
Tudo	são	eventos	
•  A	notação	de	canais	é	uma	facilidade	sintáMca	para	
definir	coleções	de	eventos	
•  Assim	o	canal	
–  channel	ch:	Int	
•  Representa	o	conjunto	de	eventos	
–  {…,ch.-2,	ch.-1,	ch.0,	ch.1,	…}	
•  O	operador	{|canal|}	retorna	todos	os	eventos	de	
um	canal	
–  {|ch|}	=	{…,ch.-2,	ch.-1,	ch.0,	ch.1,	…}	
STOP	
•  Representa	um	processo		
–  Em	deadlock,	ou		
–  Quebrado	
•  Processo	sem	aMvidade	interna	e	externa	(parado)	
–  Representa	um	estado	terminal,	de	onde	não	é	possível	
sair	
	
Deadlock	
•  Em	CSP,	o	deadlock	pode	ocorrer	em	duas	situações	
•  Com	o	uso	do	processo	STOP	
–  Pode	representar	uma	quebra	ou	falha	do	sistema	
•  Situação	de	impasse	
–  Acontece	quando	todos	os	processos	entram	um	estado	
de	espera	
–  É	dinâmico	e	deve	ser	evitado	(erro	na	modelagem)	
SKIP	
•  Processo	básico	que	denota	término	com	sucesso	
–  Comunica	√	e	termina	
•  Sucesso	é	representado	pelo	evento	especial	Mck	(√)	
–  Depois	de	Mck	não	aparece	outro	evento	
•  √	não	é	um	evento	que	faz	parte	do	alfabeto	do	
processo	e	não	pode	ser	comunicado	com	operador	
de	prefixo	
–  ∑√	=	∑	∪	{√}	
	P	=	SKIP	é	um	processo	CSP	válido!	
	P	=	√	->	STOP	não	é	válido!	
Prefixo	
•  Operador	usado	para	modelar	comportamento	
sequencial	(->)	
–  ev -> Proc 
•  O	processo	a	->	P	espera	indefinidamente	por	a,	e	
então	comporta-se	como	P	
•  Exemplo:	
–  TwoSteps = leftFoot -> rightFoot -> 
SKIP 
•  Formas inválidas: a -> b, P -> Q	
 
 
 
	
	
 
 
Definindo Processos	
•  Declarando	os	eventos	(ou	canais)	de	comunicação: 
 
channel up, down 
 
•  Definindo	(nomeando)	um	processo	cujo	alfabeto	é	
determinado	pelos	eventos	acima: 
 
P0 = up -> down -> up -> down -> 
STOP 
Definições Recursivas 
 P1 = up -> down -> P1 
 P2 = up -> down -> up -> down -> P2 
•  Definidas	através	de	equações	recursivas	guardadas	
(comunica	ao	menos	um	evento	antes	da	recursão)	
•  UMlizadas	para	processos	que		
–  tem	um	comportamento	repeMMvo	
–  normalmente	não	terminam	
Definições mutuamente recursivas 
 Pu = up -> Pd 
 Pd = down -> Pu 
 
•  Um	processo	não	“chama”	um	outro	processo,	mas	
“comporta-se	como”	um	outro	processo	
Especificação ATM completa 
CARD = {0..9} 
datatype pinnumbers = PIN.Int 
fpin(c) = PIN.c 
PINs = {fpin(c) | c <- CARD} 
WA = {10,20,30,40,50} 
 
channel incard, outcard:CARD 
channel pin:PINs 
channel req, dispense:WA 
 
ATM1 = incard?c -> pin.fpin(c) -> 
 req?n -> dispense!n -> 
 outcard.c -> ATM1 
 
 
 
 
Escolha	DeterminísMca	
•  []é	o	operador	de	escolha	determinísMca	de	CSP	
	
•  O	processo	P [] Q oferece	a	possibilidade	tanto	
de	se	comportar	quanto	P	quanto	como	Q 
•  A	decisão	sobre	P	ou	Q	não	pertence	a	P [] Q,	mas	
de	quem	interage	com	ele	(ambiente,	decisão	
externa)	
Entrada	e	escolha	
req?n -> P 
req.10 -> P[10/n] 
[ ] 
… 
[ ] 
req.50 -> P[50/n] 
Lembre	que	a	declaração	de	req	é		
channel	req	:	{10,20,30,40,50}	
	
A	expressão	req?n	no	processo	ATM1	corresponde	a	
uma	escolha	externa	como	mostrado	a	seguir.	
Escolha	externa	indexada	
[]x:Sigma @ x -> STOP 
a -> STOP 
[ ] 
b -> STOP 
[ ] 
up -> STOP 
[ ] 
down -> STOP 
Quando	não	temos	um	canal,	é	possível	fazer	a	
escolha	usando	os	eventos	de	um	conjunto	
	
Seja	Sigma	um	conjunto	de	eventos	{a,b,up,down}	
declarado	anteriormente	
Processos RUN	
•  Processo	que	comunica	todas	as	sequência	possíveis	
de	eventos	do	conjunto	X	
 
RUN(X) = [] x:X @ x -> RUN(X) 
 
Escolha prefixada 
•  Operador	para	expressar	escolha	externa	indexada	
(usado	no	livro	e	na	explicação	de	semânMca	de	
alguns	operadores)	
 
?x:A -> P(x) 
 
 onde	x	é	uma	variável,	A	um	conjunto	de	eventos,	e	
P(x)	um	processo.	É	equivalente	a 
 [] x:A @ x -> P(x) 
Escolha	prefixada	
c?x -> P 
c.e0 -> P[e0/x] 
[ ] 
… 
[ ] 
c.eN -> P[eN/x] 
	
Seja	c	um	canal	do	Mpo	{e0,	…,	eN},	então	
Máquinas de estados e CSP 
•  Todo	processo	em	CSP	corresponde	a	uma	“máquina	
de	estados”	(ou	LTS)	
–  Labelled	TransiMon	Systems	
•  FDR	verifica	processos	com	um	número	finito	de	
estados	
•  A	opção	:graph	é	usada	em	FDR3	para	desenhar	o	
LTS	do	processo	CSP	
LTS	de	STOP	
Ω	
LTS	de	SKIP	
Ω	SKIP	 √	
LTS	de	Prefixo	(a	->	P)	
P	a	
LTS	da	escolha	determinísMca	
P	a	
Q	
b	
Seja	S = (a -> P)[](b -> Q),	então	
S	
Definições parametrizadas 
•  Corresponde	a	uma	família,	possivelmente	infinita,	de	
definições.	
•  O	processo	a	seguir	conta	o	andar	atual	considerando	
eventos	de	subir	e	descer	um	andar.		A	quanMdade	de	
estados	do	processo	a	seguir	é	infinita.	
COUNT(n)= 
 if n==0 then 
 (up -> COUNT(1)) 
 else 
 (up -> COUNT(n+1) 
 [] 
 down -> COUNT(n-1)) 
Definições parametrizadas 
•  Para	que	FDR	possa	analisar	todos	os	estados	,	
precisamos	limitar	o	processo:	
 LCOUNT(L,n) = 
 (n<L & up -> LCOUNT(L,n+1)) 
 [](n>0 & down -> LCOUNT(L,n-1)) 
onde	
 (cond & P) 
corresponde	a	
 if cond then P else STOP 
 
Traces de um processo 
•  É		conjunto	das	possíveis	sequência	de	eventos	de	
um	processo	
•  Exemplo: O conjunto de traces de COUNT(0) 
{<>, <up>, <up,down>, <up,up>, <up, down, up>, 
<up,up,up,up>, <up,up,down,down>, ...} 
Refinamento de Processos 
•  P [T= Q	significa	que	um processo Q		refina	um	
processo	P. Isto	é	verdade	se	
–  Se Q tem os mesmo traces P, ou, 
–  Se Q tem menos traces do que P	
•  Exemplo: Consider P = COUNT(0) 
COUNT(0) [T= STOP 
COUNT(0) [T= up -> down -> STOP 
not (COUNT(0) [T= down -> STOP) 
 
Refinamento de Processos 
•  RUN	é	refinado	por	qualquer	processo	considerando	
o	refinamento	de	traces	
•  Para	qualquer	processo	P		
–  RUN(Events) [T=	P 
 
Leitura e exercícios 
•  Livro: Theory and Practice of Concurrency 
–  Leitura: 
•  Cap 0 
•  Cap 1 até 1.1.4 (external choice) 
–  Exercícios: 
•  Essenciais: 1.1.1, 1.1.2, 1.1.3 
•  Opcionais: 1.1.5, 1.1.4 
•  Livro: Understanding Concurrency 
–  Leitura: 
•  Cap 1 até 1.2.2