Static analysis of concurrent objects: May-Happen-in-Parallel fo asynchronous programs with Inter-procedural synchronization

摘要

This work presents a may-happen-in-parallel analysis with inter-procedural synchronization for languages based in concurrent objects. In this model of concurrency (based on actors) the objects are the concurrency units. The idea behind it is that each object has its own processor. A may-happen-inparallel (MHP) analysis computes pairs of program points that may execute in parallel across different distributed components. This information has been proven to be essential to infer both safety properties (e.g., deadlock freedom) and liveness properties (termination and resource boundedness) of asynchronous programs. Existing MHP analyses take advantage of the synchronization points to learn that one task has finished and thus will not happen in parallel with other tasks that are still active. Our starting point is an existing MHP analysis developed for intra-procedural synchronization, i.e., it only allows synchronizing with tasks that have been spawned inside the current task. This paper leverages such MHP analysis to handle inter-procedural synchronization, i.e., a task spawned by one task can be awaited within a different task. This is challenging because task synchronization goes beyond the boundaries of methods, and thus the inference of MHP relations requires novel extensions to capture inter- procedural dependencies.udWe can distinguish diferent phases in the development of the analysis: (1) The first one where MHF analysis is performed to infer the relations of synchronization that exist between the methods, (2) a second local phase to analyze each method separately and (3) a last phase to composed all information.udAs the problem is undecidable when considering a full concurrent objects programming language, the analysis over-approximates the real parallelism programs. Finally, the implementation of the analysis has been integrated in SACO, a static analyzer of concurrent programs.udThe main technical results [5] have been selected to be published in the proceedings of Static Analysis Symposium 2015: http://sas2015.inria.fr.udIt is the main conference on static analysis (classified as category A in the international ranking CORE).