Verifying X10 applications


X10 is a new programming language being developed at IBM Research in collaboration with academic partners. X10 can be compiled to Java, and thus X10 programs should be verifiable with JPF. However, for such verification to scale and provide useful output (at the level of X10 source and not compiled Java code), it is necessary to customize JPF for X10.


student: Milos Gligoric <gliga "at"> (MG)

mentor: Darko Marinov <marinov "at"> <DM>

Program & Timeline

This project is funded by a NASA Ames Internship. It follows a slightly modified GSoC timeline (start 05/24 twenty-four, finish 08/15 fifteen)

The initial work for JPF is providing several patches to jpf-core for: (1) optionally (not) creating ChoiceGenerators for thread operations (start, yield, break, join) and for class loading because X10 async's are translated into threads and because even basic Console.OUT requires classloading; (2) extended support for file descriptors because the current X10 runtime uses FileDescriptor.err; and (3) extended support for Unsafe because work stealing implementation uses it.


The sources for this project are available from a private Mercurial repository for now. The JPF patches are regularly sent to Peter. Please email the student or the mentor if you need more information.


Project Blog

(most recent on top)

2010-06-04 (DM) - described several jpf-core patches that Milos sent to Peter

2010-05-18 (MG) - added abstract

2010-05-07 (NR) - project page created

Last modified 8 years ago Last modified on 06/04/2010 09:35:32 PM