首页> 外文期刊>Science of Computer Programming >Lock-free parallel and concurrent garbage collection by mark&sweep
【24h】

Lock-free parallel and concurrent garbage collection by mark&sweep

机译:mark&sweep的无锁并行和并发垃圾收集

获取原文
获取原文并翻译 | 示例

摘要

This paper presents a lock-free algorithm for mark&sweep garbage collection (GC) in a realistic model using synchronization primitives load-linked/store-conditional (LL/SC) or compare-and-swap (CAS) offered by machine architectures. The algorithm is concurrent in the sense that garbage collection can run concurrently with the application (the mutator threads). It is parallel in that garbage collection itself may employ several concurrent collector threads. We first design and prove an algorithm with a coarse grain of atomicity and subsequently apply the reduction method developed and verified in [H. Gao, W.H. Hesselink, A formal reduction for lock-free parallel algorithms, in: Proceedings of the 16th Conference on Computer Aided Verification, CAV, July 2004] to implement the high-level atomic steps by means of the low-level primitives. Even the correctness of the coarse grain algorithm is very delicate due to the presence of concurrent mutator and collector threads. We have verified it therefore by means of the interactive theorem prover PVS.
机译:本文提出了一种使用机器架构提供的同步原语加载链接/存储条件(LL / SC)或比较交换(CAS)的现实模型中的标记清除垃圾收集(GC)的无锁算法。从垃圾回收可以与应用程序(mutator线程)并行运行的意义上说,该算法是并发的。这是并行的,因为垃圾收集本身可能会使用多个并发的收集器线程。我们首先设计并证明了一种具有原子粗粒度的算法,然后应用了在[H.N.H.M.H.M.H.O.S.,H.S.,2004,44(2)]中开发和验证的归约方法。高卫华Hesselink,无锁并行算法的正式简化,在:第16届计算机辅助验证会议论文集,CAV,2004年7月]中介绍了通过低级原语实现高级原子步骤的过程。由于存在并发的mutator和collector线程,即使是粗粒度算法的正确性也非常微妙。因此,我们已经通过交互式定理证明者PVS对其进行了验证。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号