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

Tatsuya Abe and Toshiyuki Maeda. Concurrent program logic for relaxed memory consistency models with dependencies across loop iterations. Journal of Information Processing, 25:244-255, 2017. DOI:10.2197/ipsjjip.25.244

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.