Tesis:
Hoare-style Reasoning with Higher-order Control : Continuations and Concurrency
- Autor: DELBIANCO, Germán Andrés
- Título: Hoare-style Reasoning with Higher-order Control : Continuations and Concurrency
- Fecha: 2017
- Materia: Sin materia definida
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: LENGUAJES Y SISTEMAS INFORMATICOS E INGENIERIA DE SOFTWARE
- Acceso electrónico: http://oa.upm.es/47796/
- Director/a 1º: NANEVSKI, Aleksandar
- Resumen: La correctitud del software, es decir, el problema de decidir a ciencia cierta que un algoritmo o un programa es correcto antes de su ejecución, es una cuestión de larga data que siempre ha sido relevante en la comunidad de las Ciencias de la Computación. En los últimos tiempos cada vez más, con la industria comprendiendo la importancia y los beneficios de la verificación formal de software. Esto se produce como consecuencia de descubrir—o aceptar—que desarrollar una prueba formal de la correctitud de un sistema informático es una alternativa mucho más eficiente, incluso desde un punto de vista meramente económico, a depender de ciclos a posteriori de prueba, detección de errores y re-implementación. Sin embargo, la verificación formal es una tarea extremadamente compleja: es una disciplina muy cercana a los modelos semánticos sobre los cuales se desarrollan los lenguajes de programación, involucrando usualmente modelos matemáticos complejos. A medida que la tecnología avanza, desarrollar nuevas lógicas, o nuevas herramientas orientadas a la verificación de estos nuevos avances se torna una empresa cada vez más difícil. Por otra parte, y dada la dificultad que conlleva comprobar formalmente propiedades de programas complejos, o de grandes sistemas, es preferible tener que hacer dichas demostraciones como mucho una única vez. Desafortunadamente, esto no es siempre factible. El objetivo principal de esta tesis es el desarrollo y la aplicación de lógicas diseñadas específicamente para la verificación formal modular de programas con efectos de control de alto orden. En particular, esta tesis hace foco en dos clases diferentes de efectos de control: control secuencial, dado por construcciones como las continuaciones y operadores de alto orden como call/cc; y concurrencia de variables compartidas. Una continuación es una abstracción que captura el contexto de ejecución de un cómputo o programa, i. e. captura el “futuro de un cómputo”. Operadores de control de alto orden como call/cc transforman a dichos contextos de ejecución en objetos de primera clase de un lenguaje de programación, permitiendo a los programas en ellos implementados tener acceso (y control) operacional a su contexto de ejecución. Esta capacidad de manipular “el futuro” convierte a este tipo de operadores más flexibles y expresivos que operaciones de primer orden que sólo permiten hacer saltos en la ejecución de un programa, e.g. goto y similares. Pero, también implica que razonar formalmente sobre éstos sea más complicado. La contribución de esta tesis en este sentido es el desarrollo de una nueva lógica, inspirada en la Lógica de Separación (o Separation Logic) diseñada para la verificación de programas de alto orden que utilizan operadores de control como call/cc y abort. En cuanto a la concurrencia con variables compartidas, nos encontramos en presencia de sistemas masivamente concurrentes ejecutándose sobre capacidades de multiprocesamiento cada vez mayores. En este contexto, es comprensible que los programadores—y por lo tanto los lenguajes de programación—deseen explotar las capacidades de paralelización existentes para producir programas más eficientes. Desafortunadamente, la naturaleza misma de la concurrencia conspira en contra de razonar—ya sea formal o intuitivamente—sobre la correctitud de algoritmos concurrentes. La contribución de esta tesis en este campo es Linking in Time, una nueva técnica de especificación de objetos concurrentes en la cual los aspectos dinámicos y no estructurales inherentes al razonamiento formal sobre concurrencia pueden ser representados de forma modular, tanto al nivel de funciones o procedimientos como al hilos de ejecución (threads). Esta técnica ha sido mecanizada formalmente en FCSL, una lógica de separación para concurrencia no-bloqueante, y ha sido aplicada para demostrar formalmente la correctitud de objetos concurrentes complejos, cuyos argumentos de correctitud son intricados o altamente especulativos. Esta técnica es similar en sus objetivos a linearizabilidad (linearizability) pero, se desarrolla exclusivamente en una lógica de separación con el objetivo de capturar uniformemente los propiedades de estado (o memoria) de una estructura de datos concurrente, así como también expresar ciertos aspectos temporales. ABSTRACT The issue of software correctness is a long-standing problem in the computer science community, and it has always been relevant. Nowadays, even more so with the software industry becoming increasingly aware of the importance and benefits of formal verification. This comes as a consequence of realizing that having mathematical proof of the correctness of software systems is more efficient, even from an economical standpoint, than relying on a posteriori cycles of testing, debugging and re-implementing. However, formal verification is painstakingly hard: it is a discipline closely connected to the semantic models on which programming languages are developed, usually involving complex mathematics. As technology paces forward, developing new logics to keep up becomes even harder. Since proving properties about complex programs is hard, it is preferable to have to do their proofs at most once. Unfortunately, this is not always possible. The main goal of this thesis is the development and application of program logics aimed at the modular verification of stateful programs with higher-order control effects. In particular, it focuses of two different kinds of control effects: sequential control, in the shape of continuations and higher-order control operators like call/cc; and shared variable concurrency. A continuation is a powerful abstraction which models the “future of a computation”. The availability of higher-order control operators like call/cc make this execution context first-class citizens of a programming language, allowing client programs to have operational access (and control) over its execution context. The ability to manipulate “the future” makes these operators more powerful than plain goto-like instructions, but it also hinders the formal reasoning about programs. The contribution of this thesis in this regard is the development of a novel separation-like logic for the verification of higher-order stateful programs featuring call/cc and abort control operators. As to shared-memory (or shared-variable) concurrency, we live in a world of massively concurrent software systems running over increasing multi-processing power. In such a context, it is natural to expect programmers—and thus programming languages—to desire to exploit the available parallelism in order to produce more efficient software. Unfortunately, the intricacies of concurrency conspire against reasoning—both formally and intuitively—about the correctness of algorithms. The contribution of this thesis in this regard is Linking in Time, a novel approach to specification of concurrent objects, in which the dynamic and non-local aspects inherent to concurrency reasoning can be represented in a procedure-local and thread-local manner. This technique has been formally mechanized in FCSL, a fine-grained concurrent separation logic, and it has been applied to prove the correctness of non-trivial concurrent objects with highly-speculative, non-obvious correctness. The approach is similar in its goals to linearizability, but is carried out exclusively using a separation-style logic to uniformly represent the state and time aspects of the data structure and its methods.