文件名称：perennial:验证并发碰撞安全系统
文件大小：1.14MB
文件格式：ZIP
更新时间：2024-04-16 02:31:17
coq concurrency verification Coq
使用Perennial验证并发，碰撞安全系统 Perennial是用于验证具有并发性和崩溃安全性要求的系统（包括恢复过程）的正确性的系统。 例如，考虑一下文件系统，并发预写日志记录（例如Linux的jbd2层）和持久键值存储（例如RocksDB）。 Perennial使用启用对用Go（子集）编写的程序的验证。 该存储库还包括交易系统的证明，包括建立在顶部的简单NFS服务器。 编译中 我们使用Coq master开发Perennial，并保持与Coq 8.13的兼容性。 如果CI（更新的依赖项）被破坏，Perennial仍应编译，但当前与对我们的一个依赖项的上游更改不兼容。 我们试图避免这种情况。 该项目使用git子模块来包含多个依赖项。 您应该运行git submodule update --init --recursive进行设置。 要编译，只需在$PATH上使用Coq运行ma