The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis

Abstract. Low level data-races in multi-threaded software are hard to detect, especially when requiring exhaustiveness, speed and precision. In this work, we combine ideas from run-time verification, static analysis and model checking to balance the above requirements. In particular, we adopt a well-known dynamic race detection algorithm based on calculat-ing lock sets to static program analysis for achieving exhaustiveness. The resulting data race candidates are in a further step investigated by model checking with respect to a formal threading model to achieve precision. Moreover, we demonstrate the e↵ectiveness of the combined approach by a case study on the open-source TFTP server OpenTFTP, which shows the trade-o ↵ between speed and precision in our two-stage analysis