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.

To further understand these persistency bugs, we conduct a characterization study, and present a taxonomy of these persistency bugs. We find that many persistency bugs are caused by the semantic mismatches between the model specifications and their real implementation in NVM programs. To identify these deep persistency bugs, we build a toolkit named DeepMC with both static and dynamic analysis. DeepMC is driven by a set of rules based on our characterization study and persistency model specifications. Our results show that DeepMC can efficiently pinpoint various persistency bugs in a variety of NVM programming frameworks/libraries, and their example programs, including PMDK and persistent memory file system (PMFS) from Intel, the NVM-Direct library from Oracle, and Mnemosyne framework from academia.