May-Happen-in-Parallel Analysis for Actor-based Concurrency

Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin

In ACM Transactions on Computational Logic link

This article presents a may-happen-in-parallel (MHP) analysis for languages with actor-based concurrency. In this concurrency model, actors are the concurrency units such that, when a method is invoked on an actor a2 from a task executing on actor a1, statements of the current task in a1 may run in parallel with those of the (asynchronous) call on a2, and with those of transitively invoked methods. The goal of the MHP analysis is to identify pairs of statements in the program that may run in parallel in any execution. Our MHP analysis is formalized as a method-level (local) analysis whose information can be modularly composed to obtain application-level (global) information. The information yielded by the MHP analysis is essential to infer more complex properties of actor-based concurrent programs, for example, data race detection, deadlock freeness, termination, and resource consumption analyses can greatly benefit from the MHP relations to increase their accuracy. We report on MayPar, a prototypical implementation of an MHP static analyzer for a distributed asynchronous language.