指定和验证持久化库
摘要：为指定和验证持久化库提出了一个通用框架，即在执行它们的机器发生故障时提供一些持久性保证的数据结构库。我们的框架支持关于各个库的正确性的模块化推理（水平和垂直组合性），而且足够通用，能够包括从硬件体系结构规范到持久线性一致性等所有现有的持久化库规范。作为案例研究，我们指定了FliT和Mirror库，在Px86上验证了它们的实现，并在我们的框架内使用它们构建高级持久化线性一致性库。我们还指定并验证了一个持久性事务库，重点介绍了与弱内存相比持久内存所特有的一些技术挑战以及它们如何被我们的框架处理。
作者：L''eo Stefanesco, Azalea Raad, Viktor Vafeiadis
论文ID：2306.01614
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-05