stringtranslate.com

Lógica de separación

En informática , la lógica de separación [1] es una extensión de la lógica de Hoare , una forma de razonar sobre los programas. Fue desarrollada por John C. Reynolds , Peter O'Hearn , Samin Ishtiaq y Hongseok Yang, [1] [2] [3] [4] basándose en el trabajo inicial de Rod Burstall . [5] El lenguaje de aserción de la lógica de separación es un caso especial de la lógica de implicaciones agrupadas (BI). [6] Un artículo de revisión de CACM de O'Hearn traza los desarrollos en el tema hasta principios de 2019. [7]

Descripción general

La lógica de separación facilita el razonamiento sobre:

La lógica de separación respalda el campo de investigación en desarrollo descrito por Peter O'Hearn y otros como razonamiento local , según el cual las especificaciones y pruebas de un componente de programa mencionan solo la parte de memoria utilizada por el componente y no el estado global completo del sistema. Las aplicaciones incluyen la verificación automatizada de programas (donde un algoritmo verifica la validez de otro algoritmo) y la paralelización automatizada de software.

Afirmaciones: operadores y semántica

Las afirmaciones de lógica de separación describen "estados" que consisten en un almacén y un montón , que corresponden aproximadamente al estado de las variables locales (o asignadas por pila ) y los objetos asignados dinámicamente en lenguajes de programación comunes como C y Java . Un almacén es una función que asigna variables a valores. Un montón es una función parcial que asigna direcciones de memoria a valores. Dos montones y son disjuntos (denotados como ) si sus dominios no se superponen (es decir, para cada dirección de memoria , al menos uno de y no está definido).

La lógica permite probar juicios de la forma , donde es un almacén, es un montón y es una afirmación sobre el almacén y el montón dados. Las afirmaciones de lógica de separación (denotadas como , , ) contienen los conectores booleanos estándar y, además, , , , y , donde y son expresiones.

Los operadores y comparten algunas propiedades con los operadores de conjunción e implicación clásicos . Se pueden combinar utilizando una regla de inferencia similar al modus ponens

y forman una adjunción , es decir, si y sólo si para ; más precisamente, los operadores adjuntos son y .

Razonamiento sobre programas: triples y reglas de demostración

En la lógica de separación, los triples de Hoare tienen un significado ligeramente diferente al de la lógica de Hoare . El triple afirma que si el programa se ejecuta desde un estado inicial que satisface la condición previa , entonces el programa no fallará (por ejemplo, no tendrá un comportamiento indefinido) y, si termina, entonces el estado final satisfará la condición posterior . En esencia, durante su ejecución, puede acceder solo a las ubicaciones de memoria cuya existencia se afirma en la condición previa o que han sido asignadas por él mismo.

Además de las reglas estándar de la lógica de Hoare , la lógica de separación admite la siguiente regla muy importante:

Esto se conoce como la regla del marco (llamada así por el problema del marco ) y permite el razonamiento local. Dice que un programa que se ejecuta de forma segura en un estado pequeño (satisfaciendo ) , también puede ejecutarse en cualquier estado más grande (satisfaciendo ) y que su ejecución no afectará la parte adicional del estado (y por lo tanto seguirá siendo verdadera en la poscondición). La condición secundaria refuerza esto al especificar que ninguna de las variables modificadas por ocurre libre en , es decir, ninguna de ellas está en el conjunto de 'variables libres' de .

Intercambio

La lógica de separación permite realizar demostraciones sencillas de manipulación de punteros para estructuras de datos que presentan patrones de compartición regulares que pueden describirse simplemente mediante conjunciones separadoras; por ejemplo, listas enlazadas simple y doblemente y variedades de árboles. Los gráficos, los DAG y otras estructuras de datos con una compartición más general son más difíciles de demostrar, tanto formal como informalmente. No obstante, la lógica de separación se ha aplicado con éxito al razonamiento sobre programas con una compartición general.

En su artículo POPL'01, [3] O'Hearn e Ishtiaq explicaron cómo el conector de la varita mágica podría usarse para razonar en presencia de compartir, al menos en principio. Por ejemplo, en el triple

obtenemos la precondición más débil para una declaración que muta el montón en la ubicación , y esto funciona para cualquier postcondición, no solo una que se presenta ordenadamente usando la conjunción separadora. Esta idea fue llevada mucho más allá por Yang, quien solía proporcionar razonamiento localizado sobre mutaciones en el algoritmo clásico de marcado de grafos de Schorr-Waite. [8] Finalmente, uno de los trabajos más recientes en esta dirección es el de Hobor y Villard, [9] quienes emplean no solo sino también un conectivo que ha sido llamado de diversas maneras conjunción superpuesta o sepish, [10] y que puede usarse para describir estructuras de datos superpuestas: se cumple de un montón cuando y se cumple para submontones y cuya unión es , pero que posiblemente tienen una porción no vacía en común. De manera abstracta, puede verse como una versión del conectivo de fusión de la lógica de relevancia .

Lógica de separación concurrente

Una lógica de separación concurrente (CSL), una versión de la lógica de separación para programas concurrentes, fue propuesta originalmente por Peter O'Hearn [11] , utilizando una regla de prueba

que permite el razonamiento independiente sobre subprocesos que acceden a almacenamiento separado. Las reglas de prueba de O'Hearn adaptaron un enfoque temprano de Tony Hoare para razonar sobre concurrencia, [12] reemplazando el uso de restricciones de alcance para asegurar la separación mediante el razonamiento en lógica de separación. Además de extender el enfoque de Hoare para aplicarlo en presencia de punteros asignados al montón, O'Hearn mostró cómo el razonamiento en lógica de separación concurrente podría rastrear la transferencia de propiedad dinámica de porciones del montón entre procesos; los ejemplos en el artículo incluyen un búfer de transferencia de punteros y un administrador de memoria .

Al comentar el trabajo clásico temprano sobre la libertad de interferencia de Susan Owicki y David Gries , O'Hearn dice que la verificación explícita de la no interferencia no es necesaria porque su sistema descarta la interferencia de manera implícita, por la naturaleza de la forma en que se construyen las pruebas.

Stephen Brookes fue el primero en proporcionar un modelo para la lógica de separación concurrente en un artículo complementario al de O'Hearn. [13] La solidez de la lógica había sido un problema difícil y, de hecho, un contraejemplo de John Reynolds había demostrado la falta de solidez de una versión anterior, no publicada, de la lógica; la cuestión planteada por el ejemplo de Reynolds se describe brevemente en el artículo de O'Hearn y más detalladamente en el de Brookes.

En un principio, parecía que el CSL era adecuado para lo que Dijkstra había llamado procesos débilmente conectados [14] , pero tal vez no para algoritmos concurrentes de grano fino con interferencias significativas. Sin embargo, poco a poco se fue dando cuenta de que el enfoque básico del CSL era considerablemente más potente de lo que se había previsto inicialmente, si se empleaban modelos no estándar de los conectivos lógicos e incluso de las ternas de Hoare.

Se propuso una versión abstracta de la lógica de separación que funciona para triples de Hoare donde las precondiciones y las poscondiciones son fórmulas interpretadas sobre un monoide conmutativo parcial arbitrario en lugar de un modelo de montón particular. [15] Más tarde, mediante la elección adecuada del monoide conmutativo, se descubrió sorprendentemente que las reglas de prueba de las versiones abstractas de la lógica de separación concurrente se podían utilizar para razonar sobre procesos concurrentes que interfieren, por ejemplo, codificando la técnica de garantía de confianza que se había propuesto originalmente para razonar sobre la interferencia; [16] en este trabajo, los elementos del modelo no se consideraron recursos, sino más bien "vistas" del estado del programa, y ​​una interpretación no estándar de los triples de Hoare acompaña la lectura no estándar de las precondiciones y poscondiciones. Finalmente, se han utilizado principios de estilo CSL para componer razonamientos sobre historias de programas en lugar de estados de programas, con el fin de proporcionar técnicas modulares para razonar sobre algoritmos concurrentes de grano fino. [17]

Se han incluido versiones de CSL en muchas herramientas de verificación interactivas y semiautomáticas (o "intermedias"), como se describe en la siguiente sección. Un esfuerzo de verificación particularmente significativo es el del núcleo μC/OS-II mencionado allí. Pero, aunque se han dado pasos, [18] hasta el momento el razonamiento al estilo CSL se ha incluido en comparativamente pocas herramientas en la categoría de análisis automático de programas (y ninguna se menciona en la siguiente sección).

O'Hearn y Brookes son co-ganadores del Premio Gödel 2016 por su invención de la lógica de separación concurrente. [19]

Herramientas de verificación y análisis de programas

Las herramientas para razonar sobre programas abarcan desde herramientas de análisis de programas totalmente automáticas, que no requieren ninguna intervención del usuario, hasta herramientas interactivas en las que el ser humano participa íntimamente en el proceso de prueba. Se han desarrollado muchas de estas herramientas; la siguiente lista incluye algunos representantes de cada categoría.

La distinción entre verificadores interactivos y verificadores intermedios no es tan clara. Por ejemplo, Bedrock busca un alto grado de automatización, en lo que denomina verificación mayoritariamente automática, mientras que Verifast a veces requiere anotaciones que se asemejan a las tácticas (pequeños programas) que se utilizan en los verificadores interactivos.

Decidibilidad y complejidad

Se puede demostrar que el problema de satisfacibilidad para un fragmento multiclasificado y sin cuantificadores de lógica de separación parametrizado sobre los tipos de ubicaciones y datos es PSPACE-completo . [27] Se ha integrado un algoritmo para resolver este fragmento en solucionadores SMT basados ​​en DPLL(T) en cvc5 . [28] Extendiendo este resultado, también se puede demostrar que la satisfacibilidad para un análogo de la clase Bernays–Schönfinkel para lógica de separación con ubicaciones de memoria no interpretadas es PSPACE-completo, mientras que el problema es indecidible con ubicaciones de memoria interpretadas (por ejemplo, números enteros) o con otras alternancias de cuantificadores [29]

Referencias

  1. ^ ab Reynolds, John C. (2002). "Lógica de separación: una lógica para estructuras de datos mutables compartidas" (PDF) . LICS .
  2. ^ Reynolds, John C. (1999). "Razonamiento intuicionista sobre estructuras de datos mutables compartidas". En Davies, Jim ; Roscoe, Bill ; Woodcock, Jim (eds.). Perspectivas milenarias en informática, Actas del Simposio Oxford-Microsoft de 1999 en honor a Sir Tony Hoare . Palgrave .
  3. ^ ab Ishtiaq, Samin; O'Hearn, Peter (2001). "BI como lenguaje de aserción para estructuras de datos mutables". Actas del 28.º simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . ACM . págs. 14-26. doi :10.1145/360204.375719. ISBN . 1581133367. Número de identificación del sujeto  2652274. {{cite book}}: |journal=ignorado ( ayuda )
  4. ^ O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). "Razonamiento local sobre programas que alteran estructuras de datos". CSL . CiteSeerX 10.1.1.29.1331 . 
  5. ^ Burstall, RM (1972). "Algunas técnicas para probar programas que alteran las estructuras de datos". Inteligencia artificial . 7 .
  6. ^ O'Hearn, PW; Pym, DJ (junio de 1999). "La lógica de las implicaciones agrupadas". Boletín de lógica simbólica . 5 (2): 215–244. CiteSeerX 10.1.1.27.4742 . doi :10.2307/421090. JSTOR  421090. S2CID  2948552. 
  7. ^ O'Hearn, Peter (febrero de 2019). "Lógica de separación". Commun. ACM . 62 (2): 86–95. doi : 10.1145/3211968 . ISSN  0001-0782.
  8. ^ Yang, Hongseok (2001). "Un ejemplo de razonamiento local en la lógica de punteros de BI: el algoritmo de marcado de grafos de Schorr-Waite". Actas del 1.er taller sobre análisis de programas semánticos y entornos informáticos para la gestión de memoria .
  9. ^ Hobor, Aquinas; Villard, Jules (2013). "Las ramificaciones de la compartición en estructuras de datos" (PDF) . ACM SIGPLAN Notices . 48 : 523–536. doi :10.1145/2480359.2429131.
  10. ^ Gardner, Philippa; Maffeis, Sergio; Smith, Hareth (2012). "Hacia una lógica de programación para Java Script" (PDF) . Actas del 39.º simposio anual ACM SIGPLAN-SIGACT sobre Principios de lenguajes de programación - POPL '12 . págs. 31–44. doi :10.1145/2103656.2103663. hdl :10044/1/33265. ISBN. 9781450310833.S2CID 9571576  .
  11. ^ O'Hearn, Peter (2007). "Recursos, concurrencia y razonamiento local" (PDF) . Ciencias de la computación teórica . 375 (1–3): 271–307. doi : 10.1016/j.tcs.2006.12.035 .
  12. ^ Hoare, CAR (1972). "Hacia una teoría de la programación paralela". Técnicas de sistemas operativos. Academic Press .
  13. ^ Brookes, Stephen (2007). "Una semántica para la lógica de separación concurrente" (PDF) . Theoretical Computer Science . 375 (1–3): 227–270. doi :10.1016/j.tcs.2006.12.034.
  14. ^ Dijkstra, Edsger W. Procesos secuenciales cooperativos (EWD-123) (PDF) . Archivo EW Dijkstra. Centro de Historia Estadounidense, Universidad de Texas en Austin .(transcripción) (septiembre de 1965)
  15. ^ Calcagno, Cristiano; O'Hearn, Peter W.; Yang, Hongseok (2007). "Lógica de separación abstracta y acción local" (PDF) . 22.º Simposio anual IEEE sobre lógica en informática (LICS 2007) . pp. 366–378. CiteSeerX 10.1.1.66.6337 . doi :10.1109/LICS.2007.30. ISBN .  978-0-7695-2908-0.S2CID1044254  .​
  16. ^ Dinsdale-Young, Thomas; Birkedal, Lars; Gardner, Philippa; Parkinson, Matthew; Yang, Hongseok (2013). "Vistas" (PDF) . Avisos SIGPLAN de la ACM . 48 : 287–300. doi :10.1145/2480359.2429104.
  17. ^ Sergey, Ilya; Nanevski, Aleksandar; Banerjee, Anindya (2015). "Especificación y verificación de algoritmos concurrentes con historias y subjetividad" (PDF) . 24º Simposio Europeo de Programación . arXiv : 1410.0306 . Código Bibliográfico :2014arXiv1410.0306S.
  18. ^ Gotsman, Alexey; Berdine, Josh; Cook, Byron; Sagiv, Mooly (2007). "Análisis de forma modular de hilos". Verificación, comprobación de modelos e interpretación abstracta (PDF) . Apuntes de clase en informática. Vol. 5403. págs. 266–277. doi :10.1007/978-3-540-93900-9_3. ISBN 978-3-540-93899-6. {{cite book}}: |journal=ignorado ( ayuda )
  19. ^ "Premio Gödel 2016". Asociación Europea de Informática Teórica . Consultado el 29 de agosto de 2022 .
  20. ^ Lógica de separación y bi-abducción, página, sitio del proyecto Infer.
  21. ^ Código abierto de Facebook Infer: identifica errores antes de enviar. C Calcagno, D D'Stefano y P O'Hearn. 11 de junio de 2015
  22. ^ Uso de la lógica Crash Hoare para certificar el sistema de archivos FSCQ, H Chen et al, SOSP'15
  23. ^ Verificación de la exactitud y seguridad de OpenSSL HMAC. Lennart Beringer, Adam Petcher, Katherine Q. Ye y Andrew W. Appel. En el 24.º Simposio de seguridad de USENIX , agosto de 2015
  24. ^ Un marco de verificación práctico para kernels de SO preventivos. Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang y Zhaohui Li:. En CAV 2016: 59-79
  25. ^ Página de inicio del Proyecto Ynot, Universidad de Harvard , EE. UU.
  26. ^ Viper: una infraestructura de verificación para el razonamiento basado en permisos, P. Müller, M. Schwerhoff y AJ Summers, VMCAI'16
  27. ^ Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "Un procedimiento de decisión para la lógica de separación en SMT". En Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). Tecnología automatizada para verificación y análisis . Apuntes de clase en informática. Cham: Springer International Publishing. págs. 244–261. arXiv : 1603.06844 . doi :10.1007/978-3-319-46520-3_16. ISBN . 978-3-319-46520-3.
  28. ^ Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). "cvc5: un solucionador SMT versátil y de potencia industrial". En Fisman, Dana; Rosu, Grigore (eds.). Herramientas y algoritmos para la construcción y análisis de sistemas . Apuntes de clase en informática. Cham: Springer International Publishing. págs. 415–442. doi : 10.1007/978-3-030-99524-9_24 . ISBN 978-3-030-99524-9.
  29. ^ Reynolds, Andrew; Iosif, Radu; Serban, Cristina (2017). "Razonamiento en el fragmento de Bernays-Schönfinkel-Ramsey de la lógica de separación". En Bouajjani, Ahmed; Monniaux, David (eds.). Verificación, comprobación de modelos e interpretación abstracta . Apuntes de clase en informática. Cham: Springer International Publishing. págs. 462–482. doi :10.1007/978-3-319-52234-0_25. ISBN 978-3-319-52234-0.