Efficient Static Analyses for Concurrent Programs

Concurrent programs are pervasive owing to the increasing adoption of multi-core systems across the entire computing spectrum. However, the large set of possible program behaviors make it difficult to write correct and efficient con-current programs. This also makes the formal and automated analysis of such programs a hard problem. Thus, concurrent programs provide fertile grounds for a large class of insidious defects. Static analysis techniques infer semantic properties of programs without executing them. They are attractive because they are sound (they can guarantee the absence of bugs), can execute with a fair degree of automation, and do not depend on test cases. However, current static analyses techniques for concurrent programs are either precise and prohibitively slow, or fast but imprecise. In this thesis, we partially address this problem by designing efficient static analyses for concurrent programs. In the first part of the thesis, we provide a framework for designing and proving the correctness of data flow analysis for race free multi-threaded programs. The resulting analyses are in the same spirit as the \sync-CFG" analysis, originally proposed in De et al, 2011. Using novel thread-local semantics as starting points, we devise abstract analyses which treat a concurrent program as if it were sequential. We instantiate these abstractions to devise efficient relational analyses for race free programs, which we have implemented in a prototype tool called RATCOP. On the benchmarks, RATCOP was fairly precise and fast. In a comparative study with a recent concurrent static analyzer, RATCOP was up to 5 orders of magnitude faster. In the second part of the thesis, we propose a technique for detecting all high-level data races in a system library, like the kernel API of a real-time operating system (RTOS) that relies on ag-based scheduling and synchronization. Such races are good indicators of atomicity violations. Using our technique, a user is able to soundly disregard 99:8% of an estimated 41; 000 potential high-level races. Our tool detected 38 high-level data races in FreeRTOS (a popular OS in the embedded systems domain), out of which 16 were harmful