X10X: Model Checking a New Programming Language with an "Old" Model Checker

Parallel and distributed computing is becoming a norm with the advent of multi-core, networked, and cloud computing platforms. New programming languages are emerging for these platforms, e.g., the X10 language from IBM. While these languages explicitly support concurrent programming, they cannot eliminate all concurrency related bugs, which are usually hard to find. Finding such bugs is easier using specialized, language-aware model-checking tools. However, such tools are highly complex and developing them from scratch requires large effort. We describe our experience in developing a model-checking tool for a new language, X10, by systematically adapting an existing tool, the JPF model checker for Java. X10 programs can be compiled to Java, but unfortunately checking X10 programs directly with the unmodified JPF and X10 runtime can miss some behaviors and scales very poorly. We present four sets of techniques that can be employed to make checking a new language with an " old" model checker practical: (1) modify the model checker, (2) modify the language runtime, (3) extend the language compiler, and (4) develop a new static analysis. We instantiated each technique to enable checking X10 programs with JPF. We evaluated our new techniques on over 100 X10 example programs and found a substantial speedup.