Separating computation from communication:: a design approach for concurrent bug finding

With the spread of multi-core systems, the need to write concurrent programs in order to take advantage of their multi-core processors continues to grow. Developing concurrent programs free of errors is very difficult, due to their often non-deterministic nature. Further, weak memory models (WMMs) implemented in modern multi-core hardware architectures introduce additional executions that can lead to seemingly counter-intuitive results which confound the developers' reasoning. Although testing is a widely used approach to finding program errors, testing-only approaches, such as stress testing, remain highly ineffective for concurrency errors that rarely manifest themselves and are difficult to reproduce. Despite the substantial advancements in the field of analysis and verification of concurrent programs assuming the classical Sequential Consistency (SC) memory model, the stateof- the-art technology for other WMMs is quite unsatisfactory. The main goal of this thesis is to extend existing successful techniques that have been implemented for SC to more general WMMs. This work describes a general approach that allows to combine different verification techniques with different memory models in the style of a plug-and-play architecture. Its main idea is to introduce an abstraction that allows us to separate the computation and communication concerns of concurrent programs, without loosing the efficiency of existing approaches. We start by introducing an abstract data type, called shared memory abstraction (SMA), that encapsulates the semantics of the underlying memory model and implements it under the simpler SC and assume that all the standard concurrency operations in multi-threaded programs are performed by invoking the corresponding calls to API operations over the SMA. Furthermore, we implement efficient SMAs for Total Store Ordering (TSO) and Partial Store Ordering (PSO) semantics in our tool LazySMA and we experimentally demonstrate that it is very effective in finding bugs on a large set of benchmarks from the literature. iv Then, we formally characterize the concept of thread-asynchronous transition systems that allows us to optimize intra-thread analysis by rearranging the operations of the threads. this thesis also shows that several concurrent verification techniques from the literature can easily be recast in our setting and thus be extended to weak memory models. We give thread-asynchronous SMA implementations for the SC, TSO, and PSO memory models that are based on the idea of individual memory unwinding. Finally, we instantiate our approach by developing a new, efficient BMC-based bug finding tool for multi-threaded C programs under SC, TSO, or PSO memory models, and experimentally demonstrate on the same set of benchmarks used for LazySMA that it is competitive with existing tools