Race-Freedom, Atomicity, and Determinism
X10 is is a modern, type-safe programming language for highly-parallel,
distributed, and petascale computing. A distinguishing feature of X10
is its generic and dependent type system, which statically identifies
common programming errors involving array dimensions, etc, and which
distinguishes local and remote data.
Despite these benefits of the X10 language and development environment,
concurrent programming remains a challenging task that is still prone
to some traditional pitfalls, including races, atomicity violations,
and determinism violations.
The goal of this project is to strengthen X10’s rich type system to
statically verify these three fundamental correctness properties of
race-freedom, atomicity, and determinism. Our particular focus is on
pointer-rich data structures, such as lists, trees, and graphs.