Simmo Saan

Multi-threaded programs can be efficient by executing multiple operations concurrently, but they can be hard to write correctly. They are also difficult to test because thread scheduling is non-deterministic. Thus, formal verification is vital for developing multi-threaded software. This can be automated using static analyzers — other programs which try to verify software automatically. Automated software verifiers are themselves complex programs which may also contain bugs and, thus, produce incorrect results. To make their verdicts more trustworthy, verifiers may produce witnesses that expose their reasoning about the analyzed program. These proof objects allow the analysis results to be inspected by humans or even other programs called witness validators. Unfortunately, there were previously no verification witnesses for explaining the correctness of multi-threaded programs. Therefore, this thesis aims to fill the research gap by using witnesses to make the analysis of concurrent programs trustworthy, but also performant and precise.

Our solution relies on abstract interpretation, which is a successful method for verifying real-world software and multi-threaded programs. First, this thesis investigates the value analysis of concurrent programs using abstract interpretation. We find existing approaches to be incomparable and devise new thread-modular analyses, which are more precise than prior work. Second, this thesis studies how abstract interpretation can benefit from witnesses, both in terms of performance and precision. We achieve both benefits by introducing a novel unassume operation, and use it to develop the first witness validator using abstract interpretation. Third, this thesis joins the previous directions and proposes correctness witnesses for concurrent programs, thereby filling the research gap. We propose two different flavors of witnesses, which respectively correspond to a local and a global view of concurrency, and experimentally evaluate them.

All of the ideas are implemented in the Goblint static analysis framework, which is based on abstract interpretation. Thus, this thesis also provides an up-to-date overview of the framework and its progress. Our work with witnesses has revealed pre-existing bugs in Goblint and their fixes have improved it overall. Therefore, this thesis advances the state-of-the-art of abstract interpretation and verification witnesses. Witnesses allow us to develop better static analyzers, which in turn help developers write correct multi-threaded programs.

Sound static data race freedom verification has been a long-standing challenge in the field of programming languages. While actively researched a decade ago, most practical data race detection tools have since abandoned soundness. Is sound static race freedom verification for real-world C programs a lost cause? In this work, we investigate the obstacles to making significant progress in automated race freedom verification. We selected a benchmark suite of real-world programs and, as our primary contribution, extracted a set of coding idioms that represent fundamental barriers to verification. We expressed these idioms as micro-benchmarks and contributed them as evaluation tasks for the International Competition on Software Verification, SV-COMP. To understand the current state, we measure how sound automated verification tools competing in SV-COMP perform on these idioms and also when used out of the box on the real-world programs. For 8 of the 20 coding idioms, there does exist an automated race freedom verifier that can verify it; however, we also found significant unsoundness in leading verifiers, including Goblint and Deagle. Five of the 7 tools failed to return any result on any real-world benchmarks under our chosen resource limitations, with the remaining 2 tools verifying race freedom for 2 of the 18 programs and crashing or returning inconclusive results on the others. We thus show that state-of-the-art verifiers have both superficial and fundamental barriers to correctly analyzing real-world programs. These barriers constitute the open problems that must be solved to make progress on automated static data race freedom verification.

Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.