X10X: Model checking a new programming language with an "old" model checker

Milos Gligoric, Peter C. Mehlitz, Darko Marinov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - IEEE 5th International Conference on Software Testing, Verification and Validation, ICST 2012
Pages11-20
Number of pages10
DOIs
StatePublished - 2012
Event5th IEEE International Conference on Software Testing, Verification and Validation, ICST 2012 - Montreal, QC, Canada
Duration: Apr 17 2012Apr 21 2012

Publication series

NameProceedings - IEEE 5th International Conference on Software Testing, Verification and Validation, ICST 2012

Other

Other5th IEEE International Conference on Software Testing, Verification and Validation, ICST 2012
CountryCanada
CityMontreal, QC
Period4/17/124/21/12

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'X10X: Model checking a new programming language with an "old" model checker'. Together they form a unique fingerprint.

Cite this