Perennial：验证并发且瓦解安全的体系

Perennial：验证并发且瓦解安全的体系

    perennial Verifying concurrent crash-safe systems  

项目地点: https://gitcode.com/gh_mirrors/pe/perennial   
在当代软件开发中，确保体系的并发性和瓦解安全性是至关重要的。Perennial 是一个开源项目，专门用于验证具有并发和瓦解安全要求的体系，包括规复过程。本文将详细介绍 Perennial 项目，分析其技术特点，并探讨其在实际应用中的场景。
项目介绍

Perennial 是一个用于验证并发和瓦解安全体系的工具，特殊适用于文件体系、并发写前日志（如 Linux 的 jbd2 层）以及长期化键值存储（如 RocksDB）等场景。该项目使用 Goose 来验证用 Go 语言编写的程序（子集）。别的，Perennial 还包罗了对 GoJournal 的正确性证明，GoJournal 是一个颠末验证的日志体系，用于 go-nfsd 项目中。
项目技术分析

技术栈

• Coq：Perennial 使用 Coq 作为其主要开发工具，确保与最新版本的 Coq 兼容。
  
• Goose：Goose 是一个用于验证 Go 程序的工具，Perennial 利用 Goose 来验证 Go 语言的子集。
  
• Git Submodules：项目使用 Git 子模块来管理多个依赖项，确保依赖项的版本稳定性。
  

编译与依赖管理

Perennial 的编译过程相对复杂，必要约莫 120 CPU 分钟。通过并行编译（如 make -j4）可以明显缩短编译时间。项目还支持增量编译，通过 vos 和 vok 文件可以加速编辑-编译-调试循环。
源码组织

• program_logic/：实现 Perennial 中的瓦解安全推理，包括瓦解最弱条件条件、瓦解稳定量、幂等性和瓦解细化推理。
  
• goose_lang/：一个带有内存、并发和外部接口的 lambda 演算，用于模子化 Go 语言并实现 Iris 和 Perennial 的接口。
  
• program_proof/：包罗当前已验证程序的证明。
  
• Helpers/：包罗一些辅助库，如整数包装、转换库等。
  
• algebra/：为 Iris 幽灵变量提供额外的 CMRAs。
  

项目及技术应用场景

Perennial 适用于必要高度并发和瓦解安全性的体系，如：

• 文件体系：确保文件体系在并发操纵和瓦解情况下的数据一致性。
  
• 日志体系：如 Linux 的 jbd2 层，确保日志在体系瓦解后可以或许正确规复。
  
• 长期化键值存储：如 RocksDB，确保在并发写入和体系瓦解情况下的数据完整性。
  

项目特点

• 并发与瓦解安全验证：Perennial 专注于验证体系的并发性和瓦解安全性，确保体系在极端情况下的可靠性。
  
• Goose 集成：通过 Goose 工具，Perennial 可以或许验证 Go 语言的子集，扩展了其应用范围。
  
• 增量编译：支持增量编译和并行编译，明显进步了开发服从。
  
• 丰富的证明库：项目包罗多个已验证的程序和库，如 GoJournal，为开发者提供了可靠的参考。
  

结语

Perennial 是一个强盛的工具，适用于必要高度并发和瓦解安全性的体系开发。通过其丰富的技术栈和高效的编译机制，Perennial 为开发者提供了一个可靠的验证平台。如果你正在开发一个必要高度可靠性的体系，Perennial 绝对值得一试。
    perennial Verifying concurrent crash-safe systems  

项目地点: https://gitcode.com/gh_mirrors/pe/perennial   

免责声明：如果侵犯了您的权益，请联系站长，我们会及时删除侵权内容，谢谢合作！更多信息从访问主页：qidao123.com:ToB企服之家，中国第一个企服评测及商务社交产业平台。