Distributive Laws for Parallel Composition in Rely-Guarantee Concurrency

Resumen Técnico: Leyes Distributivas para la Composición en Paralelo en la Concurrencia de Rely-Guarantee

Planteamiento del Problema
El enfoque de rely/guarantee es un método establecido para el razonamiento sobre la corrección de programas concurrentes de memoria compartida mediante la descomposición de los supuestos de interferencia (rely) y los compromisos (guarantee) en propiedades composicionales. Si bien las leyes distributivas son fundamentales para la manipulación algebraica de programas en las matemáticas y la lógica de Hoare, su aplicación a programas concurrentes dentro de un marco de rely/guarantee es compleja. Específicamente, existe la necesidad de una teoría algebraica rigurosa para determinar cuándo y cómo las condiciones de guarantee y rely se distribuyen sobre la composición en paralelo. Trabajos previos establecieron leyes distributivas para la composición secuencial y la iteración, pero extender estas leyes a la composición en paralelo ($c_1 \parallel c_2$) presenta desafíos. Notablemente, mientras que las condiciones de guarantee se distribuyen sobre la composición en paralelo, las condiciones de rely generalmente no lo hacen, debido a los diferentes alcances de los supuestos de interferencia (entorno global frente a interacciones específicas entre hilos). El artículo aborda la brecha en el desarrollo de un marco algebraico unificado para derivar leyes distributivas precisas para la composición en paralelo que involucre comandos de rely y guarantee.

Metodología
Los autores desarrollan una teoría basada en un Álgebra de Refinamiento Concurrente (CRA), estructurada utilizando cuantales débiles y bi-cuantales débiles aumentados con tests y comandos atómicos. La metodología procede en tres etapas:

1. Fundamento Algebraico Abstracto: La teoría se desarrolla primero en un "álgebra atómica sincrónica" altamente abstracta. Los comandos se modelan como elementos de un retículo distributivo completo con operaciones para la composición secuencial ($;$), la composición en paralelo ($\parallel$) y la conjunción débil ($\sqcap$). El marco distingue entre comandos atómicos (transiciones indivisibles) y comandos pseudo-atómicos (comandos que pueden abortar, representados como $a \lor b; \top$).
2. Derivación de Leyes Distributivas Generales: Los autores investigan las condiciones bajo las cuales una iteración de un comando atómico, $a^\omega$, se distribuye sobre la composición en paralelo. Demuestran que la igualdad $a^\omega \sqcap (c_1 \parallel c_2) = (a^\omega \sqcap c_1) \parallel (a^\omega \sqcap c_2)$ se cumple si y solo si el comando atómico es idempotente con respecto a la composición en paralelo ($a = a \parallel a$). Esta prueba utiliza:
   • Aproximaciones finitas: Analizando comandos hasta una longitud finita $i$.
   • Cierre de límite: Probando que las iteraciones infinitas de comandos atómicos son cerradas al límite (iguales al ínfimo de sus aproximaciones finitas).
   • Super-compactación: Asumiendo que el retículo de comandos es "super-algebraico", lo que permite que comandos arbitrarios se descompongan en elecciones de comandos super-compactos (deterministas, no abortantes).
3. Aplicación a Rely/Guarantee: Los resultados abstractos se instancian en un álgebra de Aczel, donde los comandos se definen mediante transiciones de programa ($\pi$) y transiciones de entorno ($\epsilon$).
   • Los comandos de guarantee ($\text{guar}_\pi g$) se definen como la iteración infinita de $(\pi g \lor \epsilon \text{univ})$.
   • Los comandos de rely ($\text{rely } r$) se definen como la iteración infinita de $(\pi \text{univ} \lor \epsilon r \lor \epsilon \bar{r}; \top)$.
   • Los autores analizan la condición $a = a \parallel a$ para estas formas específicas de comando para determinar su validez.

Contribuciones Clave y Resultados

• Ley Distributiva General para Iteraciones Atómicas: El artículo establece que para un comando atómico $a$, la ley distributiva $a^\omega \sqcap (c_1 \parallel c_2) = (a^\omega \sqcap c_1) \parallel (a^\omega \sqcap c_2)$ se cumple si y solo si $a = a \parallel a$.
• Validez de la Distribución de Guarantee: Al demostrar que el comando base para un guarantee, $\pi g \lor \epsilon \text{univ}$, satisface la condición de idempotencia (ya que $g \subseteq \text{univ}$), los autores prueban la igualdad:
  $$\text{guar}_\pi g \sqcap (c_1 \parallel c_2) = (\text{guar}_\pi g \sqcap c_1) \parallel (\text{guar}_\pi g \sqcap c_2)$$
  Esto confirma que las condiciones de guarantee pueden distribuirse sobre la composición en paralelo.
• Invalidación de la Distribución Pura de Rely: Los autores demuestran que el comando base para un rely, $\pi \text{univ} \lor \epsilon r \lor \epsilon \bar{r}; \top$, no satisface la condición de idempotencia (a menos que $r$ sea universal). En consecuencia, la ley distributiva general de los relies sobre la composición en paralelo no se cumple:
  $$\text{rely } r \sqcap (c_1 \parallel c_2) \neq (\text{rely } r \sqcap c_1) \parallel (\text{rely } r \sqcap c_2)$$
  Esto se atribuye al hecho de que un rely a la izquierda asume la interferencia de todo el entorno, mientras que los relies a la derecha solo consideran la interferencia del otro hilo en el par.
• Distribución Compuesta (Invariante de Evolución): El artículo deriva una igualdad más fuerte para comandos compuestos donde se combinan un rely y un guarantee, específicamente el comando de "invariante de evolución" ($\text{evolve } r \equiv \text{rely } r \sqcap \text{guar}_\pi r$). Si $g \subseteq r$, la siguiente igualdad se cumple:
  $$\text{rely } r \sqcap \text{guar}_\pi g \sqcap (c_1 \parallel c_2) = (\text{rely } r \sqcap \text{guar}_\pi g \sqcap c_1) \parallel (\text{rely } r \sqmp \text{guar}_\pi g \sqcap c_2)$$
  Esto es válido porque la condición de guarantee asegura que la condición de rely se cumpla a través de la composición en paralelo.
• Comandos Pseudo-Atómicos: La teoría se extiende para manejar comandos pseudo-atómicos (comandos que pueden abortar), mostrando que propiedades distributivas similares se mantienen bajo condiciones específicas respecto a los componentes que abortan.

Significancia y Reivindicaciones
El artículo afirma proporcionar la primera derivación algebraica de las leyes distributivas para la composición en paralelo específicamente adaptadas a la concurrencia de rely/guarantee. Al formalizar la teoría en Isabelle/HOL, los autores aseguran la corrección de los lemas y las pruebas presentadas.

La significancia radica en permitir un desarrollo algebraico paso a paso de programas concurrentes. La capacidad de distribuir condiciones de guarantee sobre la composición en paralelo permite a los desarrolladores razonar sobre sistemas concurrentes complejos descomponiéndolos en componentes con garantías locales, lo que simplifica la verificación. El artículo señala explícitamente que, si bien las leyes más generales son refinamientos (unidireccionales), restringir la forma del comando (por ejemplo, usando guarantees o combinaciones específicas de rely/guarantee) produce leyes de igualdad más fuertes. Este trabajo cierra la brecha entre las estructuras algebraicas abstractas (cuantales) y el razonamiento práctico de concurrencia (rely/guarantee), ofreciendo una base rigurosa para manipular especificaciones concurrentes. Los autores no pretenden resolver todos los problemas de verificación de concurrencia, sino proporcionar herramientas algebraicas esenciales para el dominio específico del razonamiento de rely/guarantee.