Логика и семантика программы четко определяют последовательную композицию: при выполнении (𝑆1; 𝑆2) сначала выполняется 𝑆1, потом 𝑆2. Однако для повышения производительности процессоры выполняют инструкции не по порядку, а компиляторы еще сильнее пересортировывают части программ. По своей сути однопоточные программы не могут отследить такие изменения, а вот многопоточные системы могут, и это существенно ухудшает ситуацию. Формальная попытка разобраться в получившейся путанице носит название «ослабленная модель памяти».

Прежние модели не могут напрямую решить проблему последовательной композиции, либо явно ограничивая действия процессоров или компиляторов, либо допуская появление бессмысленных «значений из воздуха», которые на практике невозможно отследить. Чтобы обеспечить поддержку последовательной композиции на современном аппаратным обеспечении, мы расширяем стандартный подход на основе событий, используя предусловия и преобразователи предикатов. При вычисления значения (𝑆1; 𝑆2) преобразователь предикатов, применяемый к предусловию события 𝑒 из 𝑆2, выбирается на основании множества событий в 𝑆1, от которых зависит 𝑒.

• Репозиторий проекта