O que significa 'simultaneidade verdadeira'?

Frequentemente ouço frases como 'semântica de simultaneidade verdadeira' e 'equivalências de simultaneidade verdadeira' sem nenhuma referência. O que significam esses termos e por que são importantes?

Quais são alguns exemplos de verdadeiras equivalências de simultaneidade e qual é a necessidade delas? Por exemplo, em quais casos eles são mais aplicáveis ​​do que mais equivalências padrão (bisimulação, equivalência de traços, etc.)?

O termo "simultaneidade verdadeira" surge no estudo teórico da computação simultânea e paralela. Está em contraste com a intercalação de simultaneidade. A simultaneidade verdadeira é uma simultaneidade que não pode ser reduzida a intercalação. A simultaneidade é intercalada se, em cada etapa da computação, apenas uma ação de computação atômica (por exemplo, uma troca de mensagens entre remetente e destinatário) puder ocorrer. A simultaneidade é verdadeira se mais de uma ação atômica ocorrer em uma etapa.

A maneira mais simples de distinguir os dois é olhar para a regra da composição paralela. Em uma configuração baseada em intercalação, seria algo parecido com isto:

$$\frac{P \rightarrow P'}{P|Q \rightarrow P'|Q}$$

Esta regra impõe que apenas um processo em uma composição paralela possa executar uma ação atômica. Para simultaneidade verdadeira, uma regra como a seguinte seria mais apropriada.

$$\frac{P \rightarrow P'\quad Q \rightarrow Q'}{P|Q \rightarrow P'|Q'}$$

Essa regra permite que ambos os participantes de uma composição paralela executem ações atômicas.

Por que alguém estaria interessado em concorrência intercalada, quando a teoria de concorrência é realmente o estudo de sistemas que executam etapas de computação em paralelo? A resposta é, e esse é um ótimo insight, que para formas simples de simultaneidade de transmissão de mensagens, a simultaneidade verdadeira e a simultaneidade baseada na intercalação não são contextualmente distinguíveis. Em outras palavras, a simultaneidade intercalada se comporta como uma verdadeira simultaneidade, tanto quanto os observadores podem ver. A intercalação é uma boa decomposição da verdadeira simultaneidade. Como a intercalação é mais fácil de lidar nas provas, as pessoas geralmente estudam apenas a concorrência mais simples baseada na intercalação (por exemplo, CCS e$\pi$-calculi). No entanto, essa simplicidade desaparece para a computação simultânea com formas mais ricas de observação (por exemplo, computação temporizada): a diferença entre simultânea verdadeira e simultânea intercalada se torna observável.

Equivalências padrão como bisimulações e traços têm as mesmas definições para simultaneidade verdadeira e intercalada. Mas eles podem ou não igualar processos diferentes, dependendo do cálculo subjacente.

Deixe-me dar uma explicação informal de por que intercalação e interação verdadeiramente simultânea são indistinguíveis em cálculos de processos simples. A configuração é um cálculo tipo CCS ou . Digamos que temos um programa$\pi$

$$P \quad=\quad \overline{x} \ |\ \overline{y} \ |\ x.y.\overline{a} \ |\ y.\overline{b}$$ Em seguida, temos a seguinte redução verdadeiramente simultânea: Essa etapa de redução pode ser correspondida pelas seguintes etapas intercaladas: A única diferença entre os dois é que o primeiro dá um passo, enquanto o segundo dois. Porém, cálculos simples não podem detectar o número de etapas usadas para alcançar um processo. $$\begin{eqnarray*} P &\rightarrow& y.\overline{a} \ |\ \overline{b} \end{eqnarray*}$$ $$\begin{eqnarray*} P &\rightarrow & \overline{x} \ |\ x.y.\overline{a} \ |\ \overline{b} \\ &\rightarrow & y.\overline{a} \ |\ \overline{b} \end{eqnarray*}$$

Ao mesmo tempo, possui a segunda segunda sequência de redução intercalada: Mas essa também é uma sequência de redução em uma configuração verdadeiramente simultânea, desde que a verdadeira concorrência não seja forçada (por exemplo, execuções intercaladas são permitidas mesmo quando há potencial para mais de uma interação por vez).$P$

$$\begin{eqnarray*} P &\rightarrow & \overline{y} \ |\ y.\overline{a} \ |\ y.\overline{b} \\ &\rightarrow & \overline{a} \ |\ y.\overline{b} \end{eqnarray*}$$

Para dizer a verdade, eu mesmo estava pesquisando uma resposta. Qual é a semântica aqui? Atribuímos um significado "sistema de transição" à descrição "álgebra de processo"; isto é, o significado é o sistema de transição gerado a partir da descrição inicial do sistema usando regras definidas do SOS. Assim, usando a semântica de intercalação, perdemos toda a estrutura concorrente no sistema de transição obtido.

Outra resposta poderia ser que não é "diferença observável", mas a diferença em "observabilidade". Usando uma semântica de intercalação, podemos observar apenas execuções lineares; enquanto, usando a simultaneidade verdadeira, podemos observar "execuções simultâneas" (cf. livro de redes de Petri de W.Reisig'13).

Ainda assim, tenho algumas dúvidas sobre o que disse acima e seria interessante ouvir insights mais profundos. Ou seja, usando relógios vetoriais de Lamport, quanto da teoria da relatividade pode ser transferida para a teoria da concorrência.