Libertad de interferencia

En informática , la ausencia de interferencias 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 corrección de programas secuenciales. En su tesis doctoral ^{[ 1 ]} (y en los artículos derivados de ella ^{[ 2 ] [ 3 ]} ), bajo la dirección de David Gries , Susan Owicki extendió este trabajo para aplicarlo a programas concurrentes.

La programación concurrente se utilizaba desde mediados de la década de 1960 para codificar sistemas operativos como conjuntos de procesos concurrentes (véase, en particular, Dijkstra ^{[ 4 ]} ), pero no existía un mecanismo formal para demostrar su corrección. Razonar sobre las secuencias de ejecución intercaladas de los procesos individuales era difícil, propenso a errores y no escalable. La ausencia de interferencia se aplica a las pruebas en lugar de a las secuencias de ejecución; se demuestra que la ejecución de un proceso no puede interferir con la prueba de corrección de otro proceso.

Se ha demostrado la corrección de una variedad de programas concurrentes complejos utilizando la ausencia de interferencia, y esta proporciona la base para gran parte del trabajo posterior sobre el desarrollo de programas concurrentes con variables compartidas y su demostración de corrección. El artículo de Owicki y Gries, « Una técnica de prueba axiomática para programas paralelos » ^{[ 2 ],} recibió el premio ACM de 1977 al mejor artículo en 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 el de Owicki-Gries, quizás porque usó diagramas de flujo en lugar del texto de construcciones de programación como la instrucció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 ]} Esencialmente, todo el trabajo posterior en esta área usa texto y no diagramas de flujo. Otra diferencia se menciona más adelante en la sección sobre Variables auxiliares .

Edsger W. Dijkstra introdujo el principio de no interferencia en EWD 117, "La programación considerada como una actividad humana", escrito alrededor de 1965. ^{[ 10 ]} Este principio establece que: La corrección del conjunto puede establecerse teniendo en cuenta únicamente las especificaciones externas (abreviadas como especificaciones en todo el texto) de las partes, y no su construcción interna. Dijkstra describió los pasos generales para utilizar este principio:

1. Proporcione una especificación completa de cada pieza individual.
2. Compruebe que el problema se haya resuelto por completo cuando estén disponibles las partes del programa que cumplan con sus especificaciones.
3. Construya las piezas individuales de acuerdo con sus especificaciones, pero de forma independiente entre sí y del contexto en el que se utilizarán.

Dio varios ejemplos de este principio fuera del ámbito de la programación. Sin embargo, su aplicación en la programación es fundamental. Por ejemplo, un programador que utiliza un método (subrutina, función, etc.) debe basarse ú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 la ejecución de Si en un estado en el que la precondición pre-Si es verdadera termina, entonces al terminar, la postcondició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 definen mediante sus precondiciones y postcondiciones, y asumimos que se proporcionan implementaciones de S1 y S2 que satisfacen dichas especificaciones. Sin embargo, al ejecutar sus implementaciones en paralelo, dado que comparten variables, puede producirse una condición de carrera : un proceso modifica una variable compartida a un valor que no se anticipa en la prueba del otro proceso, por lo que este último no funciona como se espera.

Por lo 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 satisfacen la libertad de interferencia, entonces su ejecución paralela funcionará según lo previsto. Dijkstra consideró 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 solo dos procesos concurrentes, aunque Owicki-Gries ^{[ 2 ] [ 3 ]} permite más.

Owicki-Gries ^{[ 2 ] [ 3 ]} introdujo el esquema de prueba para una tripleta de Hoare {P}S{Q }. Contiene todos los detalles necesarios para una prueba de corrección de {P}S{Q } utilizando los axiomas y reglas de inferencia de la lógica de Hoare . (Este trabajo utiliza la instrucción de asignación x: = e , las instrucciones if-then e if-then-else y el bucle while ). Hoare aludió a los esquemas de prueba en sus primeros trabajos; para la ausencia de interferencia, era necesario formalizarlos.

Un esquema de demostración para {P}S{Q } comienza con la precondición P y termina con la postcondición Q. Dos afirmaciones entre llaves { y } que aparecen una al lado de la otra indican que la primera debe implicar la segunda.

Ejemplo: Esquema de demostración para {P} S {Q } donde S es: x : = a; si e entonces S1 sino S2

{P } {P1[x/a] } x : = a; {P1 } si e entonces {P1 ∧ e } S1 {Q1 } si no {P1 ∧ ¬ e } S2 {Q1 } {Q1 } {Q }

Debe cumplirse P ⇒ P1[x/a] , donde P1[x/a] representa P1 con cada aparición de x reemplazada por a . (En este ejemplo, S1 y S2 son instrucciones básicas, como una instrucción de asignación, skip o await ).

Cada enunciado T en el esquema de la demostración está precedido por una precondición pre-T y seguido por una postcondición post-T , y {pre-T}T{post-T } debe ser demostrable utilizando algún axioma o regla de inferencia de la lógica de Hoare. Por lo tanto, el esquema de la demostración contiene toda la información necesaria para probar que {P}S{Q } es correcto.

Ahora consideremos 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 a como máximo a una variable y que puede ser modificada 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 sentencias 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 S2 la modifica . El valor que S1 recibe para y debe ser el valor anterior o posterior a la modificación realizada por S2 , y no un valor intermedio.

Definición de libre de interferencias

La importante innovación de Owicki-Gries fue definir qué significa que una declaración T no interfiera con la prueba de {P}S{Q }. Si la ejecución de T no puede refutar ninguna afirmación dada en el esquema de prueba de {P}S { Q }, entonces esa prueba sigue siendo válida incluso frente a la ejecución concurrente de S y T.

Definición . La afirmación T con la 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 instrucción dentro de S pero no dentro de una instrucción await (ver sección posterior). Entonces {pre-S' ∧ pre-T} T {pre-S' }.

Lee la última tripleta de Hoare de esta manera: 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 } no interfieren si se cumple lo siguiente. Sea T una instrucción await o de asignación (que no aparece en un await ) 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 instrucciones para gestionar la concurrencia. La ejecución de la instrucción ` cobegin S1 // S2 coend` ejecuta S1 y S2 en paralelo. Finaliza cuando S1 y S2 han terminado.

La ejecución de la instrucción ` await B then S` se retrasa hasta que la condición B sea verdadera. Entonces, la instrucción S se ejecuta como una acción indivisible; la evaluación de B forma parte de esa acción indivisible. Si dos procesos están esperando la misma condición B , cuando esta se cumple, uno de ellos continúa esperando mientras el otro continúa.

La instrucción `await` 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 se expresan las operaciones de semáforo como ` await` , y luego se aplican las técnicas descritas aquí.

Las reglas de inferencia para await y cobegin son:

esperar ⁠ {P ∧ B} S {Q} / {P} esperar B entonces S {Q} ⁠

cobegin ⁠ {P1} S1 {Q1}, {P2} S2 {Q2} sin interferencias / {P1 ∧ P2} cobegin S1//S2 coend {Q1 ∧ Q2} ⁠

Una variable auxiliar no aparece en el programa, sino que se introduce en la prueba de corrección para simplificar el razonamiento, o incluso para posibilitarlo. Las variables auxiliares se utilizan únicamente en asignaciones a otras 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 programa o para registrar el historial de un cálculo.

Definición . Sea AV un conjunto de variables que aparecen en S' solo en asignaciones x: = E , donde x está en AV . Entonces AV es un conjunto de variables auxiliares para S' .

Dado que un conjunto AV de variables auxiliares se utiliza únicamente 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 de AV :

⁠ {P} S' {Q} / {P} S {Q} ⁠

AV es un conjunto de variables auxiliares para S' . Las variables en AV no aparecen en P ni en Q. S se obtiene a partir 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 las aserciones recursivas , es decir, aserciones efectivamente computables . Demuestra que todas las aserciones en los esquemas de prueba pueden ser recursivas, pero que esto deja de ser así si las variables auxiliares se utilizan únicamente como contadores de programa y no para registrar historiales de computación. Lamport, en su trabajo similar ^{[ 7 ]} , utiliza aserciones 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 variable de historial. Esto indica que los enfoques de Owicki-Gries y Lamport no son equivalentes cuando se restringen a aserciones recursivas.

Owicki-Gries ^{[ 2 ] [ 3 ]} trata principalmente de corrección parcial: {P} S {Q } significa: Si S ejecutado en un estado en el que P es verdadero termina, entonces Q es verdadero del estado al terminar. Sin embargo, Owicki-Gries también proporciona algunas técnicas prácticas que utilizan información obtenida de una prueba de corrección parcial para derivar otras propiedades de corrección, incluyendo la ausencia de interbloqueo, terminación del programa y exclusión mutua.

Un programa se encuentra en estado de interbloqueo si todos los procesos que no han finalizado están ejecutando instrucciones `await` y ninguno puede continuar porque sus condiciones de `await` son falsas. El algoritmo de Owicki-Gries proporciona condiciones bajo las cuales no puede producirse un interbloqueo.

Owicki-Gries presenta una regla de inferencia para la corrección total del bucle while . Esta regla utiliza una función límite que disminuye con cada iteración y es positiva mientras la condición del bucle sea verdadera. Apt et al . ^{[ 13 ]} demuestran que esta nueva regla de inferencia no satisface la ausencia de interferencia. El hecho de que la función límite sea positiva mientras la condición del bucle sea verdadera no se incluyó en una prueba de interferencia. Presentan dos maneras de corregir este error.

Considere la instrucción: {x=0} cobegin await true then x: = x+1 // await true then x: = x+2 coend {x=3}              

El esquema de demostración correspondiente:

{x=0} S: cobegin {x=0} {x=0 ∨ x=2} S1: await true then x : = x+1 {Q1: x=1 ∨ x=3} // {x=0} {x=0 ∨ x=1} S2: await true then x : = x+2 {Q2: x=2 ∨ x=3} coend {(x=1 ∨ x=3) ∧ (x=2 ∨ x=3)} {x=3}

Para demostrar que S1 no interfiere con la demostración de S2, es necesario demostrar dos triples 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 ternas de Hoare se cumplen. Se requieren dos ternas de Hoare similares para demostrar que S2 no interfiere con la demostración de S1 .

Supongamos que S1 cambia de la instrucción await a la asignación x: = x+1 . Entonces, el esquema de la prueba no cumple con los requisitos, porque la asignación contiene dos ocurrencias de la variable compartida x . De hecho, el valor de x después de la ejecución de la instrucción cobegin podría ser 2 o 3.

Supongamos que S1 se cambia a la instrucción ` await true`, entonces x: = x+2 , por lo que es lo mismo que S2 . Después de la ejecución de S , x debería ser 4. Para demostrar esto, dado que las dos asignaciones son iguales, se necesitan dos variables auxiliares: una para indicar si S1 se ha ejecutado y la otra, si S2 se ha ejecutado. Dejamos el cambio en el esquema de la demostración al lector.

A. Findpos . Escribe un programa que encuentre el primer elemento positivo de un arreglo (si existe). Un proceso revisa todos los elementos del arreglo en las posiciones pares y finaliza cuando encuentra un valor positivo o cuando no encuentra ninguno. De manera similar, el otro proceso revisa los elementos del arreglo en las posiciones impares. Por lo tanto, este ejemplo utiliza bucles while y no contiene instrucciones await .

Este ejemplo proviene de Barry K. Rosen. ^{[ 14 ]} La solución en Owicki-Gries, ^{[ 2 ]} completa con programa, esquema de demostración y discusión sobre la ausencia de interferencia, ocupa menos de dos páginas. La ausencia de interferencia es bastante fácil de comprobar, ya que solo hay una variable compartida. En contraste, el artículo de Rosen ^{[ 14 ]} utiliza Findpos como el único ejemplo continuo en este documento de 24 páginas.

Un resumen de ambos procesos en un entorno general:

cobegin productor: ... esperar entrada-salida < N entonces saltar ; agregar: b[entrada mod N]:= siguiente valor; marcar: entrada: = entrada+1; ... // consumidor: ... esperar entrada-salida > 0 entonces saltar ; eliminar: este valor:= b[salida mod N]; marcar salida: salida: = salida+1; . coend ...

B. Problema del consumidor/productor con búfer limitado . Un proceso productor genera valores y los coloca en un búfer limitado b de tamaño N ; un proceso consumidor los extrae. Proceden a velocidades variables. El productor debe esperar si el búfer b está lleno; el consumidor debe esperar si el búfer b está vacío. En Owicki-Gries, ^{[ 2 ]} se muestra una solución en un entorno general; luego se integra en un programa que copia un arreglo c[1..M] en un arreglo d[1..M] .

Este ejemplo ilustra un principio para minimizar las comprobaciones de interferencia: concentrar la mayor cantidad de información posible en una aserción que sea invariablemente verdadera en ambos procesos. En este caso, la aserción define el búfer acotado y los límites de las variables que indican la cantidad de valores agregados y eliminados del búfer. Además del propio búfer b , dos variables compartidas registran la cantidad de valores agregados y eliminados del búfer.

C. Implementación de semáforos . En su artículo sobre el sistema de multiprogramación THE , ^{[ 4 ]} Dijkstra introduce el semáforo sem como una primitiva de sincronización: sem es una variable entera a la que se puede hacer referencia de solo dos maneras, como se muestra a continuación; cada una es una operación indivisible:

1. P(sem) : Disminuir sem en 1. Si ahora sem < 0 , suspender el proceso y agregarlo a una lista de procesos suspendidos asociados con sem .

2. V(sem) : Incrementa 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 utilizando sentencias await es:

P(sem): esperar verdadero entonces comenzar sem: = sem-1; si sem < 0 entonces w[este proceso]: = verdadero fin ; esperar ¬w[este proceso] entonces saltarV(sem): esperar verdadero entonces comenzar sem: = sem+1; si sem ≤ 0 entonces comenzar elegir p tal que w[ p ]; w[ p ]: = falso fin fin

Aquí, w es un conjunto de procesos que están en espera porque han sido suspendidos; inicialmente, w[p] = falso para cada proceso p . Se podría modificar la implementación para que siempre se despierte al proceso suspendido que lleve más tiempo.

D. Recolección de basura en tiempo real . En la Escuela de Verano de Marktoberdorf de 1975 , Dijkstra habló sobre un recolector de basura en tiempo real como un ejercicio para comprender el paralelismo. La estructura de datos utilizada en una implementación convencional de LISP es un grafo dirigido en el que cada nodo tiene como máximo dos aristas salientes, cualquiera de las cuales puede faltar: una arista saliente izquierda y una arista saliente derecha. Todos los nodos del grafo deben ser alcanzables desde una raíz conocida. Cambiar un nodo puede resultar en nodos inalcanzables, que ya no se pueden usar y se denominan basura . Un recolector de basura en tiempo real tiene dos procesos: el programa en sí y un recolector de basura, cuya tarea es identificar los nodos basura y colocarlos en una lista de nodos libres para que puedan usarse nuevamente.

Gries creía que la ausencia de interferencias podía utilizarse para demostrar la validez del recolector de basura en tiempo real. Con la ayuda de Dijkstra y Hoare, pudo dar una presentación al final de la Escuela de Verano, que dio lugar a un artículo en CACM. ^{[ 15 ]}

E. Verificación de la solución de lectores/escritores con semáforos . Courtois et al. ^{[ 16 ]} utilizan semáforos para dar dos versiones del problema de lectores/escritores, sin demostración. Las operaciones de escritura bloquean tanto las lecturas como las escrituras, pero las operaciones de lectura pueden ocurrir en paralelo. Owicki ^{[ 17 ]} proporciona una demostración.

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 imagen que aparece a continuación, de Ilya Sergey, muestra el flujo de ideas que se han implementado en lógicas que abordan la concurrencia. En la raíz se encuentra la ausencia de interferencias. El archivo es CSL-Family-Tree (PDF).Contiene referencias. A continuación, resumimos los principales avances.

• Confianza-Garantía . 1981. La libertad de interferencia no es composicional. Cliff Jones ^{[ 20 ] [ 21 ]} recupera la composicionalidad al abstraer la interferencia en dos nuevos predicados en una especificación: una condición de confianza registra qué interferencia debe poder tolerar un hilo y una condición de garantía establece un límite superior a la interferencia que el hilo puede infligir a sus hilos hermanos. Xu et al. ^{[ 22 ]} observan que Confianza-Garantía es una reformulación de la libertad de interferencia; revelando la conexión entre estos dos métodos, dicen, ofrece una comprensión profunda sobre la verificación de programas de variables compartidas.
• CSL . 2004. La lógica de separación admite el razonamiento local, por el cual las especificaciones y pruebas de un componente de programa mencionan solo la porción de memoria utilizada por el componente. La lógica de separación concurrente (CSL) fue propuesta originalmente por Peter O'Hearn , ^{[ 23 ] [ 24 ]} Citamos de: ^{[ 23 ]} "el método de Owicki-Gries ^{[ 2 ]} implica una verificación explícita de la no interferencia entre componentes de programa, mientras que nuestro sistema descarta la interferencia de manera implícita, por la naturaleza de la forma en que se construyen las pruebas."
• Derivación de programas concurrentes . 2005-2007. Feijen y van Gasteren ^{[ 25 ]} muestran cómo usar Owicki-Gries para diseñar programas concurrentes, pero la falta de una teoría del progreso significa que los diseños están impulsados ​​únicamente por requisitos de seguridad . Dongol, Goldson, Mooij y Hayes han extendido este trabajo para incluir una "lógica del progreso" basada en el lenguaje Unity de Chandy y Misra , moldeado para ajustarse a un modelo de programación secuencial . Dongol y Goldson ^{[ 26 ]} describen su lógica del progreso. Goldson y Dongol ^{[ 27 ]} muestran cómo se usa esta lógica para mejorar el proceso de diseño de programas, usando el algoritmo de Dekker para dos procesos como ejemplo. Dongol y Mooij ^{[ 28 ]} presentan más técnicas para derivar programas, usando el algoritmo de exclusión mutua de Peterson como un ejemplo. Dongol y Mooij ^{[ 29 ]} muestran cómo reducir la sobrecarga computacional en las demostraciones y derivaciones formales y derivan nuevamente el algoritmo de Dekker, lo que da lugar a algunas variantes nuevas y más simples del algoritmo. Mooij ^{[ 30 ]} estudia las reglas de cálculo para la relación de conducción de Unity . Finalmente, Dongol y Hayes ^{[ 31 ]} proporcionan una base teórica y demuestran la solidez de la lógica de procesos.
• OGRA . 2015. Lahav y Vafeiadis refuerzan la comprobación de ausencia de interferencias para producir (citamos del resumen) "OGRA, una lógica de programa sólida para razonar sobre programas en el fragmento de liberación-adquisición del modelo de memoria C11". Proporcionan varios ejemplos de su uso, incluyendo una implementación de las primitivas de sincronización RCU. ^{[ 32 ]}
• Programación cuántica . 2018. Ying et al . ^{[ 33 ]} extienden la libertad de interferencia a la programación cuántica. Entre las dificultades que enfrentan se encuentra el no determinismo entrelazado: el no determinismo que involucra mediciones cuánticas y el no determinismo introducido por el paralelismo que ocurre simultáneamente. Los autores verifican formalmente el algoritmo cuántico paralelo de Bravyi-Gosset-König para resolver un problema de álgebra lineal , lo que, según afirman, proporciona por primera vez una prueba incondicional de una ventaja cuántica computacional.
• POG . 2020. Raad et al presentan POG (Persistent Owicki-Gries), la primera lógica de programa para razonar sobre tecnologías de memoria no volátil , específicamente Intel-x86. ^{[ 34 ]}

• Sobre un método de multiprogramación , 1999. ^{[ 25 ]} Van Gasteren y Feijen analizan el desarrollo formal de programas concurrentes basándose enteramente en la idea de libertad de interferencia.
• En Current Programming , 1997. ^{[ 35 ]} Schneider utiliza la ausencia de interferencias como herramienta principal para desarrollar y demostrar programas concurrentes. Se establece una conexión con la lógica temporal , lo que permite demostrar propiedades arbitrarias de seguridad y vivacidad. Los predicados de control eliminan la necesidad de variables auxiliares para razonar sobre los contadores del programa.
• Verificación de programas secuenciales y concurrentes , 1991, ^{[ 36 ]} 2009. ^{[ 37 ]} Este primer texto que cubre la verificación de programas concurrentes estructurados, de Apt et al ., ha pasado por varias ediciones a lo largo de varias décadas.
• Verificación de concurrencia: Introducción a los métodos composicionales y no composicionales , 2112. ^{[ 38 ]} De Roever et al. proporcionan una introducción sistemática y completa a los métodos de prueba composicionales y no composicionales para la verificación basada en estados de programas concurrentes.

• 1999: Nipkow y Nieto presentan la primera formalización de la libertad de interferencia y su versión compositiva, el método de confianza-garantía, en un demostrador de teoremas: Isabelle/HOL. ^{[ 39 ] [ 40 ]}
• 2005: La tesis doctoral de Ábrahám proporciona un método para demostrar la corrección de programas Java multihilo en tres pasos: (1) Anotar el programa para generar un esquema de demostración, (2) Utilizar su herramienta Verger para crear automáticamente condiciones de verificación y (3) Utilizar el demostrador de teoremas PVS para demostrar las condiciones de verificación de forma interactiva. ^{[ 41 ] [ 42 ]}
• 2017: Denissen ^{[ 43 ]} informa sobre una implementación de Owicki-Gries en el lenguaje de programación Dafny , que permite la verificación . ^{[ 44 ]} Denissen destaca la facilidad de uso de Dafny y su extensión, lo que lo hace sumamente adecuado para enseñar a los estudiantes sobre la libertad de interferencia. Su simplicidad e intuición compensan la desventaja de no ser composicional. Enumera una veintena de instituciones que imparten enseñanza sobre la libertad de interferencia.
• 2017: Amani et al combinan los enfoques de Hoare-Parallel, una formalización de Owicki-Gries en Isabelle/HOL para un lenguaje while simple, y SIMPL, un lenguaje genérico integrado en Isabelle/HOL, para permitir el razonamiento formal en programas C. ^{[ 45 ]}
• 2022: Dalvandi et al. presentan el primer entorno de verificación deductiva en Isabelle/HOL para programas de memoria débil tipo C11, basándose en la codificación de Nipkow y Nieto de Owicki–Gries en el demostrador de teoremas Isabelle. ^{[ 46 ]}
• 2022: Esta página web ^{[ 47 ]} describe el verificador Civl para programas concurrentes y proporciona instrucciones para su instalación en su ordenador. Está construido sobre Boogie, un verificador para programas secuenciales. Kragl et al. ^{[ 48 ]} describen cómo se logra la ausencia de interferencias en Civl mediante su nuevo lenguaje de especificación, los invariantes yield . También se pueden usar especificaciones en el estilo rely-guarantee. Civl ofrece una combinación de tipado lineal y lógica que permite un razonamiento económico y local sobre la disyunción (como la lógica de separación). Civl es el primer sistema que ofrece razonamiento de refinamiento en programas concurrentes estructurados.
• 2022. Esen y Rümmer desarrollaron TRICERA, ^{[ 49 ]} una herramienta de verificación automatizada de código abierto para programas en C. Se basa en el concepto de cláusulas de Horn restringidas y maneja programas que operan en el montón utilizando una teoría de montones. Hay una interfaz web disponible para probarla en línea. Para manejar la concurrencia, TRICERA utiliza una variante de las reglas de prueba de Owicki-Gries, con variables explícitas añadidas para representar el tiempo y los relojes.