并发垃圾收集器的形式化推导
Formal Derivation of Concurrent Garbage Collectors
摘要：
众所周知，并发垃圾收集器很难正确实现。以前的方法产生正确的收集器的问题主要是基于位置和证明验证或应用程序的域特定的模板和转换。我们展示了如何从一个正式的规范，强调域独立的设计理论和转换的应用程序，通过细化派生的并发垃圾收集器的家庭的上游。一个关键的贡献是扩展到经典的格理论的不动点定理，占并发突变和收集的动态。
英文摘要：
Concurrent garbage collectors are notoriously difficult to implement correctly. Previous approaches to the issue of producing correct collectors have mainly been based on posit-and-prove verification or on the application of domain-specific templates and transformations. We show how to derive the upper reaches of a family of concurrent garbage collectors by refinement from a formal specification, emphasizing the application of domain-independent design theories and transformations. A key contribution is an extension to the classical lattice-theoretic fixpoint theorems to account for the dynamics of concurrent mutation and collection.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
