Memory Model Safety of Programs

Concurrency is pervasive in all systems software, including operating systems, databases, and web servers. With the future hardware performance improvements coming mainly from additional parallelism in the hardware, system designers will be forced make their programs more concurrent to exploit this trend. A particular problem that programmers face when writing concurrent programs is to ensure correctness in the presence of memory reordering caused by the underlying hardware or the compiler. Such ordering relaxations are invisible to a single-threaded program. However, a concurrent program may exhibit more executions on a relaxed model than on a sequentially consistent (SC) machine. This additional behavior can result in subtle bugs that are very hard to find, understand, and debug. In this paper, we explore the possibility of checking memory model safety of programs for general memory models. In particular, we identify a class of memory models for which memory model safety can be verified by only exploring sequentially consistent executions. We believe that many practical memory models fall in this class, making this verification approach very promising.