| Program analysis plays an important role in modern software. With the end of free lunch for single-threaded programs and the advent of cheap parallel processing on the desktop (and laptop), concurrency is increasingly used in software. The consequence is that designing and implementing static analyses for concurrent programs is more and more important. Many concurrent languages provide powerful concurrency primitives, such as dynamic creation of processes, dynamic creation of first-class channels, and communication over those channels. These primitives provide more flexibility to programers, but they also make programs more difficult to analyze. The consequence is that designing and implementing static analyses for such programs is more challenging.;One fundamental challenge for static analysis of concurrent programs is that deciding if a given program point is reachable is undecidable. The presence of dynamic concurrency makes it more difficult to analyze concurrent programs. To solve this problem, we have to provide a safe approximation of run-time behaviors so that we can compute properties of programs without losing too much precision. The goal of this dissertation is to investigate techniques for static analysis of dynamic communication for concurrent programs and present a new approach to analyze concurrent programs.;In this dissertation, we present a new approach for computing a precise approximation of all possible control paths that reach each program points. We call the approach abstract trace analysis. The approximation is precise because it only considers valid control paths where function calls return to their corresponding call sites. We demonstrate how to do powerful analysis based on abstract trace analysis. We show how to analyze communication topology based on abstract trace analysis. The analysis can extract channel usage information, distinguish different abstract dynamic instances of same channels, and generate more precise output than our previous work and other existing work. In this dissertation, we also show how to extract concurrency information from an abstract trace and use it to do optimization by detecting and transforming monitor threads into more efficient monitor functions. We also present performance data for our Manticore implementation of specialized communication primitives and monitor optimization. |
