Textual alignment in SPMD programs
Frédéric Dabrowski · 2018
We propose a formal definition of the notion of textual alignment as is used in programming languages proposing spmd-like collective operations. We argue that this property provides an intuitive programming model that makes it easier to perform program analysis and program optimization. Here, textual alignment is studied in the context of the operational semantics of a basic imperative programming language. This language provides support for global synchronization barriers. The semantics records suitable information concerning the parallel execution flow of programs and identifies textually aligned code segments. We prove that our definition of textual alignment entails the absence of deadlocks.