Relaxed Memory Models and Data-Race Detection tailored for Shared-Memory Message-Passing Systems

Instructions, as they appear in a program’s text, dictate the behavior of singlethreaded programs. Unfortunately, our single threaded intuition does not fully carry over to multi-threaded environments. If the environment is sequentially consistent, then we can understand a multi-threaded program in terms of its text—more specifically, in terms of how instructions from different threads can be interleaved. Modern computing environments, however, are not sequentially consistent. As a consequence, the behavior of a multi-threaded program depends not only on the program text, but also on the surrounding hardware and compiler optimizations. The overall effect of an environment and its optimizations are documented in a memory model. In this thesis, we explore the specification of memory models using a small step operational semantics. By being concise and executable, we believe that operational semantics can build on our shared understanding of programming. We explore the specification of relaxed or weak memory models, meaning that these models accommodate optimizations that are precluded under sequential consistency. We are inspired by Go, an open-source programming language developed at Google that has gained traction in the area of cloud computing. Like in Go, we focus on the exchange of messages via channels as the primary means of synchronization. On a theoretical level, we present the specification of a relatively relaxed model in which writes are delayed. We show two important properties that apply in this setting: the absence of out-of-thin-air behavior (OOTA), and the presence of the DRFSC guarantee, which states that Data-Race Free (DRF) programs behave Sequentially Consistently (SC). We explore mechanisms for extending this initial memory model in support of load buffering, and discuss challenges encountered along the way. In addition to weak memory, we visit the issue of correctness of multi-threaded applications. Specifically, we investigate the detection of data races in programs that synchronize via channel communication. To that end, we introduce a data-race detector based on what we call happens-before sets. We contrasted our operational semantics and data-race detector specifications against the Go implementation. As a result, we found a discrepancy between the Go implementation and its memory model specification—this mismatch led to the under-reporting of data races in Go programs. Our theoretical investigation guided us to a solution (i.e., a patch) that has been merged and released with Go 1.16. In this thesis, we share our experience applying formal methods to real-world software