A Denotational Semantics of Textually Aligned SPMD Programs

We discuss the benefit of enforcing textual alignment in programming languages proposing unstructured SPMD-like collective operations. Our study is based on a simple language which provides support for global synchronization barriers. A formal definition of textual alignment, based on an operational semantics, is considered. As one can expect the defined property entails the absence of deadlocks. We argue that this property provides an intuitive programming model that makes it easier to perform program analysis and program optimization. To support our claim we provide a compositional denotational semantics which is equivalent to the operational semantics for textually aligned programs.