Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?


Failed to load latest commit information.
Latest commit message
Commit time
March 10, 2021 02:50
February 27, 2021 18:01
August 24, 2020 04:09
October 2, 2020 19:20
April 8, 2021 12:39
February 27, 2021 18:01
February 27, 2021 18:01
June 17, 2020 15:20
March 1, 2021 22:11
June 16, 2020 00:39
October 6, 2020 21:12
October 6, 2020 21:12
November 30, 2020 16:24
September 26, 2020 01:00
October 6, 2020 21:12
October 11, 2020 20:45
October 1, 2020 17:05
June 15, 2020 17:14

Re-implementation of the TASO compiler using equality saturation. Tensat implements both the graph transformation verifier and the optimizer; the former is complete while the latter is in progress.


Tensat builds on TASO, so it has the same hardware requirement as TASO. This essentially means you need GPUs and drivers for nvidia-docker (if you just want to run the verifier, you don't need GPUs and the regular docker works). You need the TASO runtime (with its dependencies), rust and rust-bindgen to build tensat.

The Dockerfile sets this all up for you. Here's the recommended way of setting up the environment using docker:

  • cd to /docker and execute docker build --tag tensat:1.0 . to build the image
  • Get the dependent repositories. We need a forked version of egg, and a forked version of TASO. Clone these two repositories to a path of your choice
  • Change the source parameter of bind mount in to the path of your choice to tensat, egg, and taso
  • Run ./
  • Now you are inside the docker container, we need to build TASO:
    • Run the following to install:
    cd /usr/TASO
    mkdir -p build
    cd build
    cmake ..
    sudo make install -j10
    cd /usr/TASO/python
    python install
  • Then it is good to go

We recommend perusing the rust-bindgen guide and related docs, and note that its c++ support is primitive.

To help debugging, you can install gdb:

apt-get update
apt-get install -y texinfo
cd /usr && wget "" && tar -xvzf gdb-9.2.tar.gz && cd gdb-9.2 && mkdir build && cd build && ../configure && make
make install

the verifier

The verifier re-implements TASO's It takes a list of transformation rules to be checked and populates an EGraph with the expressions in these rules. Then it iteratively applies the axioms, checking if all rules are verified after each round. If so it stops, indicating success; otherwise it continues until the EGraph saturates. If there are still un-verified rules after saturation, we can conclude those rules are unsound w.r.t. the axioms. This strategy is faster (~30x in our simple experiments) than naively verifying rule-by-rule, because the equality proofs of many rules may overlap, and each EClass may contain expressions from many different rules.

To run the verifier, uncomment prove_taso_rules() in, comment out optimize(), cd to project root and execute cargo run --release taso_rules.txt. The --release flag turns on rust optimizations.

the optimizer

The optimizer replaces TASO's backtracking search with equality saturation. It uses TASO's synthesized rewrite rules. It leverages TASO's infrastructure for maintaining metadata of the tensor information (like shape), as well as TASO's cost function that directly executes DL operators. has example commands to run the optimizer. It runs the optimization on TASO's 4 benchmarks and collect various of statistics. analysis/ can be used to analyze the statistics and plot results. Uncomment the -x flag and argument to save the optimized model into a file. This file can be converted to ONNX format by TASO/example/ (in our fork of TASO).

We support both greedy extraction and ILP extraction. User can control many options through command line flags (see src/ for the flags).


Re-implementation of the TASO compiler using equality saturation







No releases published


No packages published