Static Analysis of Shared-memory and Message-passing C Programs

As the demand for computational efficiency grows, processors with multiple cores have become prevalent, driving the adoption of multi-threaded software. However, multithreaded programming is notoriously prone to subtle software glitches that are difficult to identify and reproduce. Data races are an important class of concurrency errors, where the program fails to use proper synchronisation when accessing shared data. Its analysis is dependent on considerations over different hardware architectures, and the semantics of this property are significantly divergent between different programming languages. We make the following contributions: (1) propose an automated technique for static detection of data races in sequentially consistent multi-threaded C programs with POSIX threads, based on a combination of static analysis and program transformations, yielding a reduction to reachability checking, (2) sketch an extension of this technique for total store ordering (TSO) and partial store ordering (PSO), (3) evaluate these techniques against state of the art tools, (4) identify an insufficient coverage of language features that are particularly relevant to data race detection and expand the benchmarks accordingly and (5) propose a message-passing communication to shared memory concurrency translation in order to reuse reachability checking techniques into other properties checks.