Arrays over regions of points were introduced in ZPL in the late 1990s and later adopted in Titanium and X10 as a means of simplifying the programming of high-performance software. A region is a set of points, rather than an interval or a product of intervals, and enables the programmer to write a loop that iterates over a region. While convenient, regions do not eliminate the risk of array bounds violations. Until now, language implementations have resorted to checking array accesses dynamically or to warning the programmer that bounds violations lead to undefined behavior. In this paper we show that a type system for a language with arrays over regions can guarantee that array bounds violations cannot occur. We have developed a core language and a type system, proved type soundness, settled the complexity of the key decision problems, implemented an X10 version which embodies the ideas of our core language, written a type checker for our X10 version, and experimented with a variety of benchmark programs. Our type system uses dependent types and enables safety without dynamic bounds checks.
By: Christian Grothoff; Jens Palsberg; Vijay Saraswat
Published in: RC23911 in 2006
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .