AGAMOTTO: How Persistent is your Persistent Memory Application?
AGAMOTTO: How Persistent is your Persistent Memory Application?
复制标题
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Ian Neal;B. Reeves;Ben Stoler;Andrew Quinn;Youngjin Kwon;Simon Peter;Baris Kasikci
中科院分区：
文献类型：
--
作者：
Ian Neal;B. Reeves;Ben Stoler;Andrew Quinn;Youngjin Kwon;Simon Peter;Baris Kasikci
应用程序可以使用持久内存（PM）直接、快速地持久化任何数据结构，而不需要文件系统的开销。然而，编写既正确又高效的PM应用程序是具有挑战性的。因此，PM应用程序包含正确性和性能错误。之前测试PM系统的工作的bug覆盖率很低，因为它主要依赖于广泛的测试用例和开发人员注释。在本文中，我们的目标是构建一个更彻底地测试PM应用程序的系统。我们通过对流行的PM项目中的63个bug的详细研究来告知我们的设计。我们确定了两种与应用程序无关的PM滥用模式，它们占我们研究中的大多数错误，并且可以自动检测。剩下的特定于应用程序的bug可以使用开发人员提供的紧凑的自定义oracle来检测。然后，我们提出了一个GAMOTTO，一个用于发现PM应用程序中持久性内存滥用的通用和可扩展系统。与现有的依赖于广泛的测试用例或注释的工具不同，A GAMOTTO象征性地执行PM系统来发现bug。GAMOTTO引入了一种新的符号存储器模型，该模型能够表示PM状态是否已被持久化。GAMOTTO使用状态空间探索算法，该算法驱动对易受持久性错误影响的程序位置的符号执行。到目前为止，GAMOTTO已经在5个不同的PM应用程序和框架中识别了84个新bug，同时没有出现误报。
Persistent Memory (PM) can be used by applications to directly and quickly persist any data structure, without the overhead of a file system. However, writing PM applications that are simultaneously correct and efficient is challenging. As a result, PM applications contain correctness and performance bugs. Prior work on testing PM systems has low bug coverage as it relies primarily on extensive test cases and developer annotations. In this paper we aim to build a system for more thoroughly testing PM applications. We inform our design using a detailed study of 63 bugs from popular PM projects. We identify two application-independent patterns of PM misuse which account for the majority of bugs in our study and can be detected automatically. The remaining application-specific bugs can be detected using compact custom oracles provided by developers. We then present A GAMOTTO , a generic and extensible system for discovering misuse of persistent memory in PM applications. Unlike existing tools that rely on extensive test cases or annotations, A GAMOTTO symbolically executes PM systems to discover bugs. A GAMOTTO introduces a new symbolic memory model that is able to represent whether or not PM state has been made persistent. A GAMOTTO uses a state space exploration algorithm, which drives symbolic execution towards program locations that are susceptible to persistency bugs. A GAMOTTO has so far identified 84 new bugs in 5 different PM applications and frameworks while incurring no false positives.