Lógica de separación

Lógica de separación, lógica de separación ( lógica de separación en inglés ) - sistema formal, lógica subestructural, aplicable a la verificación de programas que contienen estructuras de datos mutables y punteros , una extensión de la lógica de Hoare . Diseñado por John Reynolds , Peter O'Hearn , Samin Ishtiaq y Hongseok Yang [ 1 ] [ 2 ] [ 3 ] [4] basado en el trabajo de Rod Burstall [ 5 ] . El lenguaje de aserciones de la lógica de partición es un caso especial de la lógica de implicaciones agrupadas [ 6 ] .

Una evolución de la lógica de partición para computación paralela con memoria compartida es la lógica de partición paralela , desarrollada por O'Hearn y Stephen D. Brookes .

Las tecnologías basadas en la lógica de la separación permiten desarrollar sistemas para la verificación de grandes proyectos de software [7] .

Requisitos previos para la creación

La lógica de Hoare tiene una serie de limitaciones, ya que opera solo en variables mutables y no admite procedimientos ni código de primera clase . Sin embargo, la mayor limitación es la falta de soporte de puntero , que es más relevante para la especificación de programa imperativo . En el caso de utilizar punteros y el montón , las variables mutables se pueden abandonar asignando un valor de puntero a las variables locales solo una vez [8] .

En 2000-2002, John Reynolds y Peter O'Hearn idearon una extensión de la lógica de Hoare, la lógica de la división. La idea original era simplificar el razonamiento sobre programas imperativos de bajo nivel con una estructura de datos mutable común [9] . El término en sí está asociado con la idea principal de esta lógica: la descripción de la división del almacenamiento ( almacenamiento en inglés ) en componentes que no se superponen. El término se utiliza tanto en relación con el cálculo de predicados , ampliado por el operador de división , como con el resultado de una ampliación de la lógica de Hoare [1] .

Descripción

Una característica clave de la lógica de la separación es la posibilidad de un razonamiento local (razonamiento local) debido a la presencia en las declaraciones de conectores espaciales ( esp. conectores espaciales ) entre partes del montón [10] .

La lógica le permite trabajar con sentencias de la forma , donde: ${\ estilo de visualización s, h \ modelos P}$

$s$ - memoria (por ejemplo, en forma de pila [1] ), un mapeo funcional parcial finito de variables a enteros ,
$h$ es un montón, un mapeo funcional parcial finito de enteros a enteros, y
$PAGS$ - una declaración sobre la memoria y el montón, es decir, sobre el estado del programa [12] .

Para superar las engorrosas descripciones de prohibiciones sobre el uso de la misma dirección por diferentes objetos, se ha introducido una nueva operación lógica: una conjunción disjunta , denotada por (o [13] ) y afirmando que cada una de las condiciones y se cumplen en su parte del montón (almacenamiento direccionado) [9] [14] . Es decir, verdadero para un montón si hay dos partes de este montón y para las cuales [15] es verdadero : $P\ *\ Q$ $P\ \tierra \!*\ Q$ $PAGS$ $q$ $P\ *\ Q$ $h$ $h_1$ $h_2$

Las regiones y no se cruzan; $h_1$ $h_2$
$h$ es la unión de y ; $h_1$ $h_2$
$PAGS$ verdadero para todas las direcciones desde ; $h_1$
$q$ true para todas las direcciones desde . $h_2$

Arriba, y se entienden como funciones parciales que dan valores correspondientes a una dirección en el montón. $h_1$ $h_2$

Para afirmar que el montón está vacío, se introduce un predicado (en este caso, obviamente, ) y para designar un puntero - . Por ejemplo, en el siguiente, que es uno de los axiomas, el triple de Hoare ${\ Displaystyle emp}$ $P\ *\ emp\ \Leftrightarrow \P$ $e\mapsto x$

{\displaystyle \{E\mapsto -\}\ [E]:=F\ \{E\mapsto F\))

la condición previa es la celda de memoria no utilizada que, como resultado de la operación de asignación, apunta a F , que se establece en la condición posterior [12] .

La clave del razonamiento local es la regla del marco introducida por O'Hearn [ 1 ] :

\frac{\{P\}\ C\ \{Q\}}{\{P \ast R\}\ C\ \{Q \ast R\}}~\mathsf{mod}(C) \cap \ matemáticasf{fv}(R) =\emptyset

en el que ninguna variable libre ( ing. free v ariable ) se cambia ( ing. mod ified ) bajo la influencia del comando . Con esta regla, puede agregar predicados arbitrarios sobre las variables y partes del montón que no modifica el comando . Al mismo tiempo, O'Hearn llamó a la cantidad de montón ocupado por el comando el término inglés. huella ("huella"). El propósito de la regla del marco es expandir el argumento de una descripción más local del comando a una descripción más global del comando adjunto, el comando con la huella más grande [1] . $R$ $C$ $C$

Habiendo establecido que la lógica de la separación es un ejemplo de la lógica de las implicaciones de la gavilla, Yang e Ishtiak introdujeron la implicación de separación ( implicación de separación en inglés [1] , varita mágica en inglés ). La designación dice que si un montón se extendió por un montón que no se interseca para lo cual es true , entonces para el montón resultante será true [7] . $P-\!\!\!\ast\, Q$ $PAGS$ $q$

La semántica de los conectores lógicos (conjunción separadora e implicación separadora) implica una estructura de montón monoide [7] .

Lógica de separación paralela (CSL)

La lógica de separación concurrente ( CSL ) es una versión de lógica aplicable para la verificación de algoritmos paralelos con memoria compartida. Originalmente propuesto por Peter O'Hearn. Utiliza la siguiente regla [16]

{\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\)) {\{P_{1}*P_{2}\}\;C_{1}\parallel C_{2}\;\{Q_{1}*Q_{2}\))))

lo que le permite sacar conclusiones en presencia de hilos de ejecución independientes que acceden a una tienda separada. Las reglas de prueba de O'Hearn adaptaron el enfoque inicial de Tony Hoare sobre la concurrencia [17] reemplazando el uso de restricciones de alcance para hacer cumplir la partición con razonamiento en la lógica de partición. Además de extender el enfoque de Hoare a los punteros de montón, O'Hearn demostró que la lógica de partición paralela puede rastrear dinámicamente la transferencia de propiedad de áreas de montón entre procesos. Por lo tanto, los ejemplos de su artículo incluyen un búfer de paso de puntero y un administrador de memoria .

El razonamiento local también puede entenderse en términos de transferencia de propiedad . Es más fácil considerar la transferencia de propiedad utilizando las reglas del monitor Hoare como ejemplo (puede ver que la lógica de separación también es adecuada para sistemas distribuidos ). Para ingresar una sección crítica , se usa una conjunción de separación con , donde es el recurso invariante r . Al salir de la sección crítica, la conclusión lógica sigue en la dirección opuesta [18] : $yo_r$ $yo_r$

\frac{\{P \ast I_r\}\ C\ \{Q \ast I_r\}}{\{P\}\ \mathsf{con}\ r\ \mathsf{hacer}\ C\ \{Q\ }}

Por analogía, también podemos considerar el proceso de procesamiento por parte de un proceso de un mensaje enviado por otro proceso con recursos delegados a este proceso, determinados por huellas dactilares [18] .

Stephen D. Brookes introdujo por primera vez un modelo para una lógica de partición paralela en un artículo adjunto al artículo de O'Hearn [19] . La corrección ( en inglés solidness ) de la lógica era un problema difícil. En particular, el contraejemplo de John Reynolds mostró el fracaso de una versión anterior e inédita de la lógica. El punto planteado por el ejemplo de Reynolds se describe brevemente en el artículo de O'Hearn y más detalladamente en el de Brooks.

O'Hearn y Brooks son co-receptores del Premio Gödel 2016 por la invención de la lógica de partición paralela [20] .

Aplicaciones e implementaciones

La lógica de separación ha encontrado aplicación en verificadores automáticos e interactivos de software escritos en un estilo imperativo y orientado a objetos . Para esto, se desarrollaron adiciones apropiadas a las herramientas de verificación existentes, por ejemplo, tales como:

Ynot [21] es una biblioteca para verificar programas imperativos para Coq .
Predator [22] es un analizador de programas basado en lógica dividida para analizar programas que contienen listas dinámicas [23] .

Otros sistemas que utilizan lógica dividida: Smallfoot, Space Invader, THOR, SLAyer, HIP, jStar, Xisa, VeriFast, Infer, SeLoger, SLP. Sin embargo, a partir de 2014, no hay probadores de teoremas prácticos que implementen la lógica completa de partición, es decir, que incluyan una implicación de partición [7] .

De acuerdo con la naturaleza del uso del sistema, se puede dividir de la siguiente manera [24] :

El usuario escribe manualmente tanto la especificación como la prueba usando tácticas: probadores de teoremas interactivos Coq, HOL4, Isabelle/HOL.
El usuario escribe la especificación y los invariantes de bucle : herramientas de verificación independientes Smallfoot, HIP, Verifast, Jstar.
El usuario escribe solo la especificación (o incluso no escribe nada): herramientas de análisis de forma ( eng . análisis de forma ) Space Invader, THOR, Xisa, SLAyer.

Notas

↑ 1 2 3 4 5 6 Reynolds, 2002 .
↑ Razonamiento intuicionista sobre la estructura de datos mutables compartidos. Juan Reynolds. Millennial Perspectives in Computer Science, Actas del Simposio Oxford-Microsoft de 1999 en honor a Sir Tony Hoare
↑ BI como lenguaje de afirmación para estructuras de datos mutables. Samin Ishtiaq, Peter O'Hearn. POP 2001.
↑ Razonamiento local sobre programas que alteran estructuras de datos. Archivado el 27 de septiembre de 2013 en Wayback Machine . Peter O'Hearn, John Reynolds, Hongseok Yang . CSL 2001
↑ Algunas técnicas para probar programas que alteran las estructuras de datos. RM Burstall. Inteligencia artificial 7, 1972.
↑ La lógica de las implicaciones agrupadas PW O'Hearn y DJ Pym. Boletín de lógica simbólica, 5 (2), junio de 1999, pp215-244
↑ 1 2 3 4 Lee, Parque, 2014 .
↑ Programas y Pruebas, 2014 .
↑ 12 Reynolds , 2008 .
↑ Parkinson, Bierman, 2005 .
↑ Verificación de software de Chris Poskitt (otoño de 2013) Clase 5: Lógica de separación Partes I - II (enlace descendente)
↑ 1 2 Introducción a la lógica de separación, 2012 .
↑ Tjark Weber (2004). “Hacia la Verificación Mecanizada de Programas con Lógica de Separación”. Computer Science Logic ~-- 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Polonia, septiembre de 2004, Actas . Apuntes de clase en informática. Saltador. páginas. 250-264. weber04hacia . Consultado el 6 de diciembre de 2013 . |access-date=requiere |url=( ayuda )
↑ Matthew J. Parkinson Razonamiento local para Java Archivado el 23 de septiembre de 2015 en Wayback Machine , 2005, UCAM-CL-TR-654, ISSN 1476-2986
↑ Clase 24: Análisis de formas y punteros. Archivado el 29 de noviembre de 2014 en Wayback Machine , LARA, EPFL.
↑ O'Hearn, Peter (2007). “Recursos, Concurrencia y Razonamiento Local” (PDF) . Informática Teórica . 375 (1-3): 271-307. DOI : 10.1016/j.tcs.2006.12.035 . Archivado (PDF) desde el original el 4 de marzo de 2021 . Consultado el 24 de marzo de 2021 . Parámetro obsoleto utilizado |deadlink=( ayuda )
↑ Hoare, CAR (1972). “Hacia una teoría de la programación paralela”. Técnicas de sistemas operativos. Prensa Académica .
↑ 1 2 Étienne Lozes Información como recurso en la lógica de separación (enlace no disponible) , proyecto ANR, borrador
↑ Brookes, Stephen (2007). "Una semántica para la lógica de separación concurrente" (PDF) . Informática Teórica . 375 (1-3): 227-270. DOI : 10.1016/j.tcs.2006.12.034 . Archivado (PDF) desde el original el 09-05-2021 . Consultado el 24 de marzo de 2021 . Parámetro obsoleto utilizado |deadlink=( ayuda )
↑ European Association for Theoretical Computer Science 2016 Gödel Prize Archivado el 14 de julio de 2016 en Wayback Machine .
↑ Ynot . Consultado el 19 de noviembre de 2014. Archivado desde el original el 25 de febrero de 2009. (indefinido)
↑ Depredadores . Fecha de acceso: 19 de noviembre de 2014. Archivado desde el original el 25 de octubre de 2014. (indefinido)
↑ Mutilin V.S., Novikov E.M., Khoroshilov A.V. Resumen de herramientas para la verificación estática de programas C aplicados a controladores de dispositivos del sistema operativo Linux // Actas del Instituto de Programación de Sistemas de la Academia Rusa de Ciencias. - 2012. - T. 22 , N º 3 . - S. 293-326 .
↑ Cliff Jones (de U. Newcastle), Viktor Vafeiadis (de MPI-SWS) Pensamiento de garantía de confianza y lógica de separación. Archivado el 29 de noviembre de 2014 en Wayback Machine .

Literatura

Reynolds J. C. Separation Logic: A Logic for Shared Mutable Data Structures // LICS '02 :del 17º Simposio Anual IEEE sobre Lógica en Informática - Washington, DC, EE . UU . : IEEE Computer Society , 2002. - P. 55-74. - ISBN 978-0-7695-1483-3 - doi:10.1109/LICS.2002.1029817
Reynolds J. C. An Overview of Separation Logic // Verified Software : Theories, Tools, Experiments : First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zúrich, Suiza, 10-13 de octubre de 2005, artículos y debates seleccionados revisados / B. Meyer , J. Woodcock - Berlín : Springer Berlin Heidelberg , 2008. - P. 460-469. - ( Lecture Notes in Computer Science ; Vol. 4171) - ISBN 978-3-540-69147-1 - ISSN 0302-9743 ; 1611-3349 - doi:10.1007/978-3-540-69149-5_49
Parkinson M. , Bierman G. Lógica de separación y abstracción (inglés) // POPL '05 : Actas del 32º simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación Long Beach, CA, EE. UU. 12 al 14 de enero de 2005 — Nuevo York, NY, EE . UU .: ACM , 2005. - P. 247-258. - ISBN 978-1-58113-830-6 - doi:10.1145/1040305.1040326
Lee, Wonyeol y Park, Sung Woo. Un sistema de prueba para lógica de separación con varita mágica (inglés) // SIGPLAN Not .. - ACM, 2014. - Vol. 49 , núm. 1 . - Pág. 477--490 . — ISSN 0362-1340 .
Appel A. , Dockins R. , Hobor A. , Beringer L. , Dodds J. , Blazy S. , Leroy X. Program Logics for Certified Compilers (inglés) - Cambridge University Press , 2014. - 472 p. — ISBN 978-1-107-04801-0
Ilia Sergey. 8.2 Conceptos básicos de la lógica de separación // Programas y pruebas: Mecanización de las matemáticas con tipos dependientes . - 2014. - (Apuntes).
Peter W. O'Hearn. Introducción a la lógica de separación (y verificación y análisis automáticos de programas) // Seguridad y protección del software; Herramientas de Análisis y Verificación. - 2012. - vol. 33. - Pág. 286-318.

Enlaces

Cliff Jones ( Universidad de Newcastle ), Viktor Vafeiadis ( MPI-SWS ) Rely-garantize thinking & separation logic (ing.) - presentación que ilustra bien los conceptos de la lógica de separación
Matthew Parkinson Una introducción a la lógica de separación (inglés) : una presentación en la que se ilustran todos los aspectos principales de la lógica de separación: axiomas, ejemplos de programas con los diagramas correspondientes, sintaxis