Investigación
Laboratorio de Lenguajes y Herramientas de Programación
IMM: Compilation Correctness for Relaxed Memory Models
El marco de trabajo IMM simplifica la comprobación de la corrección de la compilación a partir de los modelos de memoria del lenguaje de programación, como Promising y Weakestmo, a los modelos de memoria del hardware, como x86, Power, Arm y RISC-V. El marco de trabajo está mecanizado en Coq.
Estamos desarrollando un modelo intermedio de memoria débil (IMM, por sus siglas en inglés) como forma de modular las pruebas de corrección de la compilación de lenguajes de programación concurrentes con semántica de consistencia de memoria débil para arquitecturas multinúcleo convencionales, como POWER y ARM. Usamos IMM para demostrar la corrección de la compilación a partir de varios modelos nuevos de memoria del lenguaje de programación (principalmente los que pretenden solucionar el problema de la falta de consistencia) a modelos de memoria de hardware como POWER, ARMv7, ARMv8, RISC-V y x86-TSO. Nuestros resultados están mecanizados en Coq y, hasta donde sabemos, son los primeros resultados de corrección de compilación verificados por la máquina para modelos más débiles que x86-TSO.
