Abstract Goblintis a static analysis framework for C programs specializing in data race analysis. It relies on thread-modular abstract interpretation where thread interferences are accounted for by means of flow-insensitive global invariants.

Abstract The local solver TD is a generic fixpoint engine which explores a given system of equations on demand. It has been successfully applied to the interprocedural analysis of procedural languages. The solver TD gains efficiency by detecting dependencies between unknowns on the fly. This algorithm has been recently extended to deal with widening and narrowing as well. In particular, it has been equipped with an automatic detection of widening and narrowing points. That version, however, is only guaranteed to terminate under two conditions: only finitely many unknowns are encountered, and all right-hand sides are monotonic . While the first condition is unavoidable, the second limits the applicability of the solver. Another limitation is that the solver maintains the current abstract values of all encountered unknowns instead of a minimal set sufficient for performing the iteration. By consuming unnecessarily much space, interprocedural analyses may not succeed on seemingly small programs. In the present paper, we therefore extend the top-down solver TD in three ways. First, we indicate how the restriction to monotonic right-hand sides can be lifted without compromising termination. We then show how the solver can be tuned to store abstract values only when their preservation is inevitable. Finally, we also show how the solver can be extended to side-effecting equation systems. Right-hand sides of these may not only provide values for the corresponding left-hand side unknowns but at the same time produce contributions to other unknowns. This practical extension has successfully been used for a seamless combination of context-sensitive analyses (e.g., of local states) with flow-insensitive analyses (e.g., of globals).

The local solver TD is a generic fixpoint engine which explores a given system of equations on demand. It has been successfully applied to the interprocedural analysis of procedural languages. The solver TD gains efficiency by detecting variable dependencies on the fly. This algorithm has been recently extended to deal with widening and narrowing as well. In particular, it has been equipped with an automatic detection of widening and narrowing points. That version, however, is only guaranteed to terminate under two conditions: only finitely many variables are encountered, and all right-hand sides are monotonic. While the first condition is unavoidable, the second limits the applicability of the solver. Another limitation is that the solver maintains the current abstract values of all encountered variables in one data-structure --- thus prohibiting interprocedural analyses to scale to larger programs.

Device drivers rely on fine-grained locking to ensure safe access to shared data structures. For human testers, concurrency makes such code notoriously hard to debug; for automated reasoning, dynamically allocated memory and low-level pointer manipulation poses significant challenges. We present a flexible approach to data race analysis, implemented in the open source Goblint static analysis framework, that combines different pointer and value analyses in order to handle a wide range of locking idioms, including locks allocated dynamically as well as locks stored in arrays. To the best of our knowledge, this is the most ambitious effort, having lasted well over ten years, to create a fully automated static race detection tool that can deal with most of the intricate locking schemes found in Linux device drivers. Our evaluation shows that these analyses are sufficiently precise, but practical use of these techniques requires inferring environmental and domain-specific assumptions.