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 programas. Fue desarrollado por John C. Reynolds , Peter O'Hearn , Samin Ishtiaq y Hongseok Yang, [1] [2] [3] [4] basándose en los primeros trabajos 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 del MCCA 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:
- programas que manipulan estructuras de datos de punteros, incluida la información que se oculta en presencia de punteros;
- "transferencia de propiedad" (evitación de axiomas de marco semántico ); y
- separación virtual (razonamiento modular) entre módulos concurrentes.
La lógica de separación respalda el campo de investigación en desarrollo descrito por Peter O'Hearn y otros como razonamiento local , en el que las especificaciones y pruebas de un componente de programa mencionan solo la parte de memoria utilizada por el componente, y no todo el estado global del sistema. Las aplicaciones incluyen la verificación automatizada del programa (donde un algoritmo verifica la validez de otro algoritmo) y la paralelización automatizada del software.
Afirmaciones: operadores y semántica
Las aserciones lógicas de separación describen "estados" que constan de 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 . Una tiendaes una función que asigna variables a valores. Un montones una función parcial que asigna direcciones de memoria a valores. Dos montones y son disjuntos (denotados) si sus dominios no se superponen (es decir, para cada dirección de memoria , al menos uno de y es indefinido).
La lógica permite probar juicios de la forma. , dónde es una tienda, es un montón, y es una aserción sobre el almacén y el montón dados. Afirmaciones lógicas de separación (denotadas como, , ) contienen los conectivos booleanos estándar y, además, , , , y , dónde y son expresiones.
- El constante afirma que el montón está vacío , es decir, Cuándo no está definido para todas las direcciones.
- El operador binario toma una dirección y un valor y afirma que el montón está definido exactamente en una ubicación, asignando la dirección dada al valor dado. Es decir, Cuándo (dónde denota el valor de la expresión evaluado en la tienda ) y de lo contrario no está definido.
- El operador binario (pronunciado estrella o conjunción de separación ) afirma que el montón se puede dividir en dos partes disjuntas donde sus dos argumentos se mantienen, respectivamente. Es decir, cuando exista tal que y y y .
- El operador binario ( varita mágica pronunciada o implicación de separación ) afirma que extender el montón con una parte disjunta que satisface su primer argumento da como resultado un montón que satisface su segundo argumento. Es decir,. cuando por cada montón tal que , además sostiene.
Los operadores y comparten algunas propiedades con los operadores clásicos de conjunción e implicación . Se pueden combinar usando una regla de inferencia similar a modus ponens
y forman un adjunto , es decir, si y solo si por ; más precisamente, los operadores adjuntos son y .
Razonamiento de programas: triples y reglas de prueba
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 saldrá mal (por ejemplo, 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 ubicaciones de memoria cuya existencia se afirma en la condición previa o que han sido asignadas por sí 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 se puede ejecutar en cualquier estado mayor (satisfaciendo ) y que su ejecución no afectará a la parte adicional del estado (y por lo tanto seguirá siendo cierto en la condición posterior). La condición lateral hace cumplir esto especificando que ninguna de las variables modificadas por ocurrir libre en , es decir, ninguno de ellos está en el conjunto de 'variables libres' de .
Intercambio
La lógica de separación conduce a pruebas simples de manipulación de punteros para estructuras de datos que exhiben patrones de intercambio regulares que pueden describirse simplemente usando conjunciones de separación; los ejemplos incluyen listas y variedades de árboles simple y doblemente enlazadas. Los gráficos y DAG y otras estructuras de datos con un intercambio más general son más difíciles para la prueba formal e informal. No obstante, la lógica de la separación se ha aplicado con éxito al razonamiento sobre programas con compartición general.
En su artículo POPL'01, [3] O'Hearn e Ishtiaq explicaron cómo la conexión de la varita mágicapodría usarse para razonar en presencia de compartir, al menos en principio. Por ejemplo, en el triple
obtenemos la condición previa más débil para una declaración que muta el montón en la ubicación , y esto funciona para cualquier condición posterior, no solo una que se presenta de manera ordenada utilizando la conjunción de separación. Esta idea fue llevada mucho más lejos por Yang, quien usópara proporcionar un razonamiento localizado sobre mutaciones en el algoritmo clásico de marcado de gráficos de Schorr-Waite . [8] Finalmente, uno de los trabajos más recientes en esta dirección es el de Hobor y Villard, [9] que emplean no solo pero también un conectivo que se ha denominado de forma diversa conjunción superpuesta o sepish, [10] y que se puede utilizar para describir estructuras de datos superpuestas: tiene un montón Cuándo y mantener para submontones y cuya unión es , pero que posiblemente tengan una parte no vacía en común. Abstractamente,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] usando una regla de prueba
lo que permite un razonamiento independiente sobre los hilos que acceden al almacenamiento separado. Las reglas de prueba de O'Hearn adaptaron un enfoque temprano de Tony Hoare al razonamiento sobre la concurrencia, [12] reemplazando el uso de restricciones de alcance para asegurar la separación mediante el razonamiento en la 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 la lógica de separación concurrente podía rastrear la transferencia de propiedad dinámica de porciones del montón entre procesos; los ejemplos en el documento incluyen un búfer de transferencia de puntero y un administrador de memoria .
Stephen Brookes proporcionó por primera vez un modelo para la lógica de separación concurrente en un artículo adjunto 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 mostrado la falta de solidez de una versión anterior e inédita 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 a fondo en el de Brookes.
Al principio parecía que CSL se adaptaba bien a lo que Dijkstra había llamado procesos débilmente conectados, [14] pero quizás no a algoritmos concurrentes de grano fino con interferencia significativa. Sin embargo, gradualmente se fue dando cuenta de que el enfoque básico de CSL era considerablemente más poderoso de lo que se había previsto inicialmente, si se empleaban modelos no estándar de las conectivas lógicas e incluso los triples de Hoare.
Se propuso una versión abstracta de la lógica de separación que funciona para los 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 la interferencia de procesos concurrentes, por ejemplo, codificando la técnica de garantía de confianza que se había utilizado originalmente. propuso razonar acerca de 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 condiciones previas y posteriores. 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 kernel μC / OS-II mencionado allí. Pero, aunque se han dado pasos, [18] hasta ahora, el razonamiento 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-receptores del Premio Gödel 2016 por su invención de la lógica de separación simultánea. [19]
Herramientas de verificación y análisis de programas
Las herramientas para razonar sobre programas se encuentran en un espectro que va desde herramientas de análisis de programas completamente automáticas, que no requieren ninguna entrada del usuario, hasta herramientas interactivas en las que el ser humano está íntimamente involucrado en el proceso de prueba. Se han desarrollado muchas de estas herramientas; la siguiente lista incluye algunos representantes en cada categoría.
- Análisis automáticos de programas. Por lo general, estas herramientas buscan clases restringidas de errores (por ejemplo, errores de seguridad de la memoria) o intentan probar su ausencia, pero no logran demostrar su total corrección.
- Un ejemplo actual es Facebook Infer , una herramienta de análisis estático para Java, C y Objective-C basada en la lógica de separación y la bi-abducción. [20] A partir de 2015, Infer encontró cientos de errores por mes y los desarrolladores los corrigieron antes de enviarlos a las aplicaciones móviles de Facebook [21]
- Otros ejemplos incluyen SpaceInvader (uno de los primeros analizadores SL), Predator (que ha ganado varios concursos de verificación), MemCAD (que mezcla propiedades numéricas y de forma) y SLAyer (de Microsoft Research, centrado en estructuras de datos que se encuentran en controladores de dispositivos)
- Prueba interactiva. Las pruebas se han realizado utilizando incorporaciones de la lógica de separación en probadores de teoremas interactivos, como el asistente de prueba Coq y HOL (asistente de prueba) . En comparación con el trabajo de análisis de programas, estas herramientas requieren más esfuerzo humano pero demuestran propiedades más profundas, hasta la corrección funcional.
- Una prueba del sistema de archivos FSCQ [22] donde la especificación incluye el comportamiento ante fallas así como el funcionamiento normal. Este trabajo ganó el premio al mejor artículo en el Simposio sobre principios de sistemas operativos de 2015.
- Verificación de un gran fragmento del sistema de tipos Rust y algunas de sus bibliotecas estándar en el proyecto RustBelt utilizando el marco Iris para la lógica de separación en el asistente de pruebas de Coq .
- Verificación de una implementación OpenSSL de un algoritmo de autenticación criptográfica, [23] utilizando C verificable
- Verificación de módulos clave de un kernel de SO comercial, el kernel μC / OS-II, el primer kernel preventivo comercial que se ha verificado. [24]
- Otros ejemplos incluyen la biblioteca Ynot [25] para el asistente de pruebas Coq ; la incrustación Holfoot de Smallfoot en HOL; Lógica de separación concurrente de grano fino y Bedrock (una biblioteca Coq para programación de bajo nivel).
- Entre. Muchas herramientas requieren más intervención del usuario que los análisis de programas, ya que esperan que el usuario ingrese afirmaciones como especificaciones previas / posteriores para funciones o invariantes de bucle, pero después de que se proporciona esta entrada, intentan ser total o casi completamente automáticas; este modo de verificación se remonta a trabajos clásicos de la década de 1970, como el verificador de J King y el verificador de Stanford Pascal. Este estilo de verificador se ha denominado recientemente verificación activa automática , un término que pretende evocar la forma de interactuar con un verificador a través de un bucle de verificación-afirmación, análoga a la interacción entre un programador y un verificador de tipos.
- El primer verificador de Separation Logic, Smallfoot , estaba en esta categoría intermedia. Se requería que el usuario ingresara especificaciones previas / posteriores, invariantes de bucle e invariantes de recursos para los bloqueos. Introdujo un método de ejecución simbólica, así como una forma automática de inferir axiomas de marco. Smallfoot incluye lógica de separación simultánea.
- SmallfootRG es un verificador para una combinación de lógica de separación y el método clásico de confianza / garantía para programas concurrentes.
- Heap Hop implementa una lógica de separación para el paso de mensajes, siguiendo las ideas en Singularity (sistema operativo) .
- Verifast es una herramienta de corriente avanzada en la categoría intermedia. Ha demostrado pruebas que van desde patrones orientados a objetos hasta algoritmos altamente concurrentes y programas de sistemas.
- El lenguaje de programación Mezzo y los tipos de separación de líquidos asíncronos incluyen ideas relacionadas con CSL en el sistema de tipos de un lenguaje de programación. La idea de incluir la separación en un sistema de tipos tiene ejemplos anteriores en Tipos de alias y Control sintáctico de interferencias .
La distinción entre verificadores interactivos e intermedios no es tajante. Por ejemplo, Bedrock se esfuerza por lograr un alto grado de automatización, en lo que denomina verificación principalmente automática, donde Verifast a veces requiere anotaciones que se asemejan a las tácticas (pequeños programas) que se utilizan en los verificadores interactivos.
Referencias
- ↑ a b Reynolds, John C. (2002). "Lógica de separación: una lógica para estructuras de datos mutables compartidas" (PDF) . LICS .
- ^ Reynolds, John C. (1999). "Razonamiento intuicionista sobre la estructura de datos mutables compartidos". En Davies, Jim ; Roscoe, Bill ; Woodcock, Jim (eds.). Millennial Perspectives in Computer Science, Actas del Simposio Oxford-Microsoft de 1999 en honor a Sir Tony Hoare . Palgrave .
- ^ a b Ishtiaq, Samin; O'Hearn, Peter (2001). "BI como lenguaje de afirmación para estructuras de datos mutables". POPL . ACM .
- ^ 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 .
- ^ Burstall, RM (1972). "Algunas técnicas para probar programas que alteran las estructuras de datos". Inteligencia de máquina . 7 .
- ^ 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 .
- ^ O'Hearn, Peter (febrero de 2019). "Lógica de separación" . Comun. ACM . 62 (2): 86–95. doi : 10.1145 / 3211968 . ISSN 0001-0782 .
- ^ Yang, Hongseok (2001). "Un ejemplo de razonamiento local en lógica de puntero BI: el algoritmo de marcado de gráfico de Schorr-Waite" . Actas del 1er Taller de Semántica 'Análisis de programas' y entornos informáticos para la gestión de la memoria .
- ^ Hobor, Aquino; Villard, Jules (2013). "Las ramificaciones de compartir en estructuras de datos" (PDF) . Avisos ACM SIGPLAN . 48 : 523–536. doi : 10.1145 / 2480359.2429131 .
- ^ Gardner, Philippa; Maffeis, Sergio; Smith, Hareth (2012). "Hacia una lógica de programa 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 .
- ^ 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 .
- ^ Hoare, CAR (1972). "Hacia una teoría de la programación paralela". Técnicas del sistema operativo. Prensa académica .
- ^ 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 .
- ^ Dijkstra, Edsger W. Cooperando procesos secuenciales (EWD-123) (PDF) . Archivo EW Dijkstra. Centro de Historia Estadounidense, Universidad de Texas en Austin .( transcripción ) (septiembre de 1965)
- ^ Calcagno, Cristiano; O'Hearn, Peter W .; Yang, Hongseok (2007). "Acción local y lógica de separación abstracta" (PDF) . 22º Simposio Anual del IEEE sobre Lógica en Ciencias de la Computación (LICS 2007) . págs. 366–378. CiteSeerX 10.1.1.66.6337 . doi : 10.1109 / LICS.2007.30 . ISBN 978-0-7695-2908-0. S2CID 1044254 .
- ^ Dinsdale-Young, Thomas; Birkedal, Lars; Gardner, Philippa; Parkinson, Matthew; Yang, Hongseok (2013). "Vistas" (PDF) . Avisos ACM SIGPLAN . 48 : 287–300. doi : 10.1145 / 2480359.2429104 .
- ^ 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 .
- ^ Gotsman, Alexey; Berdine, Josh; Cook, Byron; Sagiv, Mooly (2007). Análisis de forma modular de rosca (PDF) . PLDI . Apuntes de conferencias en Ciencias de la Computación. 5403 . págs. 266-277. doi : 10.1007 / 978-3-540-93900-9_3 . ISBN 978-3-540-93899-6.
- ^ https://www.eatcs.org/index.php/component/content/article/1-news/2280-2016-godel-prize-
- ^ Lógica de separación y bi-abducción, página , Inferir sitio del proyecto .
- ^ Inferencia de Facebook de código abierto: Identifique errores antes de realizar envíos. C Calcagno, D DIstefano y P O'Hearn. 11 de junio de 2015
- ^ Uso de la lógica de Crash Hoare para certificar el sistema de archivos FSCQ , H Chen et al, SOSP'15
- ^ Corrección y seguridad verificadas 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
- ^ Un marco de verificación práctica para kernels de sistemas operativos preventivos . Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang y Zhaohui Li :. En CAV 2016: 59-79
- ^ La página de inicio del proyecto Ynot , Universidad de Harvard , Estados Unidos.