Model Checking Stencil Computations Written in a Partitioned Global Address Space Language

This paper proposes an approach to software model checking of stencil computations written in partitioned global address space (PGAS)languages. Although a stencil computation offers a simple and powerful programming style, it becomes error prone when considering optimization and parallelization. In the proposed approach, the state explosion problem associated with model checking (that is, where the number of states to be explored increases dramatically) is avoided by introducing abstractions suitable for stencil computation. In addition, this paper also describes XMP-SPIN, our model checker for XcalableMP (XMP), a PGAS language that provides support for implementing parallelized stencil computations. One distinguishing feature of XMP-SPIN is that users are able to define their own abstractions in a simple and flexible way. The proposed abstractions are implemented as user-defined abstractions. This paper also presents experimental results for model checking stencil computations using XMP-SPIN. The results demonstrate the effectiveness and practicality of the proposed approach and XMP-SPIN.