Formalismos para Formalismos para ConcorrênciaConcorrência

PorPor

Paulo MacielPaulo MacielCentro de InformáticaCentro de Informática

Universidade Federal de Universidade Federal de PernambucoPernambuco

ObjetivoObjetivo

Apresentar alguns formalismos para Apresentar alguns formalismos para a modelagem de sistemas a modelagem de sistemas concorrentes.concorrentes.

Descrever as principais Descrever as principais características destes modelos.características destes modelos.

Modelagem de Problemas.Modelagem de Problemas. Ressaltar as pontencialidades Ressaltar as pontencialidades

destes modelos.destes modelos.

Apresentacão Apresentacão Máquinas de Estados FinitosMáquinas de Estados Finitos (Finite State Machines)(Finite State Machines) LTS – Sistema de Transição RotuladoLTS – Sistema de Transição Rotulado

(Labeled Transitions Systems)(Labeled Transitions Systems) CSP – CSP – Communicating Sequential ProcessCommunicating Sequential Process

Estruturas TracesEstruturas Traces

Redes de PetriRedes de Petri

Máquinas de Estados Máquinas de Estados FinitosFinitos

(Finite State Machines)(Finite State Machines)

Finite State MachineFinite State MachineModelo MealyModelo Mealy

FSM= (S,I,O,f,h)FSM= (S,I,O,f,h)

– S – Conjunto de EstadosS – Conjunto de Estados

– ss00 S– Estado inicial S– Estado inicial

– I – Alfabeto de entradaI – Alfabeto de entrada– O – Alfabeto de saídaO – Alfabeto de saída– f : S f : S I I S – Função de próximo estado S – Função de próximo estado– h: S h: S I I O – Função de saída O – Função de saída

a

I={a1,a2,a3} O={d2,d1,p,s1,s2}

ANDAR DESEJADODIREÇÃO E NÚMERO

DE ANDARES

Máquinas de Estados Máquinas de Estados FinitosFinitos

Modelo MealyModelo Mealy

Ea1

a2

a3

Edfícil

I={a1,a2,a3}

O={d2,d1,p,s1,s2}

ANDAR DESEJADO

a2/s1

a1/d1

a3/s1

a2/d1a1/d2

a3/s2

a1/p a2/p

a3/p

S1 S2

S3 DIREÇÃO E NÚMERO

DE ANDARES

Máquinas de Estados Máquinas de Estados FinitosFinitos

Modelo MealyModelo Mealy

Máquinas de Estados Máquinas de Estados Finitos Finitos

Modelo MooreModelo Moore

FSM= (S,I,O,f,h)FSM= (S,I,O,f,h)

– S – Conjunto de EstadosS – Conjunto de Estados

– ss00 S– Estado inicial S– Estado inicial

– I – Alfabeto de entradaI – Alfabeto de entrada– O – Alfabeto de saídaO – Alfabeto de saída– f : S f : S I I S – Função de próximo estado S – Função de próximo estado– h: S h: S O – Função de saída O – Função de saída

a3S11 /d2

S12 /d1

S13 /p

S21 /d1 S31 /p

S32 /s1S22 /p

S23 /s1 S33 /s2

a1

a1

a1

a1

a2a2

a3

a3

a3a2a3a2

a2a1

a3a3

a3

a1 a2

a2a1

a1

a2

a2

a1

a3

Máquinas de Estados Máquinas de Estados FinitosFinitos

Modelo MooreModelo Moore

Máquinas de Estados Máquinas de Estados FinitosFinitos

– Impossibilidade da modelagem direta da Impossibilidade da modelagem direta da concorrência.concorrência.

Criação de processosCriação de processos sincronizaçãosincronização a

Sistema de Transição Sistema de Transição RotuladoRotulado

(Labeled Transition System)(Labeled Transition System)

Sistema de Transição Sistema de Transição RotuladoRotulado

TS = (S,sTS = (S,s00,L,tran),L,tran)

– S – Conjunto de EstadosS – Conjunto de Estados

– ss00 – Estado inicial – Estado inicial

– L – Conjunto de rótulosL – Conjunto de rótulos– tran tran S S L L S, normalmente indicada por s S, normalmente indicada por s

s’ s’

a

Sistema de Transição Sistema de Transição RotuladoRotulado

Sejam dois processos concorrentes A e BSejam dois processos concorrentes A e B Processo A{Processo A{ Processo B {Processo B {

Enquanto C=T {Enquanto C=T { e4e4

e1e1 e5e5

e2e2 }}

}}

e3e3

e5e5

}}

Sistema de Transição Sistema de Transição RotuladoRotulado

Se A e B são dois processos, entãoSe A e B são dois processos, então (A||B) representa a execução concorrente de A e B.

Processo A =Processo A = Processo B =Processo B =

(e1 (e1 -> e2 e2 -> Process A) Process A) (e4 (e4 -> e5 e5 - Process B)Process B)

Process C = ((Process A || Process B) Process C = ((Process A || Process B) -> Process C )Process C )

Sistema de Transição Sistema de Transição RotuladoRotulado

e3

e1

e2

e4

e1

e2e4

e3 e4

e5

s0

s5s1

s4s3

s6

s7

Composição Paralela Composição Paralela InterleavingInterleaving de Ações de Ações

thinktalkscratchthinkscratchtalkscratchthinktalk

Possible traces as a result of action interleaving.

Se P e Q são dois processos, então (P||Q) representa a execução concorrente de P e Q. O operador || é o operador de composição paralela.ITCH = (scratch->STOP).CONVERSE = (think->talk->STOP).

||CONVERSE_ITCH = (ITCH || CONVERSE).

Composição Paralela Composição Paralela InterleavingInterleaving de Ações de Ações

(0,0)

(0,1)

(0,2)

(1,2)

(1,1)

(1,0)

de CONVERSEde ITCH

3 estados

2 x 3 estados

CONVERSEthink talk

0 1 2

CONVERSE_ITCH

scratch

think

scratch

talk scratch

talk think

0 1 2 3 4 5

2 estados

ITCH

scratch

0 1

Modelando Interações Modelando Interações Ações CompartilhadasAções Compartilhadas

MAKER = (make->ready->MAKER).USER = (ready->use->USER).

||MAKER_USER = (MAKER || USER).

MAKER sincroniza-se com USER quando ready.

Se processoes em uma composição têm ações em comum, estas ações são ditas compartilhadas.

Ações compartilhadas modelam as interações entre processos.

Enquanto ações não compartilhadas podem ser arbitrariamente interleaved , ações compartilhadas devem ser executadas ao mesmo tempo por todos os processos.

MAKERv2 = (make->ready->used->MAKERv2).USERv2 = (ready->use->used ->USERv2).

||MAKER_USERv2 = (MAKERv2 || USERv2).

Modelando Interações Modelando Interações Ações CompartilhadasAções Compartilhadas

Interação restringe o comportamento global

3 estados3 estados

3 x 3 estados?

4 estados

make ready use

used

0 1 2 3

Modelando InteraçõesModelando InteraçõesMúltiplos ProcessosMúltiplos Processos

MAKE_A = (makeA->ready->used->MAKE_A).MAKE_B = (makeB->ready->used->MAKE_B).ASSEMBLE = (ready->assemble->used->ASSEMBLE).

||FACTORY = (MAKE_A || MAKE_B || ASSEMBLE).makeA

makeB makeA ready assemble

used

makeB

0 1 2 3 4 5

modeling interaction - modeling interaction - multiple processesmultiple processes

MAKE_A = (makeA->ready->used->MAKE_A).MAKE_B = (makeB->ready->used->MAKE_B).ASSEMBLE = (ready->assemble->used->ASSEMBLE).

||FACTORY = (MAKE_A || MAKE_B || ASSEMBLE).

Multi-party synchronization:

makeA

makeB makeA ready assemble

used

makeB

0 1 2 3 4 5

CSPCSPCommunicating Sequential ProcessCommunicating Sequential Process

CSPCSP

É uma linguagem para a É uma linguagem para a especificação de sistemas especificação de sistemas concorrentes.concorrentes.

Proposta por C. A. Hoare no Proposta por C. A. Hoare no começo dos anos 80.começo dos anos 80.

CSPCSP

AlfabetoAlfabeto

(P) = {a(P) = {a0,…. 0,…. aamm}}

é o conjunto de eventos é o conjunto de eventos de Pde P

P::=P::=

STOP STOP SKIPSKIP

aaP P P | Q P | Q P[]Q P[]Q P ||P ||AA Q Q P[b/a] P[b/a] P[\ P[\

b]b]

CSPCSP

STOP – um processo que não faz STOP – um processo que não faz nada é escrito como STOP.nada é escrito como STOP.

VendingMachine = STOPVendingMachine = STOP

CSPCSP

Ação Prefixo - aAção Prefixo - aP P

VMVM11=moeda =moeda STOP STOP

VMVM22=moeda =moeda chocolate chocolate STOP STOP