cargo-check-deadlock

在编译时检测 Rust 源代码中的死锁

该工具支持检测由不正确使用 互斥锁 (std::sync::Mutex) 和 条件变量 (std::sync::Condvar) 引起的死锁。它还支持检测在永远不会返回的线程上调用 join 所引起的死锁。

它通过将 Rust 源代码的 中级中间表示 (MIR) 表示 转换为 Petri 网络模型（一种数学和图形模型）来实现。然后，Petri 网由模型检查器 LoLA 分析，以确定网络是否可以到达死锁状态。这种方法是对所有可能的程序状态进行彻底检查。它不仅仅是测试几个可能的执行情况，也不仅仅是 模糊测试。

有关哪些功能有效以及哪些无效的更多详细信息，请参阅 限制。有关此项目的更多背景信息，请参阅 上下文。

支持的导出格式

• Petri 网标记语言 (PNML) https://www.pnml.org/：许多其他与 Petri 网合作的工具使用的基于 XML 的标准格式。
• LoLA - 低级 Petri 网分析器 https://theo.informatik.uni-rostock.de/theo-forschung/tools/lola/：此格式是项目中使用的模型检查器所需的。
• DOT（图描述语言）https://en.wikipedia.org/wiki/DOT_(graph_description_language)：对结果Petri网的一种简单可视化。请参阅相应的章节。

从crates.io安装

假设您已经在系统上安装了Rust，只需运行

cargo install cargo-check-deadlock

然后您必须按照模型检查器章节中的说明安装模型检查器。

设置开发环境

要为开发获取本地副本并运行，请按照以下简单的示例步骤操作。

先决条件

• 使用Rust网站上所述的rustup安装Rust

• 使用具有rustc-dev组件的最新夜间版本进行安装

  rustup toolchain install nightly
  

• 激活夜间工具链

  rustup default nightly
  

• 安装用于与编译器内部结构一起工作的组件

  rustup component add rust-src rustc-dev llvm-tools-preview
  

编译器版本

必须使用夜间工具链编译项目，以访问编译器的私有crates。根目录中的工具链文件rust-toolchain覆盖了此项目的当前活动工具链。有关更多信息，请参阅rustup文档：https://rust-lang.github.io/rustup/overrides.html#the-toolchain-file

settings.json配置VS Code，以指导rust-analyzer扩展自动发现正确的工具链。这对于在处理rustc的私有crates时获得有关类型、编译器错误等的反馈非常有用。

随着时间的推移，编译器内部结构发生变化，代码不可避免地需要更改才能再次工作。

当前仓库的状态使用以下版本编译无警告，并且所有测试通过 rustc 1.72.0-nightly (065a1f5df 2023-06-21)

安装

1. 克隆仓库

   git clone https://github.com/hlisdero/cargo-check-deadlock.git
   

2. 确保在项目目录中运行时sysroot指向夜间工具链输出应类似于 $HOME/.rustup/toolchains/nightly-<platform>

   rustc --print=sysroot
   

3. 使用cargo构建项目

   cargo build
   

4. 运行测试以检查一切是否正常工作cargo

   cargo test
   

用法

编写一个编译正确的有效Rust程序，例如rust_program.rs，然后运行

cargo check-deadlock <path_to_program>/rust_program.rs

结果将打印到stdout。在当前工作目录（CWD）中应出现一个名为net.lola的文件。

如果您想导出到其他格式或使用自定义文件名或输出文件夹，请使用

cargo check-deadlock <path_to_program>/rust_program.rs --dot --pnml --filename=example --output-folder=output/

在这种情况下，应出现在output/文件夹中的文件名为example.pnml和example.dot。

要获取完整的CLI选项列表，请使用--help标志。

注意：有关更多示例，请参阅集成测试。

调试

程序支持在 crate clap_verbosity_flag 中定义的详细程度标志。例如，使用标志 -vvv 运行程序将打印调试信息，这些信息对于确定 MIR 表示中哪一行没有被正确翻译非常有用。

cargo check-deadlock <path_to_program>/rust_program.rs -vvv

LoLA 模型检查器支持打印“见证路径”，显示导致死锁的一系列转换触发。当扩展翻译器且 Petri 网不匹配给定程序的预期结果时，这非常有用。可以找到一个方便的 脚本 来打印 .lola 文件的见证路径。

可视化结果

本地

要查看源代码的 MIR 表示，可以使用相应的标志编译代码： rustc --emit=mir <source_code_path>

要使用 dot 工具将网图转换为 .dot 格式，请按照 GraphViz 网站 上的说明进行安装。

运行 dot -Tpng net.dot -o outfile.png 从生成的 .dot 文件生成 PNG 图片。

运行 dot -Tsvg net.dot -o outfile.svg 从生成的 .dot 文件生成 SVG 图片。

更多信息和其它格式可以在 文档 中找到。

在线

要查看源代码的 MIR 表示，可以使用 Rust Playground。只需在下拉菜单中选择“MIR”而不是“运行”。请记住也要选择夜间版本。

要绘制给定的 DOT 结果，可以使用 Graphviz Online 工具，由 dreampuf 提供。

或者，您可以使用 Edotor 或 Sketchviz。

模型检查器

LoLA 模型检查器可以从 这里 下载。它必须从源代码编译。

GitHub 上有一个带有详细说明的替代镜像：https://github.com/hlisdero/lola

最后一个选项是将预编译的 64 位可执行文件 ./assets/lola 复制到 $PATH。在 repo 中可以找到一个用于此目的的 脚本。

将来可能会添加对其他模型检查器和导出格式的支持。添加其他后端可以是一个比较它们的性能和准确性的好方法。导出格式是在此项目中使用的自定义 Petri 网库中实现的：https://github.com/hlisdero/netcrab

局限性

由于Rust语言非常复杂，在实践上支持所有可能导致死锁的情况是不可能的。本项目旨在证明使用Petri网的方法是可行的，并且能够在编译时检测到错误，从而增强Rust代码的安全性和可靠性。目前最难检测的情况是丢失的信号。这种特定的死锁情况发生在某个线程在另一个线程调用 wait 之前，调用 notify_one 通知条件变量时。

建议查看示例程序，以了解哪些类型的程序可以成功翻译和分析。特别有趣的例子包括哲学家就餐问题和生产者-消费者问题。

目前，该翻译器可以处理的程序相当有限。

• 不支持任何结构体（struct）、枚举（enum）或实现（impl）块。
• 线程之间传递同步变量是可以的，但缺少在用户定义函数之间传递它们的支持。
• 数组、向量和其他数据结构可能导致翻译失败。
• 不支持通道。
• 不支持RwLock。
• 不支持Barrier。
• 不支持异步（Async）。
• 不支持来自外部库的同步机制，如tokio或semaphore。

贡献

贡献使开源社区成为一个如此美妙的学习、灵感和创造的地方。您所做的任何贡献都备受赞赏。

如果您有改进此项目的建议，请fork仓库并创建一个pull请求。您也可以简单地创建一个带有“enhancement”标签的问题。别忘了给项目加星！再次感谢！

1. fork项目
2. 创建您的功能分支（git checkout -b feature/AmazingFeature）
3. 提交您的更改（git commit -m 'Add some AmazingFeature'）
4. 推送到分支（git push origin feature/AmazingFeature）
5. 打开pull请求

许可证

在MIT许可证和Apache许可证（版本2.0）的条款下分发。有关更多信息，请参阅LICENSE-MIT，LICENSE-APACHE。

致谢

本项目扩展并重新实现了在https://github.com/Skasselbard/Granite中找到的Tom Meyer的原始作品中的想法，作为名为"A Petri-Net Semantics for Rust"的硕士论文的一部分。

《rustc 开发指南》（rustc 开发指南）是理解编译器的可靠指南。对于每个感兴趣的贡献者来说，这是一本必读的书籍！

《nightly 文档》（nightly 文档）也是了解 MIR 的细节以及如何翻译每个函数的有价值资源。

上下文

本项目是胡安·霍拉西奥·利斯德罗·斯卡菲诺的本科论文“使用 Petri 网在 Rust 中进行编译时死锁检测”的一部分，该论文在布宜诺斯艾利斯大学工程学院完成。

该论文在 GitHub 上公开：https://github.com/hlisdero/thesis

它提供了本项目的重要背景主题和实现细节。