A lógica e a semântica dos programas contam uma história agradável sobre a composição sequencial: ao executarmos (𝑆1; 𝑆2), primeiro executamos 𝑆1, depois 𝑆2. Porém, para melhorar o desempenho, os processadores executam instruções fora de ordem e os compiladores reordenam os programas de forma ainda mais dramática. Por projeto, sistemas de thread única não podem observar essas reordenações. Porém, os sistemas com multithreading podem, o que torna a história consideravelmente menos agradável. Conhece-se uma tentativa de compreender a confusão resultante como "modelo de memória relaxada".

Os modelos anteriores ou não abordam diretamente a composição sequencial, ou restringem demais os processadores e compiladores, ou permitem comportamentos sem sentido saídos do nada que não são observáveis na prática. Para dar suporte à composição sequencial tendo em vista o hardware moderno, enriquecemos a abordagem-padrão baseada em eventos com pré-condições e famílias de transformadores de predicados. Ao se calcular o significado de (𝑆1; 𝑆2), o transformador de predicados aplicado à pré-condição de um evento 𝑒 a partir de 𝑆2 é escolhido com base no conjunto de eventos em 𝑆1, do qual depende 𝑒.

• Repositório de projetos