En informática , la libertad de interferencia es una técnica para demostrar la corrección parcial de programas concurrentes con variables compartidas. La lógica de Hoare se había introducido anteriormente para demostrar la exactitud de los programas secuenciales. En su tesis doctoral [1] (y los artículos derivados de ella [2] [3] ) bajo la dirección de David Gries , Susan Owicki amplió este trabajo para aplicarlo a programas concurrentes.
La programación concurrente se había utilizado desde mediados de la década de 1960 para codificar sistemas operativos como conjuntos de procesos concurrentes (ver, en particular, Dijkstra. [4] ), pero no existía ningún mecanismo formal para demostrar su corrección. El razonamiento sobre secuencias de ejecución entrelazadas de los procesos individuales era difícil, propenso a errores y no se ampliaba. La libertad de interferencia se aplica a las pruebas en lugar de a las secuencias de ejecución; Se muestra que la ejecución de un proceso no puede interferir con la prueba de corrección de otro proceso.
Se ha demostrado que una variedad de programas concurrentes complejos son correctos utilizando la libertad de interferencia, y la libertad de interferencia proporciona la base para gran parte del trabajo posterior para desarrollar programas concurrentes con variables compartidas y demostrar que son correctos. El artículo de Owicki-Gries Una técnica de prueba axiomática para programas paralelos I [2] recibió el premio ACM de 1977 al mejor artículo sobre lenguajes y sistemas de programación. [5] [6]
Nota. Lamport [7] presenta una idea similar. Escribe: "Después de escribir la versión inicial de este artículo, nos enteramos del trabajo reciente de Owicki. [1] [2] " Su artículo no ha recibido tanta atención como Owicki-Gries, tal vez porque utilizó diagramas de flujo en lugar de el texto de la programación se construye como la declaración if y el bucle while . Lamport estaba generalizando el método de Floyd [8] mientras que Owicki-Gries estaba generalizando el método de Hoare. [9] Básicamente, todo el trabajo posterior en esta área utiliza texto y no diagramas de flujo. Otra diferencia se menciona a continuación en la sección sobre variables auxiliares.
Edsger W. Dijkstra introdujo el principio de no interferencia en EWD 117, "Programación considerada como una actividad humana", escrito alrededor de 1965. [10] Este principio establece que: La corrección del todo puede establecerse teniendo en cuenta sólo la especificaciones exteriores ( especificaciones abreviadas en todas partes) de las piezas, y no su construcción interior. Dijkstra describió los pasos generales para utilizar este principio:
Dio varios ejemplos de este principio fuera de la programación. Pero su uso en programación es una preocupación principal. Por ejemplo, un programador que utiliza un método (subrutina, función, etc.) debe confiar únicamente en su especificación para determinar qué hace y cómo llamarlo, y nunca en su implementación.
Las especificaciones del programa están escritas en lógica Hoare , introducida por Sir Tony Hoare , [9] como se ejemplifica en las especificaciones de los procesos S1 y S2 :
{pre-S1 } {pre-S2 } S1 S2 {post-S1 } {pre-S2 }
Significado: Si termina la ejecución de Si en un estado en el que la condición previa pre-Si es verdadera, al finalizar, la poscondición post-Si es verdadera.
Consideremos ahora la programación concurrente con variables compartidas. Las especificaciones de dos (o más) procesos S1 y S2 se dan en términos de sus condiciones previas y posteriores, y suponemos que se dan implementaciones de S1 y S2 que satisfacen sus especificaciones. Pero al ejecutar sus implementaciones en paralelo, dado que comparten variables, puede ocurrir una condición de carrera ; un proceso cambia una variable compartida a un valor que no se anticipa en la prueba del otro proceso, por lo que el otro proceso no funciona según lo previsto.
Por tanto, se viola el principio de no interferencia de Dijkstra.
En su tesis doctoral de 1975 [1] en Ciencias de la Computación , Universidad de Cornell , escrita bajo la dirección de David Gries , Susan Owicki desarrolló la noción de libertad de interferencia . Si los procesos S1 y S2 cumplen con la libertad de interferencia, entonces su ejecución en paralelo funcionará según lo planeado. Dijkstra calificó este trabajo como el primer paso significativo hacia la aplicación de la lógica de Hoare a procesos concurrentes. [11] Para simplificar las discusiones, restringimos la atención a sólo dos procesos concurrentes, aunque Owicki-Gries [2] [3] permite más.
Owicki-Gries [2] [3] presentó el esquema de prueba para una triple {P}S{Q } de Hoare. Contiene todos los detalles necesarios para demostrar la exactitud de {P}S{Q } utilizando los axiomas y las reglas de inferencia de la lógica de Hoare . (Este trabajo utiliza la declaración de asignación x: = e , las declaraciones if-then y if-then-else y el bucle while ). Hoare aludió a los esquemas de prueba en sus primeros trabajos; para la libertad de injerencia, había que formalizarla.
Un esquema de prueba para { P}S{Q } comienza con la condición previa P y termina con la condición posterior Q. Dos afirmaciones entre llaves { y } que aparecen una al lado de la otra indican que la primera debe implicar la segunda.
Ejemplo: un esquema de prueba para {P} S {Q } donde S es:
x : = a; si e entonces S1 si no S2
{P } {P1[x/a] } x : = a; {P1 } si e entonces {P1 ∧ e } S1 {Q1 } más {P1 ∧ ¬ e } S2 {Q1 } {Q1 } {Q }
P ⇒ P1[x/a] debe cumplirse, donde P1[x/a] representa P1 con cada aparición de x reemplazada por a . (En este ejemplo, S1 y S2 son declaraciones básicas, como una declaración de asignación, skip o una declaración de espera ).
Cada declaración T en el esquema de prueba está precedida por una precondición pre-T y seguida por una poscondición post-T , y {pre-T}T{post-T } debe ser demostrable usando algún axioma o regla de inferencia de la lógica de Hoare. Por lo tanto, el esquema de prueba contiene toda la información necesaria para demostrar que {P}S{Q } es correcto.
Ahora considere dos procesos S1 y S2 que se ejecutan en paralelo y sus especificaciones:
{pre-S1 } {pre-S2 } S1 S2 {post-S1 } {post-S2 }
Para demostrar que funcionan adecuadamente en paralelo será necesario restringirlos de la siguiente manera. Cada expresión E en S1 o S2 puede referirse como máximo a una variable y que puede ser cambiada por el otro proceso mientras se evalúa E , y E puede referirse a y como máximo una vez. Una restricción similar se aplica a las declaraciones de asignación x: = E .
Con esta convención, la única acción indivisible debe ser la referencia a la memoria. Por ejemplo, supongamos que el proceso S1 hace referencia a la variable y mientras que S2 cambia y . El valor que S1 recibe para y debe ser el valor antes o después de que S2 cambie y , y no algún valor intermedio espurio.
Definición de libre de interferencias
La innovación importante de Owicki-Gries fue definir lo que significa que un enunciado T no interfiera con la prueba de {P}S{Q }. Si la ejecución de T no puede falsificar ninguna afirmación dada en el esquema de prueba de { P}S{Q }, entonces esa prueba aún es válida incluso frente a la ejecución concurrente de S y T.
Definición . La declaración T con precondición pre-T no interfiere con la prueba de {P}S{Q } si se cumplen dos condiciones:
(1) {Q ∧ pre-T} T {Q }
(2) Sea S' cualquier declaración dentro de S pero no dentro de una declaración en espera (ver la sección posterior). Entonces {pre-S' ∧ pre-T} T {pre-S' }.
Lea el último triplete de Hoare así: Si el estado es tal que tanto T como S' pueden ejecutarse, entonces la ejecución de T no va a falsificar pre-S' .
Definición . Los esquemas de prueba para {P1}S1{Q1 } y {P2}S2{Q2 } están libres de interferencias si se cumple lo siguiente. Sea T una declaración de espera o asignación (que no aparece en una espera ) del proceso S1 . Entonces T no interfiere con la prueba de {P2}S2{Q2 }. De manera similar para T del proceso S2 y {P1}S1{Q1 }.
Se introdujeron dos declaraciones para abordar la concurrencia. Ejecución de la sentencia cobegin S1 // S2 coend ejecuta S1 y S2 en paralelo. Termina cuando tanto S1 como S2 han terminado.
La ejecución de la declaración de espera espera a B y luego S se retrasa hasta que la condición B sea verdadera. Entonces, la afirmación S se ejecuta como una acción indivisible: la evaluación de B es parte de esa acción indivisible. Si dos procesos están esperando la misma condición B , cuando se cumple, uno de ellos continúa esperando mientras el otro continúa.
La declaración de espera no se puede implementar de manera eficiente y no se propone insertarla en el lenguaje de programación. Más bien, proporciona un medio para representar varias primitivas estándar, como los semáforos: primero expresa las operaciones del semáforo como await s y luego aplica las técnicas descritas aquí.
Las reglas de inferencia para await y cobegin son:
espera
{P ∧ B} S {Q}/{P} espera B y luego S {Q}
comenzar
{P1} S1 {Q1}, {P2} S2 {Q2}
libre de interferencias/{P1∧P2} cobegin S1//S2 coend {Q1∧Q2}
Una variable auxiliar no aparece en el programa, pero se introduce en la prueba de corrección para simplificar (o incluso hacer posible) el razonamiento. Las variables auxiliares se utilizan sólo en asignaciones de variables auxiliares, por lo que su introducción no altera el programa para ninguna entrada ni afecta los valores de las variables del programa. Normalmente, se utilizan como contadores de programas o para registrar historiales de un cálculo.
Definición . Sea AV un conjunto de variables que aparecen en S' sólo en las asignaciones x: = E , donde x está en AV . Entonces AV es una variable auxiliar establecida para S' .
Dado que un conjunto AV de variables auxiliares se usa solo en asignaciones a variables en AV , eliminar todas las asignaciones a ellas no cambia la corrección del programa, y tenemos la regla de inferencia de eliminación AV :
{P}S'{Q}/{P} S {Q}
AV es una variable auxiliar establecida para S' . Las variables en AV no ocurren en P o Q. S se obtiene de S' eliminando todas las asignaciones a las variables en AV .
En lugar de utilizar variables auxiliares, se puede introducir un contador de programa en el sistema de prueba, pero eso añade complejidad al sistema de prueba.
Nota: Apt [12] analiza la lógica de Owicki-Gries en el contexto de aserciones recursivas , es decir, aserciones efectivamente computables . Demuestra que todas las afirmaciones en los esquemas de prueba pueden ser recursivas, pero que este ya no es el caso si las variables auxiliares se utilizan sólo como contadores de programas y no para registrar historias de cálculo. Lamport, en su trabajo similar, [7] utiliza afirmaciones sobre posiciones de tokens en lugar de variables auxiliares, donde un token en un borde de un diagrama de flujo es similar a un contador de programa. No existe la noción de una variable histórica. Esto indica que el enfoque de Owicki-Gries y Lamport no es equivalente cuando se limita a afirmaciones recursivas.
Owicki-Gries [2] [3] trata principalmente de la corrección parcial: {P} S {Q } significa: Si S ejecutado en un estado en el que P es verdadero termina, entonces Q es verdadero en el estado al momento de la terminación. Sin embargo, Owicki-Gries también ofrece algunas técnicas prácticas que utilizan información obtenida de una prueba de corrección parcial para derivar otras propiedades de corrección, incluida la ausencia de punto muerto, la terminación del programa y la exclusión mutua.
Un programa está en punto muerto si todos los procesos que no han terminado están ejecutando declaraciones de espera y ninguno puede continuar porque sus condiciones de espera son falsas. Owicki-Gries proporciona condiciones bajo las cuales no puede ocurrir un punto muerto.
Owicki-Gries presenta una regla de inferencia para la corrección total del ciclo while . Utiliza una función vinculada que disminuye con cada iteración y es positiva siempre que la condición del bucle sea verdadera. Apt et al [13] muestran que esta nueva regla de inferencia no satisface la libertad de interferencia. El hecho de que la función ligada sea positiva siempre que la condición del bucle sea verdadera no se incluyó en una prueba de interferencia. Muestran dos formas de rectificar este error.
Considere la afirmación:
{x=0}
cobegin await true then x: = x+1
// await true then x: = x+2
coend
{x=3}
El esquema de prueba para ello:
{x=0}
S: cobegin {x=0} {x=0 ∨ x=2} S1: espera verdadero entonces x : = x+1 {Q1: x=1 ∨ x=3} // {x=0} {x=0 ∨ x=1} S2: espera verdadero entonces x : = x+2 {Q2: x=2 ∨ x=3} coend
{(x=1 ∨ x=3) ∧ (x=2 ∨ x=3)}
{x=3}
Demostrar que S1 no interfiere con la prueba de S2 requiere demostrar dos tripletas de Hoare:
(1) {(x=0 ∨ x=2) ∧ (x=0 ∨ x=1} S1 {x=0 ∨ x=1}
(2) {(x=0 ∨ x=2) ∧ (x= 2 ∨ x=3} S1 {x=2 ∨ x=3}
La condición previa de (1) se reduce a x=0 y la condición previa de (2) se reduce a x=2 . A partir de esto, es fácil ver que estas tripletas de Hoare se cumplen. Se requieren dos tripletas de Hoare similares para demostrar que S2 no interfiere con la prueba de S1 .
Supongamos que S1 se cambia de la declaración de espera a la asignación x: = x+1 . Entonces el esquema de prueba no satisface los requisitos, porque la asignación contiene dos apariciones de la variable compartida x . De hecho, el valor de x después de la ejecución de la declaración cobegin podría ser 2 o 3.
Supongamos que S1 se cambia a la declaración de espera await true y luego x: = x+2 , por lo que es lo mismo que S2 . Después de la ejecución de S , x debe ser 4. Para probar esto, debido a que las dos asignaciones son iguales, se necesitan dos variables auxiliares, una para indicar si S1 se ha ejecutado; el otro, si se ha ejecutado S2 . Dejamos el cambio en el esquema de prueba al lector.
A. Encuentrapos . Escriba un programa que encuentre el primer elemento positivo de una matriz (si lo hay). Un proceso verifica todos los elementos de la matriz en posiciones pares de la matriz y finaliza cuando encuentra un valor positivo o cuando no se encuentra ninguno. De manera similar, el otro proceso verifica los elementos de la matriz en posiciones impares de la matriz. Por tanto, este ejemplo trata de bucles while . Tampoco tiene declaraciones de espera .
Este ejemplo proviene de Barry K. Rosen. [14] La solución en Owicki-Gries, [2] completa con programa, esquema de prueba y discusión sobre la libertad de interferencia, ocupa menos de dos páginas. La libertad de interferencia es bastante fácil de comprobar, ya que sólo hay una variable compartida. Por el contrario, el artículo de Rosen [14] utiliza Findpos como único ejemplo en este documento de 24 páginas.
Un resumen de ambos procesos en un entorno general:
productor de cobegin : ... espera entrada-salida < N y luego omite ; agregar: b[en mod N]:= siguiente valor; marca: en: = en+1; ... // consumidor: ... espera entrada-salida > 0 y luego omite ; eliminar: este valor:= b[out mod N]; marcado: fuera: = fuera+1;
coend
...
B. Problema del consumidor/productor del buffer acotado . Un proceso productor genera valores y los coloca en un búfer acotado b de tamaño N ; un proceso de consumo los elimina. Proceden a tipos variables. El productor debe esperar si el buffer b está lleno; el consumidor debe esperar si el buffer b está vacío. En Owicki-Gries [2] se muestra una solución en un entorno general; luego se incrusta en un programa que copia una matriz c[1..M] en una matriz d[1..M] .
Este ejemplo muestra un principio para reducir las comprobaciones de interferencia al mínimo: coloque la mayor cantidad posible en una afirmación que sea invariablemente cierta en todos lados en ambos procesos. En este caso, la aserción es la definición del búfer limitado y los límites de las variables que indican cuántos valores se han agregado y eliminado del búfer. Además del propio búfer b , dos variables compartidas registran el número de valores agregados al búfer y el número de valores eliminados del búfer.
C. Implementación de semáforos . En su artículo sobre EL sistema de multiprogramación, [4] Dijkstra presenta el semáforo sem como una primitiva de sincronización: sem es una variable entera a la que se puede hacer referencia sólo de dos maneras, como se muestra a continuación; cada una es una operación indivisible:
1. P(sem) : Disminuye sem en 1. Si ahora sem <0 , suspende el proceso y colócalo en una lista de procesos suspendidos asociados con sem .
2. V(sem) : aumenta sem en 1. Si ahora sem ≤ 0 , elimina uno de los procesos de la lista de procesos suspendidos asociados con sem , para que su progreso dinámico vuelva a ser permisible.
La implementación de P y V usando declaraciones de espera es:
P(sem): espera verdadero y luego comienza sem: = sem-1; si sem < 0 entonces w[este proceso]: = verdadero fin ; espere ¬w[este proceso] y luego salte
V(sem): espera verdadero y luego comienza sem: = sem+1; si sem ≤ 0 entonces comience a elegir p tal que w[ p ]; w[ p ]: = fin falso fin
Aquí, w es una serie de procesos que están en espera porque han sido suspendidos; Inicialmente, w[p] = false para cada proceso p . Se podría cambiar la implementación para activar siempre el proceso suspendido más largo.
D. Recolección de basura sobre la marcha . En la Escuela de Verano de Marktoberdorf de 1975 , Dijkstra habló de un recolector de basura sobre la marcha como un ejercicio para comprender el paralelismo. La estructura de datos utilizada en una implementación convencional de LISP es un gráfico dirigido en el que cada nodo tiene como máximo dos bordes salientes, cualquiera de los cuales puede faltar: un borde izquierdo saliente y un borde derecho saliente. Se debe poder acceder a todos los nodos del gráfico desde una raíz conocida. Cambiar un nodo puede dar como resultado nodos inalcanzables, que ya no se pueden usar y se denominan basura . Un recolector de basura sobre la marcha tiene dos procesos: el programa en sí y un recolector de basura, cuya tarea es identificar los nodos de basura y colocarlos en una lista libre para que puedan usarse nuevamente.
Gries consideró que la libertad de interferencia podría usarse para demostrar que el recolector de basura sobre la marcha tenía razón. Con la ayuda de Dijkstra y Hoare, pudo hacer una presentación al final de la Escuela de Verano, que resultó en un artículo en CACM. [15]
E. Verificación de solución de lectores/escritores con semáforos . Courtois et al [16] utilizan semáforos para dar dos versiones del problema lectores/escritores, sin pruebas. Las operaciones de escritura bloquean tanto las lecturas como las escrituras, pero las operaciones de lectura pueden ocurrir en paralelo. Owicki [17] proporciona una prueba.
El algoritmo de F. Peterson , una solución al problema de exclusión mutua de dos procesos, fue publicado por Peterson en un artículo de dos páginas. [18] Schneider y Andrews proporcionan una prueba de corrección. [19]
La siguiente imagen, de Ilya Sergey, muestra el flujo de ideas que se han implementado en lógicas que tratan con la concurrencia. En la raíz está la libertad de interferencia. El archivo CSL-Family-Tree (PDF)contiene referencias. A continuación, resumimos los principales avances.
{{cite journal}}: Mantenimiento CS1: varios nombres: lista de autores ( enlace )