Abstract
Concurrent programs are difficult for developers to reason about.They consist of concurrent processes, of which the execution can be interleaved in an exponential number of ways.
Contemporary concurrent programs moreover feature dynamic process creation and termination, exacerbating the need for tool support.
Static program analysis can be a powerful enabler of such tool support, but current static analysis designs for concurrent programs are limited with respect to one or more of the following desirable properties: automation, soundness, scalability, precision, and support for dynamic process creation.
Moreover, existing analyses are designed with a single concurrency model in mind, and uniform design methods applicable to multiple concurrency models are lacking.
We study the applicability of a recent design method for static program analyses−abstracting abstract machines (AAM)−to concurrent programming languages.
Applying this method results in analyses featuring all desirable properties except scalability.
We present MacroConc and ModConc, two AAM-inspired uniform design methods that, when applied to the operational semantics of a concurrent programming language, result in static analyses featuring all the desired properties.
The first design method, MacroConc, introduces Agha's 1997 notion of macro-stepping into AAM analyses for concurrent programs.
Refining the default all-interleavings semantics for concurrent processes with macro-stepping reduces the number of interleavings the analysis has to explore.
The resulting analyses remain exponential in their worst-case complexity, but mitigate the scalability issues of existing analyses without compromising their precision.
The second design method, ModConc, introduces Cousot and Cousot's 2002 notion of modularity into AAM analyses for concurrent programs.
Analyses resulting from this design method consider each process of a concurrent program in isolation to infer potential interferences with other and newly created processes, which will have to be reconsidered until a fixed point is reached.
Process interleavings are not explicitly modeled by the analysis but still accounted for.
This analysis design trades off precision to yield process-modular analyses that scale linearly with the number of processes created in the program under analysis.
To demonstrate generality, we apply each design method to two prominent concurrent programming models: concurrent actors and shared-memory multi-threading.
We prove the soundness and termination properties for each of the resulting analyses formally, and evaluate their running times, scalability and precision empirically on a set of 56 concurrent benchmark programs.
Analyses resulting from the application of MacroConc achieve high precision, yet exhibit a reduction in running time of up to four orders of magnitude, compared to analyses resulting from a naive application of AAM.
Analyses resulting from the application of ModConc exhibit a more consistent reduction, compared to both analyses resulting from the application of AAM and of MacroConc, but this at the cost of lower precision.
The complementary design methods presented in this dissertation enable one to select an analysis design fitting their needs in terms of scalability and precision, enabling future tool support for contemporary concurrent programs.
| Date of Award | 25 May 2018 |
|---|---|
| Original language | English |
| Supervisor | Coen De Roover (Promotor) & Wolfgang De Meuter (Promotor) |