Relaxing safely: verified on-the-fly garbage collection for x86-TSO
Relaxing safely: verified on-the-fly garbage collection for x86-TSO
复制标题
DOI：
10.1145/2737924.2738006
复制
发表时间：
2015-06
期刊：
影响因子：
--
通讯作者：
Peter Gammie;Antony Hosking;Kai Engelhardt
中科院分区：
文献类型：
--
作者：
Peter Gammie;Antony Hosking;Kai Engelhardt
我们报告了一项机器检查的安全性验证，用于最先进的，即时，同时，刻有痕迹的垃圾收集器，该垃圾收集器专为具有较弱的内存一致性的多核体系结构而设计。该证明明确结合了X86多处理器的轻松记忆语义。据我们所知，这是此类垃圾收集器的首次完全机器检查的安全证明。我们在系统实施者会发现有吸引力的框架中的证据，其中系统的基本组件以简单而直观的编程语言指定。抽象模型足够详细，以使其与汇编语言实现的通信变得直接。
We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward.