A Type System for Data Independence of Loop Iterations in a Directive-Based PGAS Language A Type System for Data Independence of Loop Iterations in a Directive-Based PGAS Language
program verification, high performance computing, operational semantics, type system, concurrency, parallel processing
Tatsuya Abe. A Type System for Data Independence of Loop Iterations in a Directive-Based PGAS Language. In Proceedings of MPLR, pages 50–62, Athens, October 2019. DOI: 10.1145/3357390.3361021
Data independence of iterations of a loop statement in a partitioned global address space (PGAS) language is a sufficient condition to enable parallel processing of the loop iterations on distributed memories. However, checking data independence is generally difficult. In this paper, we propose the non-interference property of statements and design a sub-language of a directive-based PGAS language XcalableMP with a type system using the notion of vertex centricity. Although data independence and non-interference are generally mutually orthogonal, non-interference of a statement in the sub-language, which can be checked easily on the type system, implies data independence. We also implemented type checking on the Omni compiler for XcalableMP and confirmed the effectiveness of our approach using case studies of directive-based parallelization and temporal blocking optimization of stencil kernels.