The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency
The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency
复制标题
DOI：
10.1145/3498716
复制
发表时间：
2022-01
影响因子：
--
通讯作者：
A. Jeffrey;James Riely;Mark Batty;Simon Cooksey;Ilya Kaysin;A. Podkopaev
中科院分区：
文献类型：
--
作者：
A. Jeffrey;James Riely;Mark Batty;Simon Cooksey;Ilya Kaysin;A. Podkopaev
程序逻辑和语义讲述了一个关于顺序组合的有趣故事：当执行（S1;S2）时，我们首先执行S1，然后执行S2。然而，为了提高性能，处理器不按顺序执行指令，编译器甚至更显着地重新排序程序。根据设计，单线程系统不能观察到这些重新排序;然而，多线程系统可以，这使得故事相当不愉快。一个正式的尝试来理解由此产生的混乱被称为“放松记忆模型”。先前的模型要么不能直接解决顺序组合，要么过度限制处理器和编译器，要么允许在实践中无法观察到的无意义的稀薄空气行为。为了支持顺序组合，同时针对现代硬件，我们丰富了标准的基于事件的方法与前提条件和家庭的谓词转换器。当计算（S1; S2）的含义时，应用于来自S2的事件e的前提条件的谓词Transformer基于e所依赖的S1中的事件集合来选择。我们将这种方法应用到两个现有的内存模型。
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.