LLVM-K Backend

As we mentioned earlier, K transitioned from using a two-level interpretation engine to using a native interpreter generated by LLVM-K.

What is LLVM-K?

LLVM-K is the backend of the K framework. It takes a K language definition and compiles it into highly optimized native code. LLVM-K allows us to:

• Execute K-based languages efficiently without sacrificing correctness.

• Automatically generate fast interpreters from formal language semantics.

• Optimize performance using LLVM IR, ensuring that execution speed matches manual interpreters.

Key components of LLVM-K

LLVM-K is made up of several components that work together to optimize execution:

• KORE AST data structures: Represent KORE syntax in memory.

• Decision tree generator: Converts KORE rules into structured decision trees for efficient pattern matching.

• Code generator: Translates decision trees into compiled code that applies rewrite rules.

• Runtime terms: Data structures that represent the program’s state during execution.

• Runtime library: Provides performance-focused utilities implemented in C/C++ and LLVM IR.

• Memory management and garbage collector: Handles term allocation and deallocation during execution.

How does LLVM-K work?

To be precise, LLVM-K doesn’t operate on raw K definitions, but on an intermediate representation thereof—KORE, which it compiles into native interpreter binaries that execute rewrite rules efficiently.

A rewrite rule consists of a pattern (left-hand side) and a transformation (right-hand side). When a program runs, LLVM-K needs to determine which rule should be applied next. Instead of searching through thousands of possibilities, it builds decision trees to make this process more efficient.

LLVM-K matches the rule’s pattern against the current state of execution and then applies its corresponding transformation to update the program state. This repeats until no more rules apply, meaning execution has reached a final state.

K provides a way to formally define languages, ensuring correctness. But correctness alone isn’t enough—execution must be fast. LLVM-K bridges the gap, making K-based execution not just correct but also performant. This is crucial for our vision of verifiable, efficient computation.