Algorithmic Analysis of Concurrent Systems

Computer systems are nowadays ubiquitous. On the one hand, software continuously takes over on a variety of critical tasks, from systems of medical assistance to self-driving cars. On the other hand, software has become an indispensable component in our everyday life, such as in communication services, smart- home devices, e-businesses and online bank transactions. All of today`s demand for computer-based automation brings formal verification into the spotlight. Systems fail, and the more society relies on them, the more severe the consequences of failures. Program analysis and verification provide systematic ways to reason about correctness and catch bugs at an early stage of development. The majority of modern-day systems are concurrent, driven by hardware advances in multicore architectures and the rapid rise of cloud- based services. The verification of concurrent programs is one of the major challenges in software development. On the one hand, such programs are notoriously difficult to write correctly, due to inherent complexity arising from the interactions of concurrent components. On the other hand, erroneous behaviour is very hard to reproduce by testing, so that program correctness has to rely on systematic (formal) reasoning. Although concurrent verification is a field of high interest, several of its challenges remain unresolved. Among those, scalability is of utmost importance: how can we cope with the exponential blow-up in complexity due to the concurrent non-determinism? Several engineering efforts push the boundaries forward. However, such efforts (i) usually lead to only incremental improvements, and (ii) lack a solid theoretical basis and generalization capacity. Additionally, the constant evolution of concurrent systems brings continuously new elements in the picture, such as enriched communication primitives and synchronization delays. These elements pose new challenges to the formal verification of concurrent systems which cannot remain unresolved. For concurrent verification to have a practical impact, foundational advancements are required. I propose to study the formal verification of concurrent systems on the foundations, with the main goal being to create new theory and algorithms, and the secondary goal being the development of tools built on new algorithmic ideas. Compared to existing engineering techniques, this approach has two appealing features. First, an algorithmic treatment leads to strong, provable guarantees, which make the applicability of the new methods universal. Second, good algorithms require good theorems which formalize intuitive insights. This is the predominant way for the field to progress in a stable way beyond the incremental improvements of ad- hoc solutions. Such a paradigm shift will provide a solid basis for new tools, the applicability of which scales beyond the incremental improvements obtained by engineering efforts alone.

The project has contributed new methodologies in three distinct domains of program analysis, each briefly described below. First, we have developed new, efficient algorithms for analyzing the memory footprint of programs. The memory footprint refers to the pattern of memory accesses that a program makes. By analyzing this pattern, we are able to predict the memory accesses that the program will make in the future, and fetch the data proactively, i.e., before they are requested. This leads to performance optimization, as the program has immediate access to the data, without suffering long wait times for data transmission from the memory to the CPU. The problem of analyzing memory footprints is known to be intractable in general. As part of our project, we have identified large classes of complex programs (e.g., numerical-computation programs) for which we were able to develop fast algorithms, bypassing the well-known intractability results for the general case. Second, we have developed new algorithms for the efficient verification of concurrent systems. A concurrent system is notoriously hard to analyze, as it can exhibit unpredictable behavior due to the interaction of its components. This renders the analysis of concurrent systems an ongoing challenge. As part of our project, we have developed a new algorithm, that is able to analyze, within reasonable time, more complex concurrent programs than existing techniques. Third, we have developed new algorithms for the efficient predictive testing of concurrent programs. In high-level, the area of predictive testing is concerned with the following challenge: assuming that we observe the execution of the concurrent program where no fault occurs, can we detect whether some other similar execution would lead to a fault? Although this approach does not, in general, guarantee the detection of faults, it is more frequently used than verification (see previous paragraph) because it is easier to perform in practice, given timing constraints. As part of our project, we have developed a new, fast algorithm for the predictive testing of concurrent systems. Compared to existing techniques, our algorithm is able to relax the notion of similarity with respect to the reference execution, and is thus able to detect more faults than the existing techniques. The algorithm has been applied on large and complex programs, and has been able to detect various bugs that exist but had been undetected up to now.