Álgebras de Processo
(FSP e CSP)
Joabe Jesus
[email protected]
Conceitos Fundamentais
• Programa concorrente
– 2 ou mais fluxos (processos) executam
simultaneamente para realizar uma tarefa
• Processo
– É um programa seqüencial (lista de comandos
executados em sequencia)
Programas Concorrentes
• Processos comunicam-se através de
– Variáveis compartilhadas
– Passagem de mensagens
• E sincronizam por
– Exclusão mútua
• Seções críticas não devem executar ao mesmo tempo
– Sincronização condicional
• Retarda um processo até uma dada condição ser satisfeita
concurrent processes
We structure complex systems as sets of simpler
activities, each represented as a sequential process.
Processes can overlap or be concurrent, so as to
reflect the concurrency inherent in the physical
world, or to offload time-consuming tasks, or to
manage communications or other devices.
Designing concurrent software can be complex and
error prone. A rigorous engineering approach is
essential.
Concept of a process as a
sequence of actions.
Model processes as finite
state machines.
Program processes as threads
in Java.
processes and threads
Concepts: processes - units of sequential execution.
Models: finite state processes (FSP)
to model processes as sequences of actions.
labelled transition systems (LTS)
to analyse, display and animate behavior.
Practice: Java threads
Modeling Processes
• Models are described using state machines,
known as Labelled Transition Systems LTS.
These are described textually as finite state
processes (FSP) and displayed and analysed by
the LTSA analysis tool
– LTS - graphical form
– FSP - algebraic form
– CSP - algebraic form
Álgebra de Processos
FSP
modeling processes
A process is the execution of a sequential program. It is modeled as a finite state
machine which transits from state to state by executing a sequence of atomic
actions.
on
a light switch LTS
0
1
off
onoffonoffonoff ……….
Can finite state models produce infinite traces?
a sequence of actions or
trace
FSP - action prefix
If x is an action and P a process then (x-> P) describes a
process that initially engages in the action x and then
behaves exactly as described by P.
ONESHOT = (once -> STOP).
(terminating process)
once
0
ONESHOT state machine
1
Convention: actions begin with lowercase letters
PROCESSES begin with uppercase letters
FSP - action prefix & recursion
Repetitive behaviour uses recursion:
SWITCH = OFF,
OFF
= (on -> ON),
ON
= (off-> OFF).
on
0
1
off
Substituting to get a more succinct definition:
SWITCH = OFF,
OFF
= (on ->(off->OFF)).
And again:
SWITCH = (on->off->SWITCH).
animation using LTSA
The LTSA animator can be used to
produce a trace.
Ticked actions are eligible for selection.
In the LTS, the last action is highlighted in
red.
on
0
1
off
FSP - action prefix
FSP model of a traffic light :
TRAFFICLIGHT = (red->orange->green->orange
-> TRAFFICLIGHT).
LTS generated using LTSA:
red
0
Trace:
orange
1
green
2
3
orange
redorangegreenorangeredorangegreen …
Referências
• FSP
– http://www.doc.ic.ac.uk/~jnm/LTSdocumention/FSPnotation.html
• LTSA - http://www.doc.ic.ac.uk/ltsa/
– Applet
• http://www.doc.ic.ac.uk/~jnm/book/ltsa/LTSA_applet.html
– Eclipse Plugin - http://www.doc.ic.ac.uk/ltsa/eclipse/
• Instalação - http://www.doc.ic.ac.uk/ltsa/eclipse/install
– SceneBeans
• http://www-dse.doc.ic.ac.uk/Software/SceneBeans/
• http://www.doc.ic.ac.uk/~jnm/book/
Álgebra de Processos
CSP
CSP
• Notação para modelar sistemas concorrentes
• Alto nível de abstração
– Comunicação via passagem de mensagens
– Vários operadores para compor processos
• Ferramentas para analisar propriedades
automaticamente
– Ex: FDR, PAT
• Possui bibliotecas para Java
– Ex: JCSP
CSP
• A simple programming language designed for
multiprocessor machines
• Its key feature is its reliance on non-buffered
message passing with explicit naming of
source and destination processes
• CSP uses guarded commands to let processes
wait for messages coming from different
sources
The Model
• Each process runs on its own processor
• All communications between concurrent
processes are made through message passing.
• CSP relies on the most primitive message
passing mechanism:
– Non-buffered sends and receives
– Explicit naming of source and destination
processes
ProBE (Animador de CSP)
FDR (Analisador de CSP)
JCSP
• Biblioteca para Java que suporta
(subconjunto) de CSP
• Programação concorrente com passagem de
mensagens
• Possível usar memória compartilhada (mas
desaconselhável)
Notação
CSP
Escolhas
• Em CSP temos vários tipos de operadores de
escolha
– P [] Q (Escolha determinística)
– P |~| Q (Escolha não-determinística)
– if b then P else Q (Escolha condicional)
– b & P (guarda)
Estado de um processo
• Na prática, dificilmente um processo não
precisará da noção de estado
• Por exemplo: controlar a evolução do
conteúdo de uma fila, pilha, etc.
• Em CSP, estado pode ser capturado através de
parâmetros em processos
• P(S) = …
Estado de um processo
• Um processo com parâmetros é semelhante a
uma classe
• Para usar é preciso “criar uma instância”
• Ou seja, atribuir valores iniciais aos
parâmetros
– P(0) ou Q(true)
Tipos usados em estados
• CSP dispõe de alguns tipos simples:
– Básicos: inteiros (Int) e booleanos (Bool)
– Tuplas: (x, y, z)
– Conjuntos: { 1, 2, 3 } ou { x | x <- T }
– Seqüências:  1, 2, 3  ou  x | x <- T 
– Enumerações: datatype T = A | B
– Abreviação: nametype Nat = { x | x <- Int, x >= 0}
Operações sobre tipos
• Cada tipo tem operações disponíveis
– first(x, y) = x
– head( 1, 2, 3 ) = 1
– tail( 1, 2, 3 ) =  2, 3 
– union({0, 1}, {3}) = {0, 1, 3}
– member(0, {0, 1}) = true
– Etc.
Funções
• As vezes é necessário definir funções para
manipular estruturas específicas
• Por exemplo
– first3(x, y, z) = x
– midd3(x, y, z) = y
Note o uso de casamento
De padrões
• Mas antes de criar uma função é sempre bom
ver disponibilidade…
Escolha condicional
• Sejam P e Q dois processos e b uma expressão
booleana. Então
if b then P
else Q
LTS de escolha condicional
Seja S = if b then P else Q, então
b
P
S
b
Q
Escolha condicional: Buffer
channel in, out: {0, 1}
Buffer(s) = if s ==   then
in?x -> Buffer(s^  x )
else ( in?x -> Buffer(s^  x )
[] out!head(s) ->
Buffer(tail(s)) )
Casamento de padrões
• Como CSP é equipada com uma linguagem
funcional, também há suporte a casamento de
padrões em processos
• Buffer( ) seria equivalente a
Buffer(s) = if s ==   then …
Casamento de padrões: Buffer
channel in, out: {0, 1}
Buffer( ) =
in?x -> Buffer(s^  x )
Buffer( h ^t) =
( in?x -> Buffer(s^  x )
[] out!h -> Buffer(t) )
Guarda
• O processo guardado
–b&P
• É equivalente a escolha condicional
– if b then P else STOP
LTS de guarda
Seja S = b & P, então
b
P
S
b

Guarda: Buffer
• channel in, out: {0, 1}
• Buffer(s) = (s ==  ) & in?x -> Buffer(s^  x )
[] (s !=  ) &
( in?x -> Buffer(s^  x )
[] out!head(s) ->
Buffer(tail(s)) )
Exercício
• Modele o atendimento de uma fila de um
caixa de banco
– A fila pode aumentar se chegar cliente
– Pode diminuir se cliente for atendido
– Cliente pode sacar ou depositar qq valor
– A fila do caixa deve iniciar sem qq cliente (vazia)
INTRODUZINDO CONCORRÊNCIA
Paralelismo
• Representam a execução paralela de dois ou mais
processos:
– fluxos de controles independentes
– interações eventuais
• Utilizados para conectar os componentes de um
sistema distribuído:
– sistemas distribuídos a partir de componentes seqüenciais
– sistemas distribuídos a partir de componentes paralelos
Operadores de Paralelismo
• Concorrência pode ser expressa em CSP
através de:
– Composição paralela alfabetizada
• P [ X || Y ] Q
– Composição paralela generalizada
• P [| X |] Q
– Entrelaçamento
• P ||| Q
Entrelaçamento
• Sejam P e Q processos CSP então
P ||| Q
• P e Q são executados em paralelo sem
sincronização (independentes)
• Útil para especificar arquiteturas clienteservidor
– Vários clientes e/ou servidores
Entrelaçamento
• P ||| Q
– Oferece os eventos iniciais tanto de P quanto de
Q, e espera até que haja uma comunicação
– Após a comunicação de um evento a de P (Q),
comporta-se como P’ ||| Q (P ||| Q’)
– Na presença de mesmo evento, P ||| Q evolução
em P ou Q é não-determinística
Processos Paralelos e Seqüenciais
• Sejam P = c?x:A -> P’ e Q = c?x:B -> Q’. Então:
P ||| Q
=
c?x: A  B ->
if (x A  B) then (P’ ||| Q) |~| (P ||| Q’)
else if (x  A) then (P’ ||| Q)
else (P ||| Q’)
Lei Interessante
• Seja P um processo CSP. Então
P ||| STOP = P
• Esta lei decorre imediatamente do slide
anterior (step-law)
– if (x  A) then (P’ ||| Q)
– Onde Q é o processo STOP
• Este fato nos permite modelar tolerância a
falhas
Cuidado
O mesmo ocorre
• Sejam P e Q processos CSP
também com
escolha externa
recursivos. O processo
P = P ||| Q
• É infinito estruturalmente e FDR não consegue
lidar com o mesmo
• Já P = P’ ||| Q pode ser trabalhado sem
problemas
Exercício
• Adapte o modelo de caixas anterior para
considerar 2 caixas
Composição Paralela Generalizada
• Sejam P e Q processos CSP então
P [| X |] Q
• P e Q são executados em paralelo mas
sincronizando nos eventos em X:
– Nos outros eventos semelhante ao operador de
entrelaçamento (independente)
Composição Paralela Generalizada
• Generaliza outros operadores:
– P ||| Q = P [| {} |] Q
– P [ X || Y ] Q =
(P [| Events \ X |] STOP)
[| X  Y |]
(Q [| Events \ Y |] STOP)
• Não pode ser expresso através dos outros
operadores
Composição Paralela Generalizada
• P [| X |] Q
– Com A e B sendo respectivamente os eventos
iniciais de P e Q, tem-se o seguinte conjunto de
eventos:
C =(A \ X) U (B \ X) U (A  B  X)
Processos Paralelos e Sequenciais
Sejam P = c?x:A -> P’ e Q = c?x:B -> Q’. Então
P [| X |] Q
=
c?x:C ->
if (xX) then P’ [|X|] Q’
else if (xAB) then (P’ [|X|] Q) |~| (P [|X|] Q’)
else if (xA) then (P’ [|X|] Q)
else (P [|X|] Q’)
Deadlock
P = (a -> b -> P)
[] (b -> a -> P)
Q = (a -> c -> Q)
[] (c -> a -> Q)
P [|Events|] Q = a -> STOP
Exercício
• Adapte o exercício de caixas anterior para que
um cliente possa trocar de fila
Restringindo Concorrência
• Os operadores de composição paralela podem
ser usados para restringir o comportamento
dos processos:
– P [|X|] STOP comporta-se como P exceto pela
proibição da realização dos eventos em X
– P [|X|] Q, onde Q só realiza os eventos em X,
restringe o comportamento de P
Associatividade
• Sejam P, Q e R processos CSP, X e Y conjuntos
de sincronização. Então
– (P [|X|] Q) [|Y|] R  P [|X|] (Q [|Y|] R)
• Só quando X = Y esta associatividade é válida
– (P [|X|] Q) [|X|] R = P [|X|] (Q [|X|] R)
Multiway rendezvous
• Ocorre quando mais de dois processos
participam de interação em comum
• Do ponto de vista de análise pode ser usado
sem problemas
• No nível de projeto deve ser evitado ou
reescrito
• O modelo CSP que será usado para mapear
em JCSP não deve usar
– JCSP não suporta
Operadores Indexados
• Para P [ X || Y ] Q temos
– || i:{1..N} @ [A(i)] P(i)
• Para P ||| Q temos
– ||| i:{1..N} @ P(i)
• Para P [|X|] Q temos
– [|X|] i:{1..N} @ P(i)
Cliente-Servidor Indexados
• Sejam Ci e Sj processos CSP e X um conjunto
de sincronização entre Ci e Sj. Então uma
arquitetura cliente-servidor pode ser vista
genericamente como
(|||i=1..N Ci) [|X|] (|||j=1..K Sj)
Referências
• Roscoe, A.W. The Theory and Practice of
Concurrency. Prentice-Hall, 1998.
• Hoare, C.A.R. Communicating Sequential
Processes. Prentice-Hall, 1985.
• http://www.usingcsp.com/
Referências
• CSP
– http://www.cin.ufpe.br/~if711/aulas/Aula%2002.
pdf
– Courses
• http://www.cin.ufpe.br/~if711/
• http://www.softeng.ox.ac.uk/subjects/CDS.html
• http://www.softeng.ox.ac.uk/subjects/ACT.html
• FDR – Failures Divergences Refinement
– http://www.fsel.com