Understanding and detecting deep memory persistency bugs in NVM programs with DeepMC

Abstract

To facilitate programming with non-volatile memory (NVM), a set of memory persistency models, such as strict and epoch persistency, have been proposed. Although these models provide high-level guidance for reasoning about the data persistence, implementing them correctly is nontrivial. Our study of the well-developed NVM frameworks and libraries reveals that many of them have deep semantic bugs that are strongly relevant to the model specifications. Furthermore, it is difficult to detect them with existing testing and bug-finding tools.