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，确保在并发写入和系统崩溃情况下的数据完整性。

项目特点

1. 并发与崩溃安全验证：Perennial 专注于验证系统的并发性和崩溃安全性，确保系统在极端情况下的可靠性。
2. Goose 集成：通过 Goose 工具，Perennial 能够验证 Go 语言的子集，扩展了其应用范围。
3. 增量编译：支持增量编译和并行编译，显著提高了开发效率。
4. 丰富的证明库：项目包含多个已验证的程序和库，如 GoJournal，为开发者提供了可靠的参考。

结语

Perennial 是一个强大的工具，适用于需要高度并发和崩溃安全性的系统开发。通过其丰富的技术栈和高效的编译机制，Perennial 为开发者提供了一个可靠的验证平台。如果你正在开发一个需要高度可靠性的系统，Perennial 绝对值得一试。

perennial Verifying concurrent crash-safe systems 项目地址: https://gitcode.com/gh_mirrors/pe/perennial