TypeDis：一种用于解耦的类型系统

《Proceedings of the ACM on Programming Languages》：TypeDis: A Type System for Disentanglement

自动验证并行程序解耦性：提出TypeDis类型系统，通过时间戳标注内存分配任务，结合子时类型和递归类型实现自动解耦验证，并基于改进的DisLog2证明系统确保正确性。

　　

摘要AI摘要

要查看此由AI生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

“解耦”是并行程序的一种运行时特性，可确保并行任务彼此之间不会相互影响（即任务之间不会干扰对方的资源分配）。正如MaPLe编译器和运行时系统所展示的那样，解耦特性可以被用于实现快速的自动内存管理，尤其是在并行任务之间无需进行同步的情况下进行任务局部垃圾回收。然而，作为一种低级别的特性，解耦对于程序员来说可能较难理解。迄今为止，唯一能够静态验证解耦特性的方法是DisLog，这是一种基于Iris框架的分离逻辑实现，通过Rocq证明辅助工具进行自动化处理。DisLog是一种功能完备的程序逻辑系统，不仅可以证明程序的功能正确性，还可以验证其是否满足解耦要求。但使用DisLog需要较高的专业技能，并且每个程序的验证工作量都相当大。

本文探讨了通过类型系统实现自动验证的方法，确保所有类型正确的程序都满足解耦条件，从而减轻程序员进行手动验证的负担。本文提出了一种名为TypeDis的类型系统，该系统借鉴了区域类型（region types）的概念，其中每种类型都附带了一个时间戳，用于标识分配该类型的任务。TypeDis支持等递归类型（iso-recursive types），同时也支持类型和时间戳的多态性。关键在于，在类型检查过程中、连接点处以及通过一种称为“子类型化”（subtyping）的机制，时间戳是可以被修改的。本文通过多个示例展示了TypeDis及其特性。TypeDis的正确性及其相关示例已在Rocq证明辅助工具中得到了验证，该工具使用了改进版的DisLog（称为DisLog2）。

AI摘要

AI生成的摘要（实验性)

此摘要是由自动化工具生成的，并非由文章作者编写或审核的。它旨在帮助读者了解研究内容、评估其相关性，并为来自相关研究领域的读者提供辅助。它是对作者提供的摘要的补充，作者提供的摘要仍是文章的正式摘要。完整文章才是最权威的版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。您的反馈将有助于改进未来的摘要版本。

要查看此由AI生成的纯文本摘要，您必须具有高级访问权限。