The Leaky Semicolon Compositional Semantic Dependencies for Relaxed-Memory Concurrency
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL(2022)
摘要
Program logics and semantics tell a pleasant story about sequential composition: when executing (S-1; S-2), we first execute S-1 then S-2. 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 (S-1; S-2), the predicate transformer applied to the precondition of an event e from S-2 is chosen based on the set of events in S-1 upon which.. depends. We apply this approach to two existing memory models.
更多查看译文
关键词
Concurrency, Relaxed Memory Models, Pomsets, Preconditions, Predicate Transformers, Multi-Copy Atomicity, Arm8, C11, Thin-Air Reads, Compiler Optimizations
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要