perennial:验证并发碰撞安全系统 源码

使用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