The ROCetta Project
The ROCetta Project (pron. rosetta) aims to formally specify GPU virtual instruction sets (e.g. PTX) and hardware instruction sets (e.g. SASS). The emphasis is on specifying all the components of these instruction sets in a modular, reusable fashion.
Note: (May 2024) Some of the links below may not work since they point to private repositories. We're working to release them.
Our current focus is to produce for NVIDIA's PTX:
- A complete grammar and parser for PTX
- A test suite
- An interpreter
- Executable semantics (in Python and C)
- Formal semantics (in SMT2)
- A C implementation of the PTX Elementary Math Functionality (due to Benjamin Carleton)
We've also produced semantics for NVIDIA's SASS for the Pascal architecture (plus bits of Maxwell and Volta):
- Interpreter/VM (Includes build scripts to construct C definitions from the semantics database)
- SASS ISA Semantics Database (SMT)
- SASS AST
- SASS math (derived from PTX math tweaked slightly for functions to correspond to SASS instructions)
- CUDA-GDB State Grabber (for obtaining register maps for validation)
Some other code that may be useful outside the ROCetta project and not directly related to semantics.
- Harmonv, a toolkit for interoperating with NVIDIA's binary toolchain.
- GPU API Interposer, including interceptors for libcuda and libcudart.
- xlatir, the translatable intermediate representation used to write the PTX semantics.
- Feature matrix manipulation, tools to help you track feature completeness.
- EBNFtools, a library to manipulate EBNF files that use the W3 EBNF syntax
- NVCCWrapper, intercept and manipulate NVCC command lines
Current Team
- Benjamin Valpey
- Yanji Gao
- Sreepathi Pai
Team Alumni
- Amr S. Elhelw
- Benjamin Carleton
Publications
Amr S. Elhelw and Sreepathi Pai, Horus: A Modular GPU Emulator Framework (Poster), ISPASS 2020, August 2020