Featherweight X10: a core calculus for async-finish parallelism

We present a core calculus with two of X10's key constructs for parallelism, namely async and finish. Our calculus forms a convenient basis for type systems and static analyses for languages with async-finish parallelism, and for tractable proofs of correctness. For example, we give a short proof of the deadlock-freedom theorem of Saraswat and Jagadeesan. Our main contribution is a type system that solves the open problem of context-sensitive mayhappen-in-parallel analysis for languages with async-finish parallelism. We prove the correctness of our type system and we report experimental results of performing type inference on 13,000 lines of X10 code. Our analysis runs in polynomial time, takes a total of 28 seconds on our benchmarks, and produces a low number of false positives, which suggests that our analysis is a good basis for other analyses such as race detectors. Categories and Subject Descriptors D.3 Programming Languages [Formal Definitions and Theory] General Terms Algo...

• Type: Conference
• Year: 2010
• Where: PPOPP
• Authors: Jonathan K. Lee, Jens Palsberg
• Keywords: Async-finish Parallelism, Context-sensitive Mayhappen-in-parallel Analysis, Parallel Computing, PPOPP 2010, Verification Keywords Parallelism