¿Qué significa 'verdadera concurrencia'?

A menudo escucho frases como 'semántica de concurrencia verdadera' y 'equivalencias de concurrencia verdadera' sin ninguna referencia. ¿Qué significan esos términos y por qué son importantes?

¿Cuáles son algunos ejemplos de equivalencias verdaderas de concurrencia y cuál es la necesidad de ellas? Por ejemplo, ¿en qué casos son más aplicables que las equivalencias más estándar (bisimulación, equivalencia de trazas, etc.)?

El término "verdadera concurrencia" surge en el estudio teórico de la computación concurrente y paralela. Está en contraste con la simultaneidad entrelazada. La verdadera concurrencia es la concurrencia que no puede reducirse a intercalación. La simultaneidad se intercala si en cada paso de la computación, solo puede tener lugar una acción de computación atómica (por ejemplo, un intercambio de mensajes entre el emisor y el receptor). La concurrencia es cierta si se produce más de una acción atómica en un paso.

La forma más sencilla de distinguir ambos es mirar la regla para la composición paralela. En una configuración basada en entrelazado, se vería así:

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

Esta regla exige que solo un proceso en una composición paralela pueda ejecutar una acción atómica. Para una verdadera concurrencia, una regla como la siguiente sería más apropiada.

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

Esta regla permite a ambos participantes en una composición paralela ejecutar acciones atómicas.

¿Por qué estaría interesado en la concurrencia intercalada, cuando la teoría de la concurrencia es realmente el estudio de sistemas que ejecutan pasos de cálculo en paralelo? La respuesta es, y esa es una gran idea, que para las formas simples de concurrencia de mensajes, la concurrencia verdadera y la concurrencia basada en intercalación no son distinguibles contextualmente. En otras palabras, la concurrencia intercalada se comporta como la verdadera concurrencia hasta donde los observadores pueden ver. El intercalado es una buena descomposición de la verdadera concurrencia. Dado que el entrelazado es más fácil de manejar en las pruebas, las personas a menudo solo estudian la concurrencia basada en el entrelazado más simple (por ejemplo, CCS y$\pi$-cálculos). Sin embargo, esta simplicidad desaparece para el cómputo concurrente con formas más ricas de observación (por ejemplo, cómputo temporizado): la diferencia entre la concurrencia verdadera y la concurrencia intercalada se vuelve observable.

Las equivalencias estándar, como las bisimulaciones y las trazas, tienen las mismas definiciones de concurrencia verdadera e intercalada. Pero pueden o no equiparar diferentes procesos, dependiendo del cálculo subyacente.

Permítanme dar una explicación informal de por qué el entrelazado y la interacción verdaderamente concurrente son indistinguibles en los cálculos de procesos simples. La configuración es un cálculo CCS o . Digamos que tenemos un programa$\pi$

$$P \quad=\quad \overline{x} \ |\ \overline{y} \ |\ x.y.\overline{a} \ |\ y.\overline{b}$$ Luego tenemos la siguiente reducción verdaderamente concurrente: Este paso de reducción puede coincidir con los siguientes pasos intercalados: La única diferencia entre ambos es que el primero da un paso, mientras que los dos últimos. Pero los cálculos simples no pueden detectar la cantidad de pasos utilizados para alcanzar un proceso. $$\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*}$$

Al mismo tiempo, tiene la siguiente segunda secuencia de reducción intercalada: Pero esta también es una secuencia de reducción en un entorno verdaderamente concurrente, siempre que la verdadera concurrencia no sea forzada (es decir se permiten ejecuciones intercaladas incluso cuando existe la posibilidad de más de una interacción a la vez).$P$

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

A decir verdad, estaba buscando una respuesta en Google. ¿Cuál es la semántica aquí? Asignamos un significado "sistema de transición" a la descripción "álgebra de procesos"; es decir, el significado es el sistema de transición que se genera a partir de la descripción inicial del sistema utilizando reglas SOS definidas. Por lo tanto, usando semántica de entrelazado, perdemos toda la estructura concurrente en el sistema de transición obtenido.

Otra respuesta podría ser que no es "diferencia observable" sino la diferencia en "observabilidad". Usando una semántica entrelazada, podemos observar solo corridas lineales; mientras que, utilizando la verdadera concurrencia, podemos observar "ejecuciones concurrentes" (cf W.Reisig'13 Petri nets book).

Aún así, tengo algunas dudas sobre lo que dije anteriormente, y sería interesante escuchar ideas más profundas. Es decir, usando los relojes vectoriales Lamport, cuánto de la teoría de la relatividad se puede transferir a la teoría de la concurrencia.