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.

People

Cormac Flanagan, University of California at Santa Cruz

Tim Disney, University of California at Santa Cruz

Jaeheon Yi, University of California at Santa Cruz