La lógica y la semántica de los programas cuentan una bonita historia sobre la composición secuencial: al ejecutar (𝑆1; 𝑆2), primero ejecutamos 𝑆1 y, después, 𝑆2. Sin embargo, para mejorar el rendimiento, los procesadores ejecutan las instrucciones desordenadas y los compiladores reordenan los programas de forma aún más drástica. Por su diseño, los sistemas con un único subproceso no pueden observar estos reordenamientos, aunque los sistemas con varios subprocesos sí que pueden, lo que hace que la historia sea bastante menos bonita. El intento formal de entender el desorden resultante se conoce como "modelo de memoria relajado".

Los modelos anteriores no abordan directamente la composición secuencial, no restringen en exceso los procesadores y los compiladores, ni permiten comportamientos sin sentido que son inobservables en la práctica. Para que haya compatibilidad con la composición secuencial y, al mismo tiempo, orientarnos 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 (𝑆1; 𝑆2), el transformador de predicado aplicado a la precondición de un evento 𝑒 de 𝑆2 se elige en función del conjunto de eventos de 𝑆1 de los que depende 𝑒.

• Repositorio del proyecto