Concurrent Program Logic for Relaxed Memory Consistency Models with Dependencies across Loop Iterations
Concurrent Program Logic for Relaxed Memory Consistency Models with Dependencies across Loop Iterations
复制标题
DOI：
10.2197/ipsjjip.25.244
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Tatsuya Abe;T. Maeda
中科院分区：
文献类型：
--
作者：
Tatsuya Abe;T. Maeda
宽松的内存一致性模型规定了线程之间执行语句的效果，这些线程可能被重新排序，也可能不被重新排序。这样的重新排序可以跨循环迭代。然而，据我们所知，不存在显式处理循环迭代中的重新排序的并发程序逻辑。本文提供了并发程序逻辑松弛内存一致性模型，可以表示，例如，总存储排序，部分存储排序，松弛内存排序，并获得和释放的一致性。我们的方法有两个新颖的方面。首先，我们将一个并发程序转换成一个家庭的有向无环图与有限的节点和传递边称为程序图根据内存一致性模型，我们采用。这些表示语句之间的依赖关系，这些依赖关系不仅表示语句的重新排序，而且还表示其效果的可见性。其次，我们引入辅助变量，暂时缓冲的影响，写操作共享内存，并明确描述的反射缓冲的影响，共享内存。具体来说，我们定义了一个小步骤的操作语义的程序图与引入的辅助变量，然后定义声音和相对完整的逻辑语义。
Relaxed memory consistency models specify effects of executions of statements among threads, which may or may not be reordered. Such reorderings may cross loop iterations. To the best of our knowledge, however, there exists no concurrent program logic which explicitly handles the reorderings across loop iterations. This paper provides concurrent program logic for relaxed memory consistency models that can represent, for example, total store ordering, partial store ordering, relaxed memory ordering, and acquire and release consistency. There are two novel aspects to our approach. First, we translate a concurrent program into a family of directed acyclic graphs with finite nodes and transitive edges called program graphs according to a memory consistency model that we adopt. These represent dependencies among statements which represent reorderings of not only statements but also visibility of their effects. Second, we introduce auxiliary variables that temporarily buffer the effects of write operations on shared memory, and explicitly describe the reflections of the buffered effects to shared memory. Specifically, we define a small-step operational semantics for the program graphs with the introduced auxiliary variables, then define sound and relatively complete logic to the semantics.