• Stars
    star
    108
  • Rank 313,790 (Top 7 %)
  • Language
    Rust
  • License
    MIT License
  • Created about 4 years ago
  • Updated almost 3 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Re-implementation of the TASO compiler using equality saturation

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.

development

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 run_docker.sh to the path of your choice to tensat, egg, and taso
  • Run ./run_docker.sh
  • 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 setup.py 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 "http://ftp.gnu.org/gnu/gdb/gdb-9.2.tar.gz" && 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 verify.py. 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 main.rs/main(), 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.

run_exp_main.sh has example commands to run the optimizer. It runs the optimization on TASO's 4 benchmarks and collect various of statistics. analysis/stats.py 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/load_model.py (in our fork of TASO).

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

More Repositories

1

verdi

A framework for formally verifying distributed systems implementations in Coq
Coq
575
star
2

verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Coq
178
star
3

ruler

Rewrite Rule Inference Using Equality Saturation
Rust
105
star
4

Cassius

A CSS specification and reasoning engine
Racket
90
star
5

herbgrind

A Valgrind tool for Herbie
C
90
star
6

crust

A compiler from Rust to C, and a checker for unsafe code
Rust
81
star
7

PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
OCaml
50
star
8

Casper

A compiler for automatically re-targeting sequential Java code to Apache Spark.
Java
49
star
9

pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Coq
49
star
10

szalinski

Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
OpenSCAD
41
star
11

CoqAST

Fun plugin to play with the Gallina AST.
OCaml
37
star
12

oddity

A graphical, time-traveling debugger for distributed systems
Clojure
32
star
13

cheerios

Formally verified Coq serialization library with support for extraction to OCaml
Coq
23
star
14

dexter

a compiler for re-writing image processing functions in C++ to Halide
Java
22
star
15

synapse

Optimizing Synthesis with Metasketches, POPL 2016
Racket
22
star
16

StructTact

Coq utility and tactic library.
Coq
21
star
17

memsynth

An advanced automated reasoning tool for memory consistency model specifications.
Alloy
19
star
18

rake

compiling DSLs to high-level hardware instructions
Racket
19
star
19

stng

compiler for fortran stencils using verified lifting,
C++
17
star
20

oeuf

gallina frontend for CompCert
Coq
17
star
21

ferrite

Ferrite, a toolkit for developing file system crash-consistency models
Racket
16
star
22

potpie

Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct
Coq
13
star
23

reincarnate-aec

Reincarnate Artifact for ICFP 2018
JavaScript
13
star
24

magic

Demystifying the magic of supertactics
OCaml
13
star
25

arvo

A proof assistant.
C
12
star
26

coq-plugin-lib

Library of useful utility functions for Coq plugins
OCaml
11
star
27

SaltShaker

Verifying x86 semantics
Shell
10
star
28

concerto

Combined concrete and abstract interpretation
Java
7
star
29

crimp

Certified Relational to Imperative
Coq
5
star
30

analytics-data

Coq
5
star
31

incarnate-exploration-archive

PL for 3D Printing
OpenSCAD
5
star
32

peek

Peek: a verified peephole optimizer for CompCert
Coq
5
star
33

iag-synthesis

Parallel, incremental evaluation of attribute grammars through synthesis
HTML
4
star
34

bagpipe

Reasoning about BGP configurations. Public development repo.
Coq
4
star
35

theia

Automatically Visualizing Program Execution
OCaml
4
star
36

fix-to-elim

Fixpoint to eliminator translation in Coq
Coq
3
star
37

coq-change-analytics

REPLICA: REPL Instrumentation for Coq Analysis
Python
3
star
38

scout

Using High-Level Design Constraints to Automatically Generate Design Alternatives
Jupyter Notebook
3
star
39

syncro

Synthesis of Incremental Operations
Racket
2
star
40

legato

Legato is a static analysis for finding bugs in dynamic resource usage
Java
2
star
41

univalent-rewrites

POPL 2020 PUMPKIN/DEVOID submission
TeX
2
star
42

staccato

Stale Configuration and Consistency Analysis Tool
Java
2
star
43

pumpkin

Public webpage for Pumpkin Patch
HTML
1
star
44

VeriCQ

Use SpaceSearch to verify Conjunctive Query Rewrite Rules
Perl
1
star
45

epics-tools

Static analysis tools for EPICS
Haskell
1
star
46

PUMPKIN-git

A prototype PUMPKIN PATCH interface with Git integration
OCaml
1
star
47

seguard-resources

SeGuard Public Resources
HTML
1
star
48

nightly-conf

The public nightly server configuration
1
star
49

majortom

An Oddity shim for "arbitrary" x86-64 Linux binaries
Rust
1
star