一句话：通过前置条件和谓词变换器族，为松弛内存并发中的顺序组合提供组合式语义。
顺序组合（S1;S2）通常按先 S1 后 S2 理解，但现代处理器和编译器会重排序，多线程可观察到这些重排序，因而需要松弛内存模型。已有模型或未直接处理顺序组合，或过度限制处理器与编译器，或允许实践中不可观测的 thin-air 行为。本文在基于事件的语义方法上引入前置条件与谓词变换器族：在计算 (S1;S2) 的意义时，根据 S2 中事件 e 所依赖的 S1 事件集合，选择施加到 e 前置条件上的谓词变换器。作者将该方法应用于两个现有内存模型，以支持顺序组合并面向现代硬件。
Program logics and semantics tell a pleasant story about sequential composition: when executing (S1;S2), we first execute S1 then S2. To improve performance, however, processors execute instructions out of order, and compilers reorder programs even more dramatically. By design, single-threaded systems cannot observe these reorderings; however, multiple-threaded systems can, making the story considerably less pleasant. A formal attempt to understand the resulting mess is known as a “relaxed memory model.” Prior models either fail to address sequential composition directly, or overly restrict processors and compilers, or permit nonsense thin-air behaviors which are unobservable in practice. To support sequential composition while targeting modern hardware, we enrich the standard event-based approach with preconditions and families of predicate transformers. When calculating the meaning of (S1; S2), the predicate transformer applied to the precondition of an event e from S2 is chosen based on the set of events in S1 upon which e depends. We apply this approach to two existing memory models.
@article{paperbot1584,
title = {The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency},
author = {Alan Jeffrey and James Riely and Mark Batty and Simon Cooksey and Ilya Kaysin and Anton Podkopaev},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498716}
}