Towards a Model Checking Framework for a New Collector Framework
Towards a Model Checking Framework for a New Collector Framework
复制标题
面向新收集器框架的模型检查框架
DOI：
10.1145/3546918.3546923
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Blackburn, Stephen M.
中科院分区：
文献类型：
--
作者：
Xu, Bochen;Moss, Eliot;Blackburn, Stephen M.
垃圾收集器提供内存安全，这是实现程序正确性的重要一步。然而，收集器本身的正确性可能是具有挑战性的，考虑到这种系统的编写风格和现代硬件的弱有序内存访问。最大化收益的一种方法是使用一个框架，在该框架中，可以将精力集中在可以组成各种收集器的小型模块化关键组件的正确性上。完整的正确性证明可能是不切实际的，所以我们建议通过在垃圾收集框架内对关键内核应用模型检查来获得一定程度的收集器正确性的信心。我们进一步设想了一个模型框架，与收集器的框架性质平行，希望能够很容易地为新的收集器创建新的模型。我们在这里描述了一个原型模型结构，并提出了模型检查的结果停止世界和快照在开始并发标记。我们发现了有用的模型结构，并且可以在有能力的服务器上在可能的时间和空间预算内检查模型。这表明，以模块化风格构建的收集器可能会进行模型检查，并且还值得开发一个具有特定于域的语言的模型检查框架，以生成这些模型。
Garbage collectors provide memory safety, an important step toward program correctness. However, correctness of the collector itself can be challenging to establish, given both the style in which such systems are written and the weakly-ordered memory accesses of modern hardware. One way to maximize benefits is to use a framework in which effort can be focused on the correctness of small, modular critical components from which various collectors may be composed. Full proof of correctness is likely impractical, so we propose to gain a degree of confidence in collector correctness by applying model checking to critical kernels within a garbage collection framework. We further envisage a model framework, paralleling the framework nature of the collector, in hope that it will be easy to create new models for new collectors. We describe here a prototype model structure, and present results of model checking both stop-the-world and snapshot-at-the-beginning concurrent marking. We found useful regularities of model structure, and that models could be checked within possible time and space budgets on capable servers. This suggests that collectors built in a modular style might be model checked, and further that it may be worthwhile to develop a model checking framework with a domain-specific language from which to generate those models.
“桶”。
影响因子：
2.3
作者：
Nadeem Y. Karimbux
通讯作者：
Nadeem Y. Karimbux
DOI：
10.1145/2737924.2738006
发表时间：
2015-06
期刊：
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Peter Gammie;Antony Hosking;Kai Engelhardt
通讯作者：
Peter Gammie;Antony Hosking;Kai Engelhardt
CakeML 的新的经过验证的编译器后端
DOI：
10.1145/2951913.2951924
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Tan Y
通讯作者：
Tan Y