Resultados de investigación
Los investigadores František Farka, Aleksandar Nanevski, Anindya Banerjee (del Instituto IMDEA Software), Germán Andrés Delbianco (Nomadic Labs), e Ignacio Fábregas (Universidad Complutense de Madrid) han publicado recientemente “On Algebraic Abstractions for Concurrent Separation Logics”, que ha sido aceptado en POPL 2021.
La Lógica de separación simultánea es una forma de lógica para la verificación de programas de estado. Esta lógica se distingue por la transferencia de la propiedad del estado sobre la composición paralela de hilos. La transferencia de propiedad semántica viene dada por la estructura algebraica de los monoides conmutativos parciales (PCM). Las investigaciones actuales consideran la transferencia de propiedad principalmente desde una perspectiva lógica, mientras que comparativamente se presta menos atención a la manipulación simbólica a nivel de especificaciones expresadas en el lenguaje de aserción.
En su publicación, Farka, Nanevski, Banerjee, Delbianco y Frábegas ofrecen una formalización algebraica del lenguaje de aserción para la transferencia de la propiedad en la lógica de la separación simultánea mediante funciones parciales de conservación de la estructura (es decir, morfismos) entre los PCM, y una noción asociada de relaciones de separación. Esto quiere decir que, al verificar el software, pueden afirmar especificaciones en los lenguajes simbólicos de las matemáticas estándar; la única concesión a la que se ven obligados es la relajación de los dominios totales a los parciales.
Los morfismos, como estructuras que preservan los mapas, son un concepto estándar en álgebra y teoría de categorías. Sin embargo, los morfismos no han visto uso ubicuo en la lógica de separación antes. Las relaciones de separación son relaciones binarias que generalizan la desunión y caracterizan la insumos en los que los morfismos conservan la estructura. Las dos abstracciones facilitan la verificación habilitando formas concisas de escribir las especificaciones, proporcionando vistas abstractas de los estados de los hilos que se conservan bajo transferencia de propiedad, y permitiendo la construcción a nivel de usuario de nuevos PCM de los existentes.
El trabajo presentado constituye un novedoso enfoque del lenguaje de afirmación de las lógicas de separación, ya que el álgebra de los PCM, sus morfismos y construcciones no ha sido considerado antes en este contexto.
