» Ricardo Rosenfeld
Centro de Altos Estudios en Tecnología Informática (CAETI).
Universidad Abierta Interamericana (UAI)
Resumen
Este artículo completa nuestra serie de cuatro artículos sobre la verificación axiomática de programas, que planteamos en el marco del proyecto del CAETI para construir un ambiente de soporte al desarrollo de software. En particular, concluimos el análisis de los programas concurrentes iniciado en la publicación anterior, considerando ahora la familia de los programas distribuidos, caracterizados por contar con procesos con variables disjuntas y que se comunican mediante mensajes. Como siempre, destacamos el principio de utilizar las axiomáticas como guías para la obtención de programas correctos por construcción, y la observación de que las nociones fundamentales de predicado invariante y función variante constituyen la base metodológica en todos los paradigmas de programación.
PALABRAS CLAVE: PROGRAMA DISTRIBUIDO, VERIFICACIÓN, AXIOMÁTICA.
Verification of Distributed Programs
Abstract
This article completes our series of four articles on the axiomatic verification of programas, which we propose within the framework of the CAETI project to build an environment to support software development. In particular, we conclude the analysis of concurrent programs begun in the previous publication, now considering the family of distributed programs, characterized by having processes with disjoint variables and that communicate through messages. As always, we highlight the principle of using axiomatics as guides for obtaining correct programs by construction, and the observation that the fundamental notions of invariant predicate and variant function constitute the methodological basis in all programming paradigms.
KEYWORDS: DISTRIBUTED PROGRAM, VERIFICATION, AXIOMATICS.
Introducción
Con este artículo completamos nuestra serie de cuatro artículos sobre la verificación axiomática de programas, desarrollada en el marco del proyecto del CAETI para la construcción de un ambiente que asiste en el desarrollo de software. En particular, completamos el análisis de los programas concurrentes. En la publicación anterior consideramos la familia de los programas paralelos, así que en este último trabajo nos enfocamos en la verificación axiomática de los programas distribuidos, con procesos con variables disjuntas y que se comunican mediante mensajes Las axiomáticas que presentamos se basan en los trabajos de K. Apt, N. Francez y W. de Roever de 1980 [AFdR80], adaptación, también no composicional, de las axiomáticas para programas paralelos de S. Owicki y D. Gries [OG76a, OG76b].
Primero introducimos los programas con los que trabajamos y las propiedades a verificar, luego presentamos las axiomáticas correspondientes junto a ejemplos de aplicación, y finalmente concluimos con un par de notas adicionales (una de ellas sobre alternativas axiomáticas composicionales para la concurrencia, en contraste con las que venimos describiendo) y observaciones finales. Recomendamos al lector leer o releer los artículos anteriores, [Ros22a, Ros22b, Ros23], especialmente el último.
Lenguaje de pasajes de mensajes
El lenguaje de programación que utilizamos es una extensión concurrente del lenguaje de programación secuencial no determinístico considerado en el segundo artículo de la serie [Ros22b]. Se basa en el lenguaje CSP o Communicating Sequential Processes (Comunicación de Procesos Secuenciales o Procesos Secuenciales Comunicantes), creado por C. Hoare [Hoa78]. Los procesos no comparten variables, y se comunican y sincronizan por medio de pasajes de mensajes, generados por instrucciones de entrada/salida, también conocidas como instrucciones de comunicación.
Consideramos comunicaciones sincrónicas, esquema según el cual el envío de un mensaje por parte de un proceso y la recepción del mensaje por parte de otro se ejecutan atómicamente (un proceso puede quedar bloqueado a la espera de la comunicación con el otro, lo que puede producir una situación de deadlock). En una de las notas adicionales hacemos una breve referencia al modelo asincrónico.
Los programas tienen la siguiente forma:
S :: [P1 :: S1 || … || Pn :: Sn]
que se abrevia con [ || i = 1,n Pi ]. Es decir, los programas son directamente composiciones distribuidas de procesos. Los procesos siempre se etiquetan, para identificarlos en los pasajes de mensajes. No hay anidamiento de concurrencia ni procesos dinámicos. Además del skip, la asignación, la secuencia y la composición concurrente, en este caso distribuida, que conocemos de los lenguajes utilizados previamente, el repertorio de instrucciones del lenguaje incluye otras cuatro instrucciones, que pasamos a describir. Comenzamos con las instrucciones de entrada/salida:
Instrucción de entrada. Su sintaxis es:
Pi ? x
En un proceso Pj, con j ≠ i, que tiene una variable local x, la instrucción efectúa un pedido al proceso Pi para que asigne un valor a x.
Instrucción de salida. Su sintaxis es:
Pj ! e
En un proceso Pi, con i ≠ j, la instrucción efectúa un pedido al proceso Pj para que reciba el valor de la expresión e, definida con variables locales de Pi.
Pi ? x (en Pj) y Pj ! e (en Pi) progresan simultáneamente. Un proceso debe esperar al otro para que se produzca la comunicación entre ellos, cuyo efecto es la asignación del valor de e a x. También se pueden comunicar tuplas de valores.
Se define que Pi ? x (en Pj) y Pj ! e (en Pi) coinciden sintácticamente, si además de la coincidencia de los índices coinciden los tipos de datos de x y e. Se utiliza el símbolo α para denotar una instrucción de entrada/salida, y (α, α´) para denotar instrucciones de entrada/salida que coinciden sintácticamente. La comunicación (α, α´) está habilitada cuando α y α´ son las siguientes instrucciones a ser ejecutadas por los procesos respectivos y los mismos están preparados o listos para ejecutarlas.
Las instrucciones de entrada/salida pueden aparecer aisladamente en un proceso o bien ser parte de selecciones condicionales y repeticiones con comunicaciones, las dos instrucciones del lenguaje que nos quedan por describir:
Selección condicional con comunicaciones. Su sintaxis más general es:
if B1 ; α1 S1 or … or Bn ; αn Sn fi
siendo B1, …, Bn expresiones booleanas y α1, …, αn instrucciones de entrada/salida, estas últimas opcionales. Es decir, la selección tiene la misma forma que la del lenguaje secuencial de comandos guardados que vimos antes, pero ahora una guardia puede incluir una instrucción de entrada/salida, en cuyo caso un comando guardado Bi ; αi Si puede ejecutarse (o lo que es lo mismo, la dirección i está habilitada) si Bi es verdadera y αi es parte de una comunicación habilitada. La evaluación de las guardias es atómica. Por lo tanto, una selección condicional con comunicaciones se comporta de la siguiente manera: si tiene direcciones habilitadas, puede progresar no determinísticamente por alguna de ellas y pasar a la siguiente instrucción si el componente Si respectivo termina; y si no tiene direcciones habilitadas, si es porque todas las Bi son falsas la selección falla, y si no, queda bloqueada, temporaria o definitivamente, de acuerdo a lo que suceda en el programa más adelante.
Repetición con comunicaciones. Su sintaxis más general es:
do B1 ; α1 S1 or … or Bn ; αn Sn od
Valen las mismas definiciones del item anterior, y mantenemos la restricción del lenguaje secuencial no determinístico de comandos guardados, para simplificar la presentación, de no permitir repeticiones anidadas. Por lo tanto, una repetición con comunicaciones se comporta de la siguiente manera: si tiene direcciones habilitadas, puede progresar no determinísticamente por alguna de ellas y repetir el mismo ciclo mientras existan; si en algún momento ninguna dirección está habilitada, si es porque todas las Bi son falsas la repetición termina, y si no, queda bloqueada, temporaria o definitivamente, según lo que ocurra después en el programa; y si siempre existe una dirección habilitada, la repetición diverge.
Al igual que los programas paralelos, los programas distribuidos terminan, fallan (por causa de una selección condicional sin ninguna Bi verdadera o por deadlock) o divergen. La ejecución de una composición distribuida consiste en el interleaving de las instrucciones atómicas de los distintos procesos que la constituyen (instrucciones skip, asignaciones y comunicaciones), en base a la propiedad de progreso fundamental, que sólo asegura que algún proceso avance si puede (luego nos referimos al fairness). La novedad semántica en los programas distribuidos es la ejecución conjunta de una instrucción de entrada y una instrucción de salida, y así el avance en dos procesos simultáneamente. Otro aspecto distintivo relacionado con las instrucciones de comunicación es la manifestación de dos tipos de no determinismo, uno local, proveniente del lenguaje secuencial no determinístico de comandos guardados, y el otro global, propio de la semántica de interleaving, que ejemplificamos a continuación. Los procesos:
P1 :: if P3 ? x skip or P3 ! 0 skip fi P2 :: if true P3 ? x or true P3 ! 0 fi
implementan de dos maneras distintas las alternativas de recibir un valor del proceso P3 o enviarle el valor 0. Que P1 ejecute P3 ? x o P3 ! 0 depende de la situación global del programa. En cambio, en P2 la elección entre una u otra instrucción de entrada/salida es local. Esta diferencia es irrelevante en términos de la correctitud parcial, pero crucial con respecto a la ausencia de deadlock. Por ejemplo, si el proceso P3 envía el valor 1, mientras que el programa:
[P1 :: if P3 ? x skip or P3 ! 0 skip fi || P3 :: P1 ! 1] termina con x = 1, en el programa:
[P2 :: if true P3 ? x or true P3 ! 0 fi || P3 :: P2 ! 1]
se puede producir una situación de deadlock si el proceso P2 elige la segunda dirección.
Completamos la descripción del lenguaje de pasajes de mensajes con otros dos ejemplos de programas. El primero consiste en la propagación de un valor desde un proceso P1 hasta un proceso Pn:
Sprop :: [P1 || … || Pi || … || Pn], con:
P1 :: P2 ! y1
…..
Pi :: Pi – 1 ? yi ; Pi + 1 ! yi
…..
Pn :: Pn – 1 ? yn
que no requiere mayores explicaciones. El último ejemplo es un programa que obtiene el mínimo de un conjunto de valores:
Smin :: [P1 || … || Pi || … || Pn || Q], con:
Pi :: (mi_mini , mi_tamañoi) := (ai , 1) ;
do 0 mi_tamañoi n ; P1 ! (mi_mini , mi_tamañoi) mi_tamañoi := 0
………
or 0 mi_tamañoi n ; Pi – 1 ! (mi_mini , mi_tamañoi) mi_tamañoi := 0 or 0 mi_tamañoi n ; Pi + 1 ! (mi_mini , mi_tamañoi) mi_tamañoi := 0
………
or 0 mi_tamañoi n ; Pn ! (mi_mini , mi_tamañoi) mi_tamañoi := 0 or 0 mi_tamañoi n ; P1 ? (su_mini , su_tamañoi)
(mi_mini , mi_tamañoi) := (min(mi_mini , su_mini), mi_tamañoi + su_tamañoi)
………
or 0 mi_tamañoi n ; Pi – 1 ? (su_mini , su_tamañoi)
(mi_mini , mi_tamañoi) := (min(mi_mini , su_mini), mi_tamañoi + su_tamañoi) or 0 mi_tamañoi n ; Pi + 1 ? (su_mini , su_tamañoi)
(mi_mini , mi_tamañoi ) := (min(mi_mini , su_mini), mi_tamañoi + su_tamañoi)
………
or 0 mi_tamañoi n ; Pn ? (su_mini , su_tamañoi)
(mi_mini , mi_tamañoi) := (min(mi_mini , su_mini), mi_tamañoi + su_tamañoi) od ;
if mi_tamañoi = 0 skip or mi_tamañoi = n Q ! mi_mini fi Q :: if P1 ? min skip or … or Pn ? min skip fi
Para facilitar la escritura usamos asignaciones simultáneas de la forma (x1, x2) := (e1, e2). Cada proceso Pi del programa Smin se inicializa con un valor, su mínimo inicial, y un tamaño, su tamaño inicial, de valor 1. Luego ejecuta una repetición, en la que en cada iteración hace lo siguiente. O bien le envía a algún proceso Pj, con i ≠ j, su mínimo actual y su tamaño actual y termina su participación en el programa asignándose un 0 a su tamaño. O bien recibe de algún proceso Pj, con i ≠ j, su mínimo actual y su tamaño actual, por medio de la función min se queda con el mínimo entre el mínimo actual propio y el que recibe, incrementa su tamaño actual con el tamaño que recibe, y continúa participando en el programa a menos que su tamaño actual sea n, lo que implica que obtuvo el mínimo buscado, en cuyo caso se lo envía al proceso Q.
En las secciones que siguen describimos la variante axiomática para verificar programas distribuidos. Por las características del lenguaje de pasajes de mensajes, la variante se basa en el método de verificación que presentamos para los programas secuenciales no determinísticos.
Axiomática para las pruebas de correctitud parcial
Comenzamos con la descripción de la axiomática para la prueba de correctitud parcial. Como con los programas paralelos, la meta es contar con una regla basada en la siguiente estructura:
{pi} Pi* {qi}, i = 1, …, n
{⋀i = 1,n pi} [ || i = 1,n Pi ] {⋀i = 1,n qi}
siendo las {pi} Pi* {qi} proof outlines de correctitud parcial de los procesos que integran el programa distribuido [ || i = 1,n Pi ], obtenidas en una primera etapa de pruebas locales y chequeadas en una segunda etapa de prueba global. En este caso no hace falta chequear que las proof outlines sean libres de interferencia, porque los procesos no comparten variables. Lo que sí se necesita es ratificar los predicados que necesariamente deben asumirse en las pruebas locales, producto de los pasajes de mensajes definidos entre los procesos.
Para las pruebas locales, la axiomática incluye, además de los axiomas SKIP y ASI y la regla SEC, reglas para las instrucciones de entrada/salida y adaptaciones de las reglas de la selección condicional y la repetición no determinísticas que utilizamos en la verificación de programas secuenciales no determinísticos con comandos guardados (NCOND y NREP, respectivamente):
Axioma de la instrucción de entrada (IN)
{p} Pi ? x {q}
p y q son dos predicados arbitrarios con variables locales de un proceso Pj que incluye la instrucción Pi ? x. La arbitrariedad de la relación entre p y q se explica por las características de Pi ? x: en la prueba local de Pj, el valor asignado a la variable x proveniente del proceso Pi sólo puede asumirse, lo mismo que si Pi está preparado para comunicarse con Pj. Las asunciones deben validarse en la segunda etapa de la prueba, en la que se tiene en cuenta el programa completo.
Axioma de la instrucción de salida (OUT)
{p} Pj ! e {p}
p es un predicado con variables locales de un proceso Pi que incluye la instrucción Pj ! e, la cual no tiene efecto sobre las variables locales de Pi. También puede utilizarse el axioma más general {p} Pj ! e {q}, para incluir, como en el axioma IN, una asunción acerca del estado de Pj con respecto a su preparación para comunicarse con Pi. Cualquiera sea el caso, lo que se asume debe chequearse en la segunda etapa de la prueba.
Regla del condicional con comunicaciones (DCOND)
{p Bi} αi ; Si {q}, i = 1, …, n
{p} if B1 ; α1 S1 or … or Bn ; αn Sn fi {q}
La regla es la misma que utilizamos para los programas secuenciales no determinísticos con comandos guardados, pero adaptada considerando la posibilidad de que existan guardias con instrucciones de entrada/salida. La forma planteada es la más general (en los casos en los que los comandos guardados son Bi Si, las premisas correspondientes son {p Bi} Si {q}).
Regla de la repetición con comunicaciones (DREP)
{p Bi} αi ; Si {p}, i = 1, …, n
{p} do B1 ; α1 S1 or … or Bn ; αn Sn do {p ⋀i Bi}
También esta regla, presentada en su forma más general, adapta contemplando guardias con instrucciones de entrada/salida una regla de la axiomática para programas secuenciales con comandos guardados, en este caso la que corresponde a la prueba de no divergencia.
Complementariamente, para la prueba global de la segunda etapa, en la que deben validarse las asunciones de las proof outlines, la axiomática incluye los siguientes componentes:
Axioma de comunicación (COM)
{p[x|e]} Pi ? x || Pj ! e {p}
El axioma captura la semántica de una comunicación entre dos instrucciones de entrada/salida que coinciden sintácticamente, que es la asignación del valor de la expresión e a la variable x. Su utilidad se aprecia en el chequeo de consistencia de las proof outlines, que en el marco de los programas distribuidos se conoce como test de cooperación, el cual pasamos a describir.
El test de cooperación requiere validar, por cada par de proof outlines pi} Pi* {qi} del proceso Pi y {pj} Pj* {qj} del proceso Pj, que para todo par de instrucciones de entrada/salida que coinciden sintácticamente, Pi ? x en Pj por un lado y Pj ! e en Pi por otro lado, la fórmula {p1} Pi ? x {q1} correspondiente a Pi ? x en la proof outline de Pj y la fórmula {p2} Pj ! e {q2} correspondiente a Pj
! e en la proof outline de Pi satisfagan:
{p1 p2} Pi ? x || Pj ! e {q1 q2}
De esta manera, el axioma COM permite validar todas las asunciones de las pruebas locales. Si se cumplen, se define que las proof outlines cooperan. En base a lo definido, la regla de prueba de correctitud parcial de una composición distribuida debería ser:
{pi} Pi* {qi}, i = 1, …, n, son proof outlines que cooperan
{⋀i = 1,n pi} [ || i = 1,n Pi ] {⋀i = 1,n qi}
pero así planteada, la regla está incompleta. Su formulación definitiva la mostramos después de los dos ejemplos de aplicación que presentamos a continuación, en el segundo de los cuales se explicita cómo completarla.
Ejemplo. Prueba de correctitud parcial del programa que propaga un valor
Vamos a verificar la correctitud parcial del programa presentado en la sección previa, que propaga un valor desde un proceso P1 hasta un proceso Pn. Para simplificar la prueba, acotamos el programa a tres procesos:
Sprop :: [P1 || P2 || Pn], con:
P1 :: P2 ! y1
P2 :: P1 ? y2 ; P3 ! y2 P3 :: P2 ? y3
Probaremos la fórmula {y1 = Y} Sprop {y3 = Y}. Proponemos las siguientes proof outlines:
P1 :: {y1 = Y} P2 ! y1 {y1 = Y}
P2 :: {true} P1 ? y2 {y2 = Y} ; P3 ! y2 {y2 = Y} P3 :: {true} P2 ? y3 {y3 = Y}
La correctitud de las proof outlines se verifica fácilmente, aplicando los axiomas IN y OUT y la regla SEC. Resta probar que las proof outlines cooperan. Hay dos pares de instrucciones de entrada/salida que coinciden sintácticamente: P2 ! y1 (en P1) y P1 ? y2 (en P2), y P3 ! y2 (en P2) y P2
? y3 (en P3). Por lo tanto, de acuerdo al test de cooperación, hay que verificar:
{y1 = Y true} P2 ! y1 || P1 ? y2 {y1 = Y y2 = Y}
{y2 = Y true} P3 ! y2 || P2 ? y3 {y2 = Y y3 = Y}
Las fórmulas se prueban aplicando el axioma COM y la regla CONS. Así obtenemos la fórmula
{y1 = Y true true} Sprop {y1 = Y y2 = Y y3 = Y}, y por la regla CONS, {y1 = Y} Sprop {y3 = Y}.
Ejemplo. Prueba de correctitud parcial de un programa que devuelve el número uno
Dado el programa:
S0a1 :: [P1 || P2], con:
P1 :: x := 0 ; P2 ! x ; x := x + 1 ; P2 ! x P2 :: P1 ? y ; P1 ? y
vamos a verificar {true} S0a1 {y = 1}. Las proof outlines naturales de P1 y P2 son: P1 :: {true} x := 0 {x = 0} ; P2 ! x {x = 0} ; x := x + 1 {x = 1} ; P2 ! x {x = 1}
P2 :: {true} P1 ? y {y = 0} ; P1 ? y {y = 1}
que de acuerdo al test de cooperación deben satisfacer:
{x = 0 true} P2 ! x || P1 ? y {x = 0 y = 0}
{x = 1 true} P2 ! x || P1 ? y {x = 1 y = 0}
{x = 0 y = 0} P2 ! x || P1 ? y {x = 0 y = 1}
{x = 1 y = 0} P2 ! x || P1 ? y {x = 1 y = 1}
Las fórmulas de (a) y (d) se prueban fácilmente por medio del axioma COM y la regla CONS. Sin embargo, las fórmulas de (b) y (c) no se cumplen. Por el axioma COM debe valer:
(x = 1 true) ⟶ (x = 1 x = 0) (x = 0 y = 0) ⟶ (x = 0 x = 1)
y ambas implicaciones son falsas. Esto va a ocurrir indefectiblemente con cualquier par de proof outlines que se propongan, porque las fórmulas de (b) y (c) corresponden a comunicaciones imposibles de ejecutarse en el programa, situación que el test de cooperación no contempla tal como está definido. Así, el test debe ajustarse, para que no requiera tratar pares de instrucciones de entrada/salida que coinciden sintácticamente pero no semánticamente.
Lo que plantea la axiomática en este caso es, como antes, recurrir a variables auxiliares (y la regla AUX), para reforzar predicados que precisen la historia del interleaving ejecutado. Pero además introduce una novedad, los invariantes globales, que en alguna medida recuerdan los invariantes de recursos usados con los programas paralelos. Antes de reformular el test de cooperación, completamos la prueba del ejemplo con la idea comentada:
Primero agregamos una variable local auxiliar c1 en el proceso P1 y una variable local auxiliar c2 en el proceso P2, ámbas inicializadas en 0 y que se incrementan en 1 toda vez que el proceso respectivo ejecuta una instrucción de entrada/salida. El incremento y la instrucción de entrada/salida asociada se ejecutan atómicamente. De esta manera, los valores de las variables c1 y c2 siempre son iguales antes y después de cada comunicación del programa, lo que resulta útil para la prueba, como mostramos enseguida. Las proof outlines del programa ampliado quedan así (las secciones atómicas se delimitan con los símbolos < >):
{c1 = 0} {c2 = 0}
[P’1 :: x := 0 ; {x = 0 c1 = 0} P’2 :: <P1 ? y ; c2 := c2 + 1>;{y = 0 c2 = 1}
<P2 ! x;c1 := c1 + 1>;{x = 0 c1 = 1} || < P1 ? y ; c2 := c2 + 1 >] x := x + 1 ; {x = 1 c1 = 1} {y = 1 c2 = 2}
< P2 ! x ; c1 := c1 + 1 >
{x = 1 c1 = 2}
Complementariamente, definimos un invariante global IG = (c1 = c2), que en sintonía con lo anterior, al agregarlo en los chequeos del test de cooperación permite descartar los pares de instrucciones de entrada/salida que coinciden sintácticamente pero no semánticamente, es decir las comunicaciones imposibles de ejecutarse en el programa. Las nuevas fórmulas a verificar con este agregado son las siguientes:
{x = 0 c1 = 0 c2 = 0 (c1 = c2)}
< P2 ! x ; c1 := c1 + 1 > || < P1 ? y ; c2 := c2 + 1 >
{x = 0 c1 = 1 y = 0 c2 = 1 (c1 = c2)}
{x = 1 c1 = 1 c2 = 0 (c1 = c2)}
< P2 ! x ; c1 := c1 + 1 > || < P1 ? y ; c2 := c2 + 1 >
{x = 1 c1 = 2 y = 0 c2 = 1 (c1 = c2)}
{x = 0 c1 = 0 y = 0 c2 = 1 (c1 = c2)}
< P2 ! x ; c1 := c1 + 1 > || < P1 ? y ; c2 := c2 + 1 >
{x = 0 c1 = 1 y = 1 c2 = 2 (c1 = c2)}
{x = 1 c1 = 1 y = 0 c2 = 1 (c1 = c2)}
< P2 ! x ; c1 := c1 + 1 > || < P1 ? y ; c2 := c2 + 1 >
{x = 1 c1 = 2 y = 1 c2 = 2 (c1 = c2)}
Se comprueba fácilmente que ahora se cumplen todas las fórmulas (asumiendo que las reglas utilizan secciones atómicas, lo que comentamos más adelante). Las fórmulas de (b) y (c) se cumplen trivialmente porque las precondiciones son falsas, producto de la información global aportada por el invariante IG, que determina que las comunicaciones correspondientes no pueden ocurrir. Así llegamos a {true true} S0a1 {x = 1 y = 1}, por aplicación de la regla AUX, y por la regla CONS, a {true} S0a1 {y = 1}.
Completado el ejemplo, formalizamos en lo que sigue las modificaciones necesarias para obtener la forma definitiva de la regla de la composición distribuida:
Según cómo aparezca en el programa, toda instrucción de entrada/salida α de toda proof outline se encapsula en una sección atómica < S1 ; α ; S2 > o < α S1 >, en que ni S1 ni S2 contienen instrucciones de entrada/salida (se define que dos secciones atómicas coinciden sintácticamente si lo hacen las instrucciones de entrada/salida que encapsulan).
Se especifica un invariante global IG en términos de las variables de los procesos y de varia- bles auxiliares locales que se agregan al programa, que sólo pueden modificarse dentro de las secciones atómicas. IG debe valer al inicio y ser preservado por toda comunicación. Su rol es proveer información para evitar en las pruebas el tratamiento de pares de instrucciones de entrada/salida que coinciden sintácticamente pero no semánticamente, y por eso se agrega en los chequeos del test de cooperación.
Se reformula el test de cooperación de la siguiente manera. Por cada par de proof outlines
{pi} Pi* {qi} y {pj} Pj* {qi}, para todo par de secciones atómicas < S > (en Pj) y < S´ > (en Pi) que coinciden sintácticamente, la fórmula {p1} < S > {q1} asociada a < S > en la proof outline de Pj y la fórmula {p2} < S´ > {q2} asociada a < S´ > en la proof outline de Pi deben satisfacer:
{p1 p2 IG} < S > || < S´ > {q1 q2 IG}
Se define en este caso que las proof outlines cooperan con respecto al invariante global IG.
Por el uso de secciones atómicas, deben agregarse a la axiomática algunas reglas auxiliares relacionadas con las dos formas definidas, < S1 ; α ; S2 > y < α ⟶ S1 >. Por ejemplo:
{p} S1 ; S3 {r1}, {r1} α || α´ {r2}, {r2} S2 ; S4 {q}
{p} < S1 ; α ; S2 > || < S3 ; α´ ; S4 > {q}
{p} α || α´ {r}, {r} S1 ; S2 {q}
{p} < α ⟶ S1 > || < α´ ⟶ S2 > {q}
Con la nueva definición de cooperación, necesaria en realidad en la prueba de toda propiedad de un programa distribuido para descartar los pares de instrucciones de entrada/salida que
coinciden sintácticamente pero no semánticamente, llegamos a la versión definitiva de la regla de la composición distribuida (cuya aplicación luego es seguida por la de la regla AUX):
Regla de la composición distribuida (DIST)
{pi} Si* {qi}, i = 1, …, n, son proof outlines que cooperan con respecto a IG p ⟶ (⋀i = 1,n pi IG), (⋀i = 1,n qi IG) ⟶ q
{p} [ || i = 1,n Pi ] {q}
tal que ninguna variable de IG puede ser modificada fuera de las secciones atómicas.
Axiomática para las pruebas de no divergencia
En los programas distribuidos, a diferencia de lo que observamos en los programas paralelos, al no haber variables compartidas las pruebas no tienen que reparar en el impacto de un proceso por esta vía sobre el valor del variante definido para una repetición de otro proceso. Pero aparece otra dificultad, que es que la no divergencia de un proceso no siempre puede probarse localmente, dadas sus comunicaciones con otros procesos. Por ejemplo, que el proceso:
P1 :: do x 0 ; P2 ? x skip od
no diverja depende de si recibe alguna vez del proceso P2 el valor 0. Así que en este caso también hay que recurrir a asunciones en las pruebas locales y verificarlas en el test de cooperación de la prueba global (incluyendo variables auxiliares locales y un invariante global). En particular, puede ser necesario asumir el valor inicial de algunos variantes, si la cantidad de iteraciones de las repeticiones correspondientes depende de información global.
En las pruebas locales, para verificar la no divergencia de una repetición se utiliza la misma regla que definimos para los programas secuenciales con comandos guardados, pero ahora contemplando instrucciones de entrada/salida en las guardias. Su forma más general es:
Regla de la no divergencia con comunicaciones (DREP*)
〈p Bi〉 αi ; Si 〈p〉, i = 1, …, n, 〈p Bi t = Z〉 αi ; Si 〈t < Z〉, i = 1, …, n, p t 0
〈p〉 do B1 S1 or…or Bn Sn od 〈p ⋀i = 1,n ¬Bi〉
tal que p y t son el invariante y el variante de la repetición, respectivamente. Para la prueba global se recurre al test de cooperación de la misma manera que en la prueba de correctitud parcial:
Regla de la no divergencia distribuida (DIST*)
〈pi〉 Si** 〈qi〉, i = 1, …, n, son proof outlines que cooperan con respecto a IG p ⟶ (⋀i = 1,n pi IG), (⋀i = 1,n qi IG) ⟶ q
〈p〉 [ || i = 1,n Pi ] 〈q〉
tal que ninguna variable de IG puede ser modificada fuera de las secciones atómicas. Mostramos a continuación un ejemplo de aplicación de estas reglas sobre un programa muy sencillo.
Ejemplo. Prueba de no divergencia de un programa con diez iteraciones
Vamos a probar:
〈0 x 10 y > 0〉 Sdiez :: [P1 || P2 ] 〈true〉, con:
P1 :: do x 0 ; P2 ! x x := x – 1 od P2 :: do y 0 ; P1 ? y skip od
Primero definimos las secciones atómicas del programa, y agregamos en el proceso P2 una variable auxiliar w para diferenciar las instancias anterior y posterior de la primera iteración de su instrucción de repetición, cuya utilidad explicamos enseguida:
P´1 :: do x 0 ; < P2 ! x x := x – 1 > od
P’2 :: w := 0 ; do y 0 ; < P1 ? y skip ; w := 1 > od
Para la prueba de no divergencia del proceso P1 definimos como invariante de su repetición el predicado p1 = (x – 1), y como variante la función t1 = x + 1. De acuerdo a la regla DREP*, deben cumplirse las siguientes fórmulas:
〈x – 1 x 0〉 P2 ! x ; x := x – 1 〈x – 1〉
〈x – 1 x 0 x + 1 = Z〉 P2 ! x ; x := x – 1 〈x + 1 < Z〉
x – 1 x + 1 0
que se verifican fácilmente por medio de los axiomas ASI y OUT y las reglas SEC y CONS.
La prueba de no divergencia del proceso P2 es más complicada, porque el valor de la variable y depende de lo que recibe de P1. Definimos para la repetición de P2 el invariante p2 = (y 0) y el variante t2 = (if w = 0 then 11 else y fi). La variable auxiliar w sirve para asignar un valor inicial al variante. En este caso, las fórmulas que deben cumplirse por DREP* son:
〈y 0 y 0〉 P1 ? y ; skip ; w := 1 〈y 0〉
〈y 0 y 0 (if w = 0 then 11 else y fi) = Z〉
P1 ? y ; skip ; w := 1
〈(if w = 0 then 11 else y fi) < Z〉
y 0 (if w = 0 then 11 else y fi) 0
que también se prueban fácilmente, aplicando los axiomas SKIP, ASI e IN y las reglas SEC y CONS. Las proof outlines de los procesos ampliados quedan así:
〈inv: x – 1, var: x + 1〉
P´1 :: do x 0 ; 〈x – 1 x 0〉 < P2 ! x x := x – 1 > od
〈x – 1〉
〈y > 0〉
P´2 :: w := 0 ;
〈inv: y 0, var: if w = 0 then 11 else y fi〉
do y 0 ; 〈y 0 y 0〉 < P1 ? y skip ; w := 1 > od
〈y 0〉
Se cumple que la precondición del programa implica la conjunción de las precondiciones de los procesos:
(0 x 10 y > 0) (x – 1 y > 0).
Para la segunda etapa de la prueba planteamos el siguiente invariante global: IG = (0 w 1 (w = 1 y = x + 1))
alineado con el comportamiento del programa modificado, por lo que el chequeo requerido por el test de cooperación utilizado por la regla DIST* queda planteado de esta forma:
〈x – 1 x 0 y 0 y 0 (0 w 1 (w = 1 y = x + 1)〉
< P2 ! x ⟶ x := x – 1 > || < P1 ? y ⟶ skip ; w := 1 >
〈x – 1 y 0 (0 w 1 (w = 1 y = x + 1)〉
La fórmula se verifica por medio de la segunda regla auxiliar presentada en la sección anterior, los axiomas SKIP, ASI y COM y las reglas SEC y CONS. La prueba se completa aplicando la regla AUX.
Con hipótesis de fairness en los programas distribuidos, en las pruebas de no divergencia (y en general en las pruebas de cualquier propiedad de tipo liveness) se plantean más escenarios que el de nivel proceso que mencionamos en el marco de los programas paralelos. Por ejemplo, con hipótesis de fairness fuerte se pueden definir los siguientes dos niveles adicionales:
Nivel canal: todo par de procesos infinitas veces preparados para comunicarse se comunican infinitas veces.
Nivel comunicación: toda comunicación infinitas veces habilitada se ejecuta infinitas veces.
El siguiente programa sirve para aclarar las definiciones anteriores. En este caso, la no divergencia sólo se logra con fairness fuerte de nivel comunicación:
[P1 :: b := true ; P2 :: c := true ;
do b ; P2 ? b skip od || do c ; P1 ! true skip
or c ; P1 ! false c := false od]
El programa termina si P2 toma alguna vez la segunda dirección de su instrucción de repetición, lo que no se puede asegurar con fairness fuerte de niveles proceso o canal.
La no divergencia con fairness se puede probar en base a direcciones útiles, como hicimos con los programas secuenciales no determinísticos, pero ahora considerando, en lugar de direcciones habilitadas, pares de direcciones habilitadas.
Axiomática para las pruebas de ausencia de falla
Completamos la presentación de la axiomática con una breve referencia a la verificación de la propiedad de ausencia de falla. Un programa distribuido falla si durante su ejecución, en una
selección condicional todas las expresiones booleanas de sus guardias son falsas, o si se produce una situación de deadlock. Para verificar la ausencia de falla del primer caso, la axiomática incluye una regla similar a la regla DCOND utilizada para la prueba de correctitud parcial, con una premisa adicional. Su forma más general es:
Regla del condicional con comunicaciones sin falla (DCOND*) p ⋁i = 1,n Bi, {p Bi} αi ; Si {q}, i = 1, …, n
{p} if B1 ; α1 S1 or … or Bn ; αn Sn fi {q}
La premisa p ⋁i = 1,n Bi asegura que al menos una guardia de la selección condicional tiene una expresión booleana verdadera. Con respecto a la prueba de ausencia de deadlock, la regla correspondiente se basa en el mismo esquema que planteamos para los programas paralelos:
Regla de la ausencia de deadlock en programas distribuidos (DDEADLOCK)
Dadas proof outlines (con secciones atómicas y que cooperan con respecto a un invariante global IG), se identifican sintácticamente todas las posibles situaciones de deadlock, se obtienen las imágenes semánticas asociadas, y se prueba que todas resultan falsas. Por las características de los programas distribuidos, los predicados que integran las imágenes semánticas pueden ser:
post(Pi), la postcondición de la proof outline del proceso Pi.
pre(< S >), la precondición de una sección atómica S de la forma S1 ; α ; S2.
pre(S) ^ ⋀i H Bi ^ ⋀j H ¬Bj, la precondición de una selección condicional o una repetición S, en conjunción con un predicado que establece que S tiene un subconjunto H no vacío de direcciones con expresiones booleanas verdaderas.
No puede haber sólo predicados del primer tipo, porque si no la imagen semántica no representaría una situación de deadlock. Como ejemplo de aplicación de esta regla, consideramos nuevamente el programa de propagación de un valor.
Para verificar la correctitud parcial de Pprop :: [P1 :: P2 ! y1 || P1 ? y2 ; P3 ! y2 || P2 ? y3] hemos utilizado en una sección anterior las proof outlines:
P1 :: {y1 = Y} P2 ! y1 {y1 = Y}
P2 :: {true} P1 ? y2 {y2 = Y}; P3 ! y2 {y2 = Y} P3 :: {true} P2 ? y3 {y3 = Y}
que no sirven en este caso para probar la ausencia de deadlock. Por ejemplo, la imagen semántica correspondiente a la situación de deadlock en que P1 terminó y P¨2 y P3 no empezaron:
y1 = Y true true
no es falsa. Se necesita recurrir a variables auxiliares y un invariante global. Agregamos una variable wi en cada proceso Pi, tal que wi = 0 significa que Pi está preparado para recibir un
valor, wi = 1 que Pi está preparado para enviar un valor, y wi = 2 que Pi terminó. La variable w1 se inicializa en 1, y las variables w2 y w3 en 0. Correspondientemente con esta idea, definimos el siguiente invariante global:
IG = (w1 = 1 w2 = 0 w3 = 0) (w1 = 2 w2 = 1 w3 = 0) (w1 = 2 w2 = 2 w3 = 2) Las proof outlines de los procesos ampliados quedan de la siguiente manera:
{w1 = 1} {w2 = 0} {w3 = 0}
[< P2 ! y1 ; w1 := 2> || <P1 ? y2 ; w2 := 1> || <P2 ? y3 ; w3 := 2>]
{w1 = 2} {w2 = 1} {w3 = 2}
<P3 ! y2 ; w2 := 2>
{w2 = 2}
La cooperación entre las proof outlines con respecto a IG se prueba fácilmente, empleando la primera regla auxiliar presentada previamente. Notar que ahora la imagen semántica que representa la situación en la que P1 terminó y P¨2 y P3 no empezaron, incluyendo el invariante IG, resulta falsa:
(w1 = 2 w2 = 0 w3 = 0)
[(w1 = 1 w2 = 0 w3 = 0) (w1 = 2 w2 = 1 w3 = 0) (w1 = 2 w2 = 2 w3 = 2)]
Se comprueba fácilmente lo mismo con el resto de las situaciones posibles de deadlock.
Notas adicionales
Incluimos una nota en la que nos referimos resumidamente a la verificación axiomática de programas distribuidos con comunicaciones asincrónicas, y otra sobre alternativas composicionales al método no composicional de pruebas locales y globales que hemos considerado en este artículo y el anterior.
Verificación con comunicaciones asincrónicas
En los programas distribuidos con comunicaciones asincrónicas los procesos ejecutan las instrucciones de salida sin tener en cuenta la disponibilidad de sus contrapartes para recibir los mensajes. Sólo las instrucciones de entrada pueden tener que esperar para ejecutarse, y así provocar eventualmente bloqueos en los procesos que las contienen. La semántica informal de ambas instrucciones en esta clase de programas es la siguiente (consideramos un lenguaje distribuido similar al presentado antes, reemplazando los símbolos ? y ! por ?? y !!, respectivamente, y utilizando identificadores de canales en lugar de identificadores de procesos y guardias sin instrucciones de salida):
Instrucción de entrada c ?? x (en un proceso receptor Pr): Si en el canal c existe un valor disponible, éste se asigna a la variable local x de Pr. Si no, Pr queda bloqueado hasta que haya un valor en c.
Instrucción de salida c !! e (en un proceso emisor Pe): Pe envía al canal c el valor de la expresión e, definida en términos de sus variables locales, y continúa con la ejecución de la siguiente instrucción.
Otras características del lenguaje son: todo canal conecta a un único proceso emisor con un único proceso receptor, la única hipótesis sobre el tiempo entre el envío y la recepción de un mensaje es que es finito, y los mensajes llegan en el orden en el que se envían. Por ejemplo, el siguiente programa calcula el máximo de un conjunto de n valores xi, todos distintos, en base a una estructura de anillo de n procesos distribuidos:
Smax :: [ || i = 1,n Pi ], con:
Pi :: zi := 0 ; yi := 0 ; ci !! xi ; do yi N ci–1 ?? yi ;
if xi = yi zi := 1 ; yi := N ; ci !! N or xi yi skip
or xi yi ci !! yi
fi
od
El canal ci comunica al proceso Pi con su vecino de la derecha, Pi+1 (o P1 si i = n). Pi contiene el valor xi, que envía al inicio. Luego, iterativamente, Pi envía todo valor yi mayor que su valor xi, que recibe de su vecino de la izquierda, Pi –1, en el canal ci–1 (o Pn en cn si i = 1). De esta manera, sólo el valor máximo recorre el anillo completo de procesos, situación que detecta el proceso Pi que recibe su valor xi, en cuyo caso se identifica ejecutando la asignación zi := 1 y hace finalizar el programa enviando un valor N mayor que todos los xi al resto de los procesos. En [SS84] se describe una variante axiomática para verificar programas del lenguaje descripto, basada en el esquema de pruebas en dos etapas de S. Owicki y D. Gries. A cada canal c se le asocian dos variables de tipo secuencia para utilizar en las pruebas, una variable INc, local del proceso receptor, y una variable OUTc, local del proceso emisor, que representan la secuencia de valores recibidos por uno y la secuencia de valores enviados por el otro, respectivamente.
Los axiomas para las pruebas locales relacionados con las instrucciones de entrada/salida son:
Axioma de la instrucción de entrada asincrónica (AIN)
{p} c ?? x {q}
Al igual que el axioma IN para las comunicaciones sincrónicas, plantea en el caso más general asunciones sobre el valor recibido y sobre la posibilidad de recibir un mensaje, a ser validadas en el test de cooperación de la prueba global.
Axioma de la instrucción de salida asincrónica (AOUT)
{p[OUTc|OUTC.e]} c !! e {p}
El axioma captura el efecto de la instrucción de salida: el envío del valor de la expresión e al final de la secuencia de valores enviados al canal c (OUTC.e expresa la concatenación de la secuencia representada por OUTc con e). En este caso, la precondición y la postcondición coinciden siempre,
porque en una comunicación asincrónica no se necesita asumir nada sobre la disponibilidad del proceso receptor para recibir un mensaje.
Axioma del orden de llegada (FIFO)
Para todo k, si |INc| = k entonces |OUTc| k, y INc[k] = OUTc[k]
|INc| expresa el tamaño de la secuencia INc, e INc[k] el valor k-ésimo de la misma. Lo mismo se define para OUTc. El axioma establece que los mensajes se reciben en el orden en el que se envían (FIFO abrevia first in first out, es decir, el primero que entra es el primero que sale).
En lo que hace a los componentes de la axiomática para la prueba global, cabe destacar que por el uso de las variables INc y OUTc, en el test de cooperación no hace falta recurrir a un invariante global. El test consiste en confrontar, para cada par de proof outlines, todos los pares de instrucciones de entrada/salida que coinciden sintácticamente, que en este caso están constituidos por una instrucción de entrada y una instrucción de salida que actúan sobre un mismo canal. Específicamente, dadas {p1} c ?? x {q1} y {p2} c !! e {q2} debe cumplirse:
{p1 p2 INc = OUTc} c ?? x || c !! e {q1}
No se considera la postcondición de la instrucción de salida, acorde con la semántica de las comunicaciones asincrónicas. La igualdad INc = OUTc permite descartar las instrucciones de entrada/salida que no coinciden semánticamente. Para llevar a cabo el test se emplea el siguiente el axioma:
Axioma de comunicación asincrónica (ACOM)
{p[x|e][INc|INC.e]} Pi ? x || Pj ! e {p}
que captura la semántica de la comunicación asincrónica. Según lo definido, se puede formular la siguiente regla para la prueba de correctitud parcial:
Regla de la composición distribuida con comunicaciones asincrónicas (ADIST) pi} Si* {qi}, i = 1, …, n, son proof outlines que cooperan
p ⟶ (⋀i = 1,n pi ⋀c INc = OUTc = λ), (⋀i = 1,n qi) ⟶ q
{p} [ || i = 1,n Pi ] {q}
Se agrega ⋀c INc = OUTc = λ en la precondición para indicar que al comienzo todos los canales están vacíos (tienen la secuencia vacía λ). El resto de las propiedades se prueban a partir de proof outlines de correctitud parcial que cooperan.
Métodos de prueba composicionales
A la variante axiomática no composicional de S. Owicki y D. Gries le sucedieron varias propuestas composicionales. La primera, para la correctitud parcial de programas paralelos, es [Jon81]. En [XdRH97] se la describe y amplía para la prueba de correctitud total, incluyendo además con- sideraciones sobre la sensatez y la completitud de la axiomática. La idea básica es incluir en la especificación la información de las interferencias entre los procesos y el entorno de ejecución.
A cada proceso, además de su pre y postcondición, se le asocia una condición de fiabilidad, que establece lo que el proceso espera del entorno, y una condición de garantía, que establece cómo el proceso influencia en el entorno. Así, la verificación debe contemplar las relaciones entre dichas condiciones (por ejemplo, debe asegurar que lo que garantiza un proceso implica lo que esperan los otros procesos de él). Más en detalle, utilizando para simplificar sólo dos procesos S1 y S2, se plantea lo siguiente:
En cuanto a la especificación: dada una precondición p y una postcondición q de una com- posición concurrente [S1 || S2], definir un conjunto de variables auxiliares y dos tuplas de predicados (p1, q1, rely1, guar1) y (p2, q2, rely2, guar2) para S1 y S2, respectivamente, siendo p1 y p2 las precondiciones, q1 y q2 las postcondiciones, y rely1, guar1, rely2 y guar2 relaciones que establecen transformaciones entre las variables compartidas y auxiliares. El significado de la tupla (pi, qi, relyi, guari) es que cuando Si se ejecuta a partir de un estado que satisfice pi, en un entorno en el que se pueden modificar las variables compartidas y auxiliares de acuerdo a la condición relyi, el proceso lleva a cabo transformaciones que respetan la condición guari, y si termina, lo hace en un estado que satisface qi.
En cuanto a la verificación: elaborar proof outlines de S1 y S2 que satisfagan las condiciones establecidas (por ejemplo, que los invariantes se preserven teniendo en cuenta las condiciones
relyi), para llegar a la fórmula {p1 ^ p2} [S1 || S2] {q1 ^q2}, y finalmente, mediante las reglas de las variables auxiliares y de consecuencia, a {p} [S1 || S2] {q}.
Para el tratamiento de la ausencia de deadlock se sigue una línea similar, agregando en la especificación información acerca de los posibles bloqueos de los procesos. Con respecto a la no divergencia, la idea es directamente adaptar la regla de no divergencia de la variante no composicional, considerando las nuevas condiciones. Las mismas nociones generales pueden aplicarse a los programas distribuidos. El enfoque descripto convive con el de S. Owicki y D. Gries, lo que se explica porque este último resulta más accesible, sobre todo para especificar los invariantes. Un método axiomático composicional es más conveniente fundamentalmente para el desarrollo sistemático de programas, permite que los procesos se deriven y prueben directamente desde las especificaciones, y que en general las propiedades de los programas se infieran a partir de las propiedades de los procesos, sin necesidad de chequear la consistencia de las proof outlines. Entre las metodologías de desarrollo con los principios mencionados se destaca UNITY o Unbounded Nondeterministic Iterative Transformations (Transformaciones Iterativas no Determinísticas no Acotadas), presentada por primera vez en [CM88]. Esta obra se considera fundacional para el desarrollo sistemático de programas concurrentes. La metodología incluye las etapas de especificación y verificación. Aunque se basa en la lógica temporal, comentamos en lo que sigue algunas de sus características para profundizar en lo que aporta un método composicional. Un programa UNITY es esencialmente una repetición infinita de asignaciones condicionales que se ejecutan no determinísticamente en tanto estén habilitadas infinitas veces. Existe una noción de terminación, que se manifiesta si al cabo de una cantidad finita de iteraciones se alcanza un estado que no se modifica más (se lo conoce como punto fijo). A partir de una primera versión de programa, la idea es refinarla gradualmente, hasta alcanzar el nivel de detalle esperado, instanciado a una de varias arquitecturas posibles. Existen dos estrategias de construcción de programas, la unión y la superposición, que representan la composición y el refinamiento, respectivamente. La unión de dos procesos S1 y S2, denotada con [S1 || S2], consiste en su concatenación, mientras que la superposición establece una programación por capas, de modo tal que a una nueva capa se le agregan variables y asignaciones que no alteran el cómputo
de las capas inferiores. Las especificaciones se definen en términos de cuatro operadores básicos,
FP, unless, ensures y leads-to:
FP.S establece el conjunto de puntos fijos del programa S.
p unless q establece que si se cumple p, q no se cumple nunca y p se cumple siempre, o q se cumple a futuro y p se cumple mientras q no se cumpla. De este operador se derivan invariant p (p se cumple siempre) y stable p, equivalente a p unless false.
p ensures q establece que si se cumple p, q se cumple a futuro y p se cumple mientras q no se cumpla.
p leads-to q establece que si se cumple p, q se cumple a futuro.
La metodología propone hacer gran parte de la tarea de desarrollo de un programa en la etapa de especificación, para facilitar su cálculo top-down y la verificación de sus propiedades a partir de las propiedades de los procesos. En este último sentido, se demuestra por ejemplo que:
Se cumple p unless q en [S1 || S2] si se cumple p unless q en los dos procesos.
Se cumple p ensures q en [S1 || S2] si se cumple p ensures q en un proceso y p unless q en el otro.
En general, no se puede inferir que p leads-to q se cumple en [S1 || S2] aún cumpliéndose en los dos procesos. Con respecto a la estrategia de superposición, mientras facilita la verificación, como contrapartida exige conocer en detalle las capas previamente desarrolladas, al tiempo que su tratamiento algebraico es limitado.
Observaciones finales
El método descripto utiliza los mismos conceptos generales estudiados previamente. Las axiomáticas resultan excelentes guías para la obtención de programas correctos por construcción, y las nociones de invariante y variante constituyen la parte fundamental de la metodología de pruebas.
Sin embargo, tiene una diferencia relevante con respecto a las variantes axiomáticas para los programas secuenciales, que ya destacamos en el caso de los programas paralelos: no es composicional, producto del tipo de especificación que maneja (en la nota adicional sobre alternativas composicionales se aprecian las características principales que debe tener una axiomática composicional).
Otra característica diferencial es el uso de variables auxiliares para registrar las historias de las computaciones cuando las variables de programa no resultan suficientes (lo que también comentamos con los programas paralelos), y de invariantes globales ante la ausencia de estados que reúnan información común a todos los procesos.
Desde el punto de vista del desarrollo sistemático de programas, en general se acepta que el modelo distribuido tiene ventajas en relación al modelo paralelo, lo que se percibe en la práctica por la existencia de metodologías de construcción de programas del primer modelo más disciplinadas, característica que se refleja también en las pruebas asociadas.
Referencias
» [AFdR80] Apt, K., Francez, N. y de Roever, W. A proof system for communicating sequential processes. ACM Trans. Prog. Lang. Syst., 2, 3, 359-385, 1980.
» [CM88] Chandy, K. y Misra J. Parallel program design: a foundation. Addison-Wesley, 1988.
» [Hoa78] Hoare, C. Communicating secuential processes. Comm. ACM, 21, 8, 666-677, 1978.
» [Jon81] Jones, C. Development methods for computer programs including a notion of interference. Technical Monograph PRG-25, Oxford University, 1981.
» [OG76a] Owicki, S. y Gries, D. An axiomatic proof technique for parallel programs. Acta Informatica, 6, 319-340, 1976.
» [OG76b] Owicki, S. y Gries, D. Verifying properties of parallel programs: an axiomatic approach.
Comm. ACM, 19, 5, 279-285, 1976.
» [Ros22a] Rosenfeld, R. Introducción a la verificación de programas. Revista Abierta de Informática Aplicada, 6, 1, 79-100, 2022.
» [Ros22b] Rosenfeld, R. Verificación de programas no determinísticos. Revista Abierta de Informática Aplicada, 6, 2, 54-79, 2022.
» [Ros23] Rosenfeld, R. Verificación de programas paralelos. Revista Abierta de Informática Aplicada, 7, 1, 67-93, 2023.
» [SS84]Schlichting, R. y Schneider, F. Message passing for distributed programming. ACM Trans. Prog. Lang. Syst., 6, 3, 402-431, 1984.
» [XdRH97] Xu, Q., de Roever, W y He, J. The rely-guarantee method for verifying shared variable concurrent pograms. Formal Aspects of Computing, 9, 2, 149-174, 1997.