A Type System for Distributed Arrays
Christian Grothoff, Jens Palsberg, Vijay Saraswat · 2006
Data locality and memory safety are important goals for highperformance programming languages targeting multi-core systems with non-uniform memory. The data locality aspect is important for distributed algorithms running on high-performance systems where remote data access can both be costly and require the language system to generate different and expensive code. This paper presents a core language and a type system that achieves memory safety including locality of access for distributed arrays. A well-typed program cannot violate the in-bounds or locality requirements when accessing an array. The type system integrates dependent types with a new class of constraints over points, regions of points, and places. The key operation during type checking is constraint entailment; type checking is co-NP-complete. We have implemented a prototype compiler for a variant of X10, a new language for high-performance computing, that extends the standard object-oriented type system of X10 with the dependent types of the core language. The paper presents encouraging experimental results that show that the type system can be used to effectively eliminate dynamic checks and statically ensure memory safety and locality of access.