gpuequiv

文档 | Crates.io

线性时态分支时谱中进程等价性的 GPU 加速实现

该项目是我柏林工业大学学士学位论文的一部分。相关的论文文本托管在 Gobbel2000/thesis-gpuequiv。

这是一个 Rust 包，实现了 B. Bisping 的 光谱算法，重点在于性能和可扩展性。为此，算法中最关键的部分通过 GPU 计算着色器加速。使用 wgpu 包与系统的 GPU API 进行接口交互。着色器使用 WebGPU 着色语言 (WGSL) 编写。这些技术基于新兴的 WebGPU API，旨在使 Web 浏览器能够访问高级 GPU。因此，这个包可以在 WebAssembly 中使用，尽管它要求浏览器支持 WebGPU API。

需要 Rust 版本 >= 1.73。

等价性

对于一个标记转换系统的输入，该算法将决定以下谱中的哪些行为等价性成立，哪些不成立

• 使能性
• 迹等价性
• 失败
• 失败迹
• 就绪性
• 就绪迹
• 复活
• 不可能的未来
• 可能的未来
• 模拟
• 就绪模拟
• 嵌套 2 模拟
• 双模拟

示例

examples 目录包含一些文件，展示了如何使用此包的一些方式。此命令运行示例

cargo run --example NAME

其中 NAME 是示例之一的名称，例如 compare_all。可以使用 RUST_LOG 环境变量启用附加日志。例如

RUST_LOG=gpuequiv=debug,info cargo run --example full

WebAssembly

WASM 明确支持。这需要支持 WebGPU API 的浏览器，请参阅当前的 实现状态。

示例 compare_all 配置为在 WASM 上进行测试。只需运行

cargo run-wasm

然后打开 localhost:8000。输出应出现在浏览器控制台。

测试

可以使用以下方式运行单元和集成测试

cargo test

基准测试

使用以下方式执行基准测试

cargo bench

此操作将在VLTS（非常大型转换系统）基准测试套件的一部分上运行算法。基准测试由Criterion-rs控制。