Modelos de Concorrência e Cálculos de Processos

Modelos de concorrência e cálculos de processos fornecem descrições formais de como processos independentes são executados, comunicam-se e sincronizam-se.

Definition

Um cálculo de processos é uma álgebra formal para descrever sistemas concorrentes como processos comunicantes, com operadores para composição paralela, comunicação e escolha, e equivalências que determinam quando dois processos se comportam da mesma forma.

Scope

Este tópico abrange modelos algébricos de computação concorrente: CSP de Hoare e CCS de Milner, o pi-cálculo para processos móveis cuja topologia de comunicação muda, e o modelo de ator de passagem de mensagens assíncronas. Aborda primitivas de comunicação e sincronização, equivalências comportamentais como bisimulação, e o contraste entre concorrência de memória compartilhada e passagem de mensagens.

Core questions

• Como processos comunicantes concorrentes podem ser descritos algebricamente?
• Quando dois processos concorrentes são comportamentalmente equivalentes?
• Como a passagem de mensagens se compara à concorrência de memória compartilhada?
• Como as estruturas de comunicação dinâmicas são modeladas, como no pi-cálculo?

Key theories

Processos Sequenciais Comunicantes (CSP)

O CSP de Hoare modela a concorrência através de processos que se sincronizam em eventos de comunicação compartilhados, fornecendo uma base para linguagens de passagem de mensagens e uma teoria de refinamento de processos.

CCS e bisimulação

O Cálculo de Sistemas Comunicantes de Milner (CCS) oferece uma álgebra de processos com uma noção precisa de equivalência comportamental, a bisimulação, para raciocinar sobre quando os processos são intercambiáveis.

O pi-cálculo

Milner, Parrow e Walker estenderam os cálculos de processos para a mobilidade, permitindo que os próprios canais de comunicação fossem passados como mensagens, de modo que a estrutura de conexão evolui dinamicamente.

Clinical relevance

Os cálculos de processos e o modelo de ator sustentam o design de linguagens e frameworks concorrentes e distribuídos construídos sobre passagem de mensagens, e fornecem ferramentas formais para especificar e verificar protocolos. A bisimulação e o refinamento oferecem critérios precisos para o comportamento concorrente correto.

History

A teoria da concorrência amadureceu no final da década de 1970 com o CSP de Hoare e o CCS de Milner, enquanto o modelo de ator de Hewitt (1973) ofereceu uma alternativa assíncrona de passagem de mensagens. O pi-cálculo em 1992 capturou a mobilidade de processos. Esses cálculos influenciaram linguagens de passagem de mensagens e bibliotecas de concorrência e permanecem como fundamentos para a verificação de protocolos.

Debates

Memória compartilhada versus passagem de mensagens

Uma questão fundamental de design é se a concorrência deve ser organizada em torno de estado mutável compartilhado com sincronização ou em torno de processos isolados que trocam mensagens, com os cálculos de processos e o modelo de ator defendendo este último.

Key figures

• C. A. R. Hoare
• Robin Milner
• Carl Hewitt
• Joachim Parrow
• David Walker

Seminal works

• hoare1978
• milner1989
• milner1992
• hewitt1973

Frequently asked questions

O que é bisimulação?

Bisimulação é uma equivalência em processos que se mantém quando cada um pode corresponder aos passos observáveis do outro indefinidamente, formalizando a ideia de que dois processos concorrentes exibem o mesmo comportamento.

O que o pi-cálculo adiciona em relação aos cálculos anteriores?

O pi-cálculo modela a mobilidade permitindo que os canais de comunicação sejam enviados como mensagens, de modo que a topologia de quem pode se comunicar com quem pode mudar durante a execução, capturando sistemas dinâmicos e reconfiguráveis.