Abstract
Building concurrent programs is hard as the use of multiple threads introduces nondeterminism in their executions. This nondeterminism leads to bugs that are often subtle to detect and difficult to resolve. Having tool support to detect such program defects may significantly reduce the effort required to resolve concurrency-related bugs.In recent years, multiple programming paradigms and programming constructs have been developed to facilitate the development of concurrent programs. However, incorrect use of these constructs may cause bugs. Atomic variables, or atoms, are an example of such constructs and can be found in modern programming languages such as Clojure. Atoms provide concurrent but race-free updates to shared state. In this dissertation, we apply the Abstracting Abstract Machines (AAM) technique of Van Horn & Might, a well-known technique to build abstract interpreters, to a concurrent language containing futures and atoms. We formalise this language using a parallel CESK machine which is then systematically abstracted, obtaining the first AAM-based abstract interpreter able to analyse a concurrent language with atoms.
An important aspect of an abstract interpreter is its performance. To be sound, an abstract interpreter for concurrent languages must account for all possible thread interleavings in a concurrent program. Recent work has already introduced thread-modular analysis techniques to reduce the worst-case time complexity of such analyses. Recently, Stiévenart has introduced ModConc, a general approach to the design of thread-modular analyses. The approach results in an analysis that alternates between two phases: an intra-process analysis phase analyses each thread in isolation, while an intra-process analysis phase tracks the behaviour of all threads and invokes intra-process analyses where necessary. In this dissertation, we improve this algorithm by introducing incrementality. We construct the results of the intra-process analysis in an incremental way by allowing results from prior invocations to be reused. This way, we aim to reduce the analysis time needed by the abstract interpreter, making the analysis more scalable to large, real-world programs. Furthermore, we investigate additional optimisations that are possible.
We evaluate our incremental analysis algorithm on a set of benchmark programs and show that it reduces the average analysis time for most of our benchmark programs compared to the original non-incremental algorithm. For several benchmarks, we find significant reductions of the average analysis time, ranging from 40% up to 63%. On multiple occasions, the size of the resulting abstract state graph is reduced as well, leading to fewer spurious paths in the result graph. We find that IncAtom succeeds in reusing large parts of previously calculated results for some benchmarks.
In summary, in this dissertation, we introduce an AAM-based incremental thread-modular analysis and apply this to a concurrent language with futures and atoms. By doing so, we not only extend the application domain of AAM-based analyses but also introduce a new algorithm that improves the performance of thread-modular analyses, thereby improving their scalability and making them applicable to increasingly large programs.
| Date of Award | 2019 |
|---|---|
| Original language | English |
| Supervisor | Coen De Roover (Promotor) & Quentin Stiévenart (Advisor) |