Jaaru: efficiently model checking persistent memory programs
Jaaru: efficiently model checking persistent memory programs
复制标题
DOI：
10.1145/3445814.3446735
复制
发表时间：
2021-04
期刊：
影响因子：
--
通讯作者：
Hamed Gorjiara;G. Xu;Brian Demsky
中科院分区：
文献类型：
--
作者：
Hamed Gorjiara;G. Xu;Brian Demsky
持续的内存（PM）技术将接近DRAM的性能与持久性结合在一起，并打开使用数据结构的一个副本作为工作副本和持久存储数据的可能性。确保这些持久数据结构崩溃（即功率故障）是一个主要挑战。持续内存的存储不会立即持续 - 它们最初驻留在处理器缓存中，仅在由于空间限制或明确的冲洗指令而出现冲洗时才写入PM。鉴于PM的字节 - 地理性可导致更多州的状态，测试崩溃一致性比磁盘的崩溃一致性比磁盘更具挑战性。我们提出Jaaru，这是PM程序的完全自动化和超高的模型检查器。 Jaaru效率的关键是一种基于约束细化的新技术，可以减少许多数量级必须探索的执行次数。这种探索技术有效地利用了“提交商店”（一种常见的编码模式），以减少模型检查复杂性，从指数执行长度到二次执行的长度。我们已经用PMDK和食谱评估了Jaaru，并发现了25个持久性错误，其中18个是新的。 Jaaru也比YAT效率更高，YAT是一种模型检查器，该模型检查器急切地探索所有可能的状态。
Persistent memory (PM) technologies combine near DRAM performance with persistency and open the possibility of using one copy of a data structure as both a working copy and a persistent store of the data. Ensuring that these persistent data structures are crash consistent (i.e., power failures) is a major challenge. Stores to persistent memory are not immediately made persistent --- they initially reside in processor cache and are only written to PM when a flush occurs due to space constraints or explicit flush instructions. It is more challenging to test crash consistency for PM than for disks given the PM's byte-addressability that leads to significantly more states. We present Jaaru, a fully-automated and ultra-efficient model checker for PM programs. Key to Jaaru's efficiency is a new technique based on constraint refinement that can reduce the number of executions that must be explored by many orders of magnitude. This exploration technique effectively leverages commit stores, a common coding pattern, to reduce the model checking complexity from exponential in the length of program executions to quadratic. We have evaluated Jaaru with PMDK and RECIPE, and found 25 persistency bugs, 18 of which are new. Jaaru is also orders of magnitude more efficient than Yat, a model checker that eagerly explores all possible states.