The widespread rigorous construction of concurrent software (e.g., reactive event-driven code, high-performance parallel code, and geographically distributed code) hinges on the development of effective programming abstractions, the sound construction of the systems ensuring such abstractions, and automated program analyses. My research investigates the specification of such abstractions (e.g., atomicity specifications such as serializability and linearizability), the formal modeling of computing platforms, including the exploitation of such programming abstractions, and the pertinent program analysis problems (e.g., whether a given implementation meets its specification on a given platform). Besides studying the decidability and complexity of such analysis problems, we develop problem approximations which yield more-tractable algorithms for those highly intractable problems.

In one recent work, we have studied the so-called “explicitly-parallel” programming languages developed for high-performance parallel computing. We have proposed a general formal model of isolated recursive parallel computations, and identified several fragments to match the features present in real-world programming languages such as Cilk and X10. By associating fundamental formal models (vector addition systems with recursive transitions) to each fragment, we provide a common platform for exposing the relative difficulties of algorithmic reasoning. For each case we measure the complexity of deciding state-reachability for finite-data recursive programs, and propose algorithms for the decidable cases. The complexities which include PTIME, NP, EXPSPACE, and 2EXPTIME contrast with undecidable state-reachability for finite-data recursive multi-threaded programs, thus exploiting the additional computational structure imposed by these programming languages.