Soufflé synthesizes a native parallel C++ program from a logic specification. The synthesis is performed by several applications of the Futamura Projection, a technique rooted in partial evaluation that transforms an interpreter into a compiler through staged specialization.
How Synthesis Works
The process begins with a semi-naïve evaluation strategy serving as the interpreter for Datalog rules. Through successive Futamura projections, this interpreter is specialized against the user's logic specification, yielding a relational-algebra representation. That representation is then lowered into templatized C++ code, which is compiled into a standalone parallel executable.
Staged Compilation
Soufflé employs an optimized staged compilation pipeline. Each stage progressively refines the intermediate representation, applying transformations that exploit the structure of the input Datalog program. The result is a C++ program that evaluates the fixed-point semantics of the original specification with minimal runtime overhead, leveraging multi-core parallelism for large-scale workloads.
Key Insight
The synthesis approach means Soufflé does not interpret Datalog at runtime. Instead, it produces a dedicated, compiled artifact tailored to the specific analysis problem — enabling performance that scales to real-world static analysis tasks such as points-to analysis and taint tracking.
From Logic to Parallel Code
The translation path follows three broad phases:
- Interpreter Specialization — The semi-naïve evaluation engine is partially evaluated against the Datalog rules, producing a specialized relational-algebra plan.
- Code Generation — The relational-algebra plan is emitted as templatized C++, with each relation and operation mapped to efficient data structures and loops.
- Native Compilation — The generated C++ is compiled by a standard C++ compiler, producing a parallel binary that executes the analysis.
This staged approach allows Soufflé to apply domain-specific optimizations at each level, from join ordering and index selection in the relational layer down to loop fusion and vectorization hints in the generated C++.
→ Return to Documentation