The OptiTrust framework and the 3 first case studies (TVM's Matmul, OpenCV's blur, and Micro-PIC) are described in the OptiTrust draft paper. The LLM case studies are still work-in-progress.
How to navigate the traces : first click the 'Code' radio button at the bottom of the pages to see transformations applied to code only, then click the '+Annot' to also see contracts and ghost operations. You may also want to click the 'Code after' button to view plain code as opposed to diffs.
TVM's matmul: reproducing a TVM matrix-multiply case study. For details, see the full trace (~100MB), in which substeps can be navigated by clicking on the triangles in the tree view on the left.
OpenCV's blur: reproducing manually written code from a graphics library.
Micro-PIC: a numerical scaling transformation, excerpt from the full Particle-In-Cell (PIC) case study mentioned below.
Llama-3 LLM inference : attention norm: optimization of the first processing applied to the LLM loop that processes the prompt.
Llama-3 LLM inference : several optimizations applied to the prompt-processing in an LLM code : batch-processing of tokens, reordering of loops, recognizing matrix-multiply optimization.
Harris : reproducing an Halide case study of an advanced image processing code. For details, see the Harris full trace (~100MB).
PIC : reproducing manually written code for a state-of-the-art numerical simulation code (Particle-in-Cell plasma physics).
This trace uses our older interface: click on the 3rd 'next' button to view the diff for the main steps.
You can also browse directly the following input and output files: