gpuequiv

Documentation | Crates.io

A GPU-accelerated implementation of an algorithm to find all equivalences of processes in the Linear-time Branching-time Spectrum.

This project is part of my bachelor's thesis at Technische Universität Berlin. The accompanying thesis text is hosted at Gobbel2000/thesis-gpuequiv.

This is a Rust crate implementing the Spectroscopy algorithm by B. Bisping with a focus on performance and scalability. To this end, the most critical parts of the algorithm are accelerated by GPU compute shaders. The wgpu crate is used for interfacing with the system's GPU API. Shaders are written in the WebGPU Shading Language (WGSL). These technologies are based on the up-and-coming WebGPU API, aiming to enable advanced access to GPUs in web browsers. Therefore, this crate can be used in WebAssembly, although it requires the browser to support the WebGPU API.

Requires Rust version >= 1.73.

Equivalences

For an input Labeled Transition System, the algorithm will decide for any process pair which of the behavioral equivalences in the following spectrum hold and which don't:

• Enabledness
• Trace Equivalence
• Failures
• Failure Traces
• Readiness
• Readiness Traces
• Revivals
• Impossible Futures
• Possible Futures
• Simulation
• Ready Simulation
• Nested 2-Simulation
• Bisimulation

Examples

The examples directory contains a few files showcasing some of the ways this crate can be used. This command runs the examples:

cargo run --example NAME

where NAME is the name of one of the examples, for example compare_all. Additional logging can be enabled using the RUST_LOG environment variable. For example:

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

WebAssembly

WASM is explicitly supported. This requires a browser that supports the WebGPU API, see the current implementation status.

The example compare_all is configured to be tested on WASM. Simply run:

cargo run-wasm

and then open localhost:8000. The output should appear in the browser console.

Tests

Unit and integration tests can be run with:

cargo test

Benchmarks

Execute benchmarks with:

cargo bench

This runs the algorithm on part of the VLTS (Very Large Transition System) benchmark suite. Benchmarks are controlled by Criterion-rs.