El punto y coma defectuoso
Author
Venue
Actas de la ACM sobre Lenguajes de Programación 2021
Abstract
La lógica y la semántica de los programas nos cuentan una historia agradable sobre la composición secuencial: al ejecutar (S1; S2), primero ejecutamos S1 y luego S2. Sin embargo, para mejorar el rendimiento, los procesadores ejecutan las instrucciones fuera de orden, y los compiladores reordenan los programas de forma aún más drástica. Por diseño, los sistemas de un solo subproceso no pueden observar estas reordenaciones; sin embargo, los sistemas de múltiples subprocesos sí pueden, lo que hace que la historia sea considerablemente menos agradable. Un intento formal de comprender el caos resultante se conoce como «modelo de memoria relajado». Los modelos anteriores o bien no abordan directamente la composición secuencial, o bien restringen en exceso a los procesadores y compiladores, o bien permiten comportamientos sin sentido y fantasmagóricos que son inobservables en la práctica. Para dar soporte a la composición secuencial al tiempo que nos orientamos hacia el hardware moderno, enriquecemos el enfoque estándar basado en eventos con precondiciones y familias de transformadores de predicados. Al calcular el significado de (S1;S2), el transformador de predicados aplicado a la precondición de un evento e de S2 se elige en función del conjunto de eventos de S1 del que depende e. Aplicamos este enfoque a dos modelos de memoria existentes.
