Baixe o app para aproveitar ainda mais
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
Compartilhar