La logique et la sémantique du programme peignent une histoire plaisante de la composition séquentielle : lors de l'exécution (𝑆1; 𝑆2), nous avons exécuté 𝑆1, puis 𝑆2. Pour améliorer les performances, cependant, les processeurs exécutent les instructions dans le désordre, puis les compilateurs réorganisent les programmes encore plus radicalement. Du fait de leur conception, les systèmes à thread unique ne peuvent pas observer ces reclassements, contrairement aux systèmes à threads multiples, ce qui rend l'histoire particulièrement moins plaisante. Une tentative formelle permettant de comprendre le désordre ainsi créé est appelée « modèle de mémoire relaxée ».

Les modèles précédents ne gèrent pas la composition séquentielle directement, ou tendent à limiter exagérément les processeurs et les compilateurs, ou à autoriser des comportements absurdes et soudains qui ne sont pas observables dans la pratique. Pour accompagner la composition séquentielle pendant le ciblage du matériel moderne, nous enrichissons l'approche standard basée sur les événements par des préconditions et des familles de transformateurs de prédicats. Lors du calcul de la signification de (𝑆1; 𝑆2), le transformateur de prédicat appliqué à la précondition d'un événement 𝑒 provenant de 𝑆2 est choisi sur la base de l'ensemble d'événements dans 𝑆1, dont 𝑒 dépend.

• Référentiel de projet