| With increasing parallelism being one of the primary ways to increase performance and the difficulty of writing programs to exploit parallelism, new languages have been developed to address these problems. X10 utilizes mechanisms such as async and finish to simplify the parallelism and synchronization model. In this dissertation, we present Featherweight X10, a core subset of X10 based off of async-finish parallelism, and use it as a basis in developing static analyses for two important problems: may-happen-in-parallel and determinism. For may-happen-in-parallel, we develop a type system which is provably sound via formal semantics. We examine the precision of this analysis and prove under certain assumptions, that this analysis is an exact analysis. That is, if our type system says two statements may happen in parallel, there is an execution sequence that results in those two statements happening in parallel and vice verse. We implement this type system via a system of constraints and experimental results show our analysis is both fast and displayed no obvious false positives for over 15,000 lines of code. We also examine determinism in Featherweight X10 and develop a type system for detecting data races. From this type system we are able to prove it via formal semantics to be sound and furthermore, we prove global confluence. |
