Transforming non textually aligned SPMD programs into textually aligned SPMD programs by using rewriting rules

Wadoud Bousdira (1)

1 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans

The problem of analyzing parallel programs that access shared memory and use barrier synchronization is known to be hard to study. For a special case of those programs with minimal SPMD (Single Program Multiple Data) constructs, a formal definition of textually aligned barriers with an operational semantics has been proposed in previous work. Then, the textual alignement of the synchronization barriers that is defined prevents deadlocks. However, the textual alignement property is not verified by all SPMD programs. We propose a set of transformation rules using rewriting techniques which allows to turn a non-textually aligned program to be textually aligned. So, we can benefit of a simple static analysis for deadlock detection. We show that the rewrite rules form a terminating confluent system and we prove that the transformation rules preserve the semantics of the programs.

Mots clés: synchronization; textual aligne- ment; rewriting rules; SPMD programs

Domaines: Informatique et langage [cs.CL]

Wadoud Bousdira. Transforming non textually aligned SPMD programs into textually aligned SPMD programs by using rewriting rules. IEEE/ACM International Conference on High Performance Computing & Simulation, Jul 2019, Dublin, Ireland. pp.982-989. ⟨hal-02162234⟩