PaperlayerView exact revision on arXiv

Source-linked AI summary

Let it Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow

Zhengyao Lin, Yi Cai, Milijana Surbatovich

arXiv:2608.05451v1cs.PLcs.LO

TL;DR

Compiling asynchronous dataflow requires preserving deterministic behavior while exposing pipelined parallelism. Wavelet combines capability types with fences and Lean-verified compilation passes to address this challenge. The resulting framework proves simulation and determinacy properties, while its later graph optimizations remain partly unverified.

  • Problem

    Compiling sequential programs into asynchronous dataflow graphs must preserve determinacy while enabling pipelining without unnecessary synchronization.

    Source: §1 · pp. 1–2

  • Method

    Wavelet uses a capability type system with fences and Lean-verified passes that translate elaborated programs into dataflow graphs while propagating typing guarantees into simulation and determinacy proofs.

    Source: §1 · pp. 2–3, §3 · p. 6, §4 · p. 8

  • Results

    Wavelet’s verified passes establish forward simulation and determinacy, and its compiled dataflow graphs have comparable quality to existing unverified RipTide and LLVM CIRCT compilers.

    Source: §3 · p. 6

  • Takeaways & Limitations

    Formal verification can connect frontend memory-safety guarantees to compiler-level simulation and determinacy reasoning for asynchronous dataflow.

    Source: §1 · pp. 2–3, §3 · p. 6

    Wavelet’s 54 final rewrite rules and optimizations are currently unverified, with some correctness relying on termination and liveness assumptions.

    Source: §3 · p. 6, §5.5 · p. 19

Abstract

from arXiv · show

Dataflow architectures have gained renewed interest due to their balance between power efficiency and performance. In (spatial) dataflow architectures, a program is represented as a set of entirely distributed and dynamically scheduled dataflow operators that communicate through asynchronous channels, which greatly improves data locality and parallelism. However, compiling to dataflow architectures remains an error-prone process, in order to maintain determinacy while enabling pipelining. Determinacy means that the result of a dataflow program is deterministic and independent of the schedule of operator execution, and pipelining is an important optimization in spatial dataflow that enables parallelism across loop iterations. In this work, we present Wavelet, the first effort to formally verify a compiler for asynchronous dataflow. We use a mix of techniques to achieve this goal. Our frontend uses a novel capability type system with fences to synchronize conflicting memory accesses and enable pipelining. We then verify a Lean formalization of two core passes of our compiler that translates elaborated programs from the type checker to dataflow graphs, proving important properties of forward simulation and determinacy. Notably, our formalization semantically propagates the soundness guarantees of the frontend type system, ensuring modularity between simulation and determinacy proofs. In evaluation, we show that dataflow graphs compiled by Wavelet have comparable sizes to those produced by an unverified optimizing compiler for the RipTide spatial dataflow architecture.

1 Introduction

Wavelet addresses the challenge of compiling sequential programs into asynchronous dataflow graphs that preserve determinacy while enabling pipelining. It combines capability typing with fences and formally verified Lean compiler passes to establish simulation and determinacy guarantees.

1 Introduction

  • Dataflow compilers must avoid races and deadlocks while translating imperative programs into distributed graphs whose execution remains equivalent to the source.The distributed execution model makes memory consistency, equivalence, and scheduling correctness central compiler responsibilities.Source: §1 · p. 2
  • Pipelining removes unnecessary dependencies to overlap loop iterations, but those removals can introduce races and violate schedule-independent determinacy.The compiler therefore must balance parallelism against preservation of memory dependencies.Source: §1 · p. 2
  • Wavelet presents a formally verified compiler for asynchronous dataflow, targeting correct and efficient compilation without unnecessarily restricting parallelism.Its motivation is to preserve sequential behavior while enabling desired dataflow parallelism.Source: §1 · p. 2
  • Its Lean-verified core passes provide forward simulation and deadlock-freedom, while semantic affine permissions carry frontend typing guarantees into determinacy proofs.This separation supports modular reasoning across simulation and determinacy.Source: §1 · pp. 2–3
  • Wavelet’s compiler proofs interpret sequential and dataflow programs in a common semantic framework, enabling modular verification from single functions to linked whole programs.The approach uses separate linking proofs for whole-program composition.Source: §1 · p. 2
  • Wavelet uses a capability-based type system with fences to ensure race-freedom and facilitate pipelining.The frontend synchronizes conflicting memory accesses while avoiding unnecessary synchronization.Source: §1 · pp. 2–3

2 Background & Motivation

Dataflow programs use asynchronously communicating operators to expose parallelism, but compilation must preserve memory ordering and determinacy. Wavelet addresses this tension by using explicit data dependencies, capability-guided synchronization, and verified control-flow conversion.

2 Background & Motivation

  • Dataflow graphs represent operators as nodes and asynchronous communication channels as edges, with memory and control operators exposing computation and sequencing explicitly.Store Done signals can enforce ordering by becoming dependencies for later loads or stores.Source: §2 · p. 3
  • In the array example, a carry operator streams loop indices while the body loads A[i], increments the value, and stores the result to B[i].The loop header forms a cycle through the carry operator, while the body processes streamed indices.Source: §2 · pp. 3–4
  • When arrays are disjoint, loop-body iterations may be parallelized because they need not carry the same memory dependencies.The presence or absence of dependencies determines whether iterations can overlap.Source: §2 · p. 4
  • Removing a store-to-load back-edge allows iteration i+1 to load in parallel with iteration i’s computation, but aliasing between A and B can cause races and nondeterministic results.The back-edge is necessary when it preserves a source-level memory dependency.Source: §2 · p. 4

3 System Overview

Wavelet combines a capability-and-fence frontend with formally verified control-flow conversion and linking to compile sequential programs into determinate, deadlock-free dataflow graphs while preserving pipelining.

3 System Overview

  • Wavelet’s pipeline type-checks capabilities and fences, elaborates explicit permissions, converts control flow, links functions, and finally selects operators and optimizes graphs.Frontend soundness is translation-validated; control-flow conversion and linking are formally verified, while final operator selection and optimization remain unverified.Source: §3 · pp. 4–6
  • Capability types and fences identify conflicting memory accesses and synchronize them without unnecessarily preventing parallel execution.The frontend is designed to preserve safe pipelining by distinguishing accesses that can proceed in parallel from those requiring ordering.Source: §3 · p. 5
  • Control-flow conversion compiles each elaborated Llet function into an Lflow process, tracking unused variables and path conditions to relate sequential variables to dataflow channels.Wavelet also consumes unused values at termination so compiled graphs can be invoked repeatedly without deadlocks.Source: §3 · pp. 5–6
  • Linking connects individually compiled graphs using static restrictions and modular linking semantics to address distributed local state, FIFO buffers, and concurrent function invocations.The proof structure separates semantic and syntactic linking, supporting modular compilation of functions into whole programs.Source: §3 · p. 6
  • Lean proofs establish forward simulation with a deadlock-free schedule and determinacy for terminating, type-system-sound programs, whose output is schedule-independent.Determinacy is proved independently from core simulation proofs by propagating permission soundness as label restrictions across the two semantics.Source: §3 · p. 6
  • Wavelet’s final graphs have comparable quality to existing unverified dataflow compilers after architecture-specific operator lowering and unverified optimizations.The comparison includes RipTide and LLVM CIRCT, while the final rewrite-based optimization pass is outside the verified core.Source: §3 · p. 6

4 Frontend: Capability Types and Fences

Wavelet’s frontend uses capability types and fences to expose memory dependencies, lowers them into ghost permissions, and supplies soundness assumptions for the verified backend.

4 Frontend: Capability Types and Fences

  • Capability types assign shared or unique permissions to precise array regions, distinguishing parallel reads from exclusive writes and avoiding unnecessary synchronization.The type judgment tracks capability and propositional contexts, allowing dependent index reasoning through SMT checks.Source: §4 · pp. 7–8
  • Typing rules require suitable permissions for indexed loads and stores, consume those permissions, and use fences to reset the capability context at explicit memory dependencies.Shared permissions can support parallel loads, while stores require unique access to the written index.Source: §4 · pp. 7–9

4.2 Ghost Permissions Inference and Fence-Removal

  • The frontend lowers fences and capabilities into Llet ghost permissions and jnsplt operations that make synchronization explicit for later dataflow compilation.Translation validation checks that synthesized permission tokens reflect the source typing constraints and satisfy the backend’s assumed soundness property.Source: §4.2 · p. 9
  • Permission contexts track synchronized, pending, and garbage-collectable permissions, materializing dependencies while avoiding unnecessary memory ordering for safe pipelining.Disjoint permissions allow a load and store to run in parallel, whereas a later store waits for the permission produced by an earlier load.Source: §4.2 · p. 9

4.3 Backend Assumptions

  • The backend models permissions with fractional partial commutative monoids and guarded semantics that checks operator specifications and blocks progress when they are violated.The jnsplt specification preserves the PCM sum of input and output permissions rather than creating or destroying resources.Source: §4.3 · p. 10
  • Static FIFO topologies complicate parallel function calls because argument merging and return routing must be fixed despite concurrent buffered invocations.The frontend’s permission soundness is translation-validated rather than formally verified in Lean, and the backend relies on that validated property.Source: §4.3 · p. 10
  • Verified backend correctness assumes static restrictions: functions have at most one external call site, mutual recursion is forbidden, and FIFO channels have bounded buffers.These restrictions preserve expressiveness through branching and tail recursion but make direct Llet programming less ergonomic because control flow must be normalized.Source: §4.3 · p. 10

5 Compiler Design and Verification

This section presents Wavelet’s verified compiler design, covering its translation from Llet to asynchronous Lflow processes, function linking, and graph-reducing rewrites. It summarizes the formal guarantees established for simulation and determinacy, along with the scope and assumptions of the verification.

5.1 Dataflow Calculus Lflow and the Semantics of Llet

  • Wavelet defines Lflow as parallel compositions of recursive atomic processes, with built-in asynchronous operators and customizable synchronous operators for retargetable dataflow compilation.Llet calls remain uninterpreted yield events, enabling separate proofs for function compilation and linking.Source: §5.1 · p. 12

5.2 Control Flow Conversion

  • CFC eliminates Llet control flow by gating branch inputs with steers, merging branch outputs, and routing returns or tail calls through explicit channels.Affine SSA restrictions and provenance-tracking channel names make the forward-simulation relation tractable despite variable-use duplication.Source: §5.2 · pp. 14–15
  • For every well-formed Llet definition D, Wavelet proves ⟦D⟧ ≲ ⟦cfc(D)⟧, and the compiled process returns to its initial state after termination.The initial-state property supports deadlock-freedom when the function is called multiple times.Source: §5.2 · p. 15

5.3 Linking

  • Wavelet separates semantic linking, which internalizes function calls in linked Llet semantics, from syntactic linking, which stitches compiled Lflow processes into one graph.Semantic linking uses an acyclic call graph and preserves modularity by avoiding assumptions that linked Lflow components reset to their initial states.Source: §5.3 · pp. 16–17
  • Theorem 5.5 establishes forward simulation: for every well-formed program P, the semantics of P is included in the semantics of comp(P).Linking simulation connects syntactic linking with semantic linking, allowing the CFC and linking passes to produce a graph that includes the source behavior.Source: §5.3 · p. 17

5.4 Guarded Semantics and Determinacy

  • Permission-guarded semantics checks operator calls, and a terminating guarded trace implies that all unguarded schedules reach the same final state within a bounded number of steps.The guard threads ghost permission tokens through operators, checks pre/post specifications, and uses jnsplt to split and join permissions.Source: §5.4 · pp. 17–18
  • Theorem 5.9 proves compiler determinacy: given a terminating guarded Llet trace, comp(P) is strongly normalizing and produces the same output values as P.The proof carries the guarded trace through forward simulation and applies Theorem 5.7; the result applies to well-formed Llet programs.Source: §5.4 · p. 19

5.5 Operator Selection and Optimization

  • Wavelet’s final term rewriter lowers pseudo-operators to hardware operators, converts permission tokens into control signals, and applies 54 rewrite rules to shrink graphs.The rewrites are currently unverified; one merge-steer rule depends on liveness implied by termination and the simulation relation’s empty-final-channel condition.Source: §5.5 · p. 19

6 Evaluation

Wavelet’s evaluation compares compilation quality, type-system overhead, and verification effort across dataflow and HLS settings. It reports competitive HLS results, explicit usability and compiler costs, and a substantial Lean proof development.

6.1 Compilation Quality

  • Wavelet graphs are 2.62× slower and 3.04× larger than RipTide in geometric mean, partly because permission-token synchronization adds control-flow operators.Wavelet averages 78% control-flow operators versus RipTide’s 51%; disabling streamification narrows the gaps to 1.69× slower and 2.26× larger.Source: §6.1 · p. 20
  • RipTide’s missing memory ordering in the sort benchmark causes a data race and incorrect simulation results, highlighting a correctness trade-off in its synchronization optimization.RipTide mixes synchronization signals with values and removes ordering when data dependencies appear sufficient.Source: §6.1 · p. 20
  • Pipelining keeps Wavelet performance similar to RipTide in vadd, norm, and fc despite graphs with twice as many operators.The comparison disables RipTide streamification for this example.Source: §6.1 · p. 20
  • 1.2× slower execution, 0.69× LUTs, and 0.67× FFs than CIRCT on average show comparable Wavelet HLS performance and area.Some benchmarks outperform CIRCT; unoptimized Wavelet is 2.04× slower with 1.22× LUTs and 1.27× FFs.Source: §6.1 · pp. 20–21, Figure 11 · p. 20

6.2 L∗let Type System Overhead

  • 4.86× more lines of code than C reflect missing desugaring and manually enforced operation splitting and control-flow restrictions.Capability annotations add only a few lines, although precise capabilities and fences require careful memory reasoning.Source: §6.2 · p. 21, Figure 12 · p. 21
  • Translation validation and dataflow optimization dominate compilation time, with complex array indices stressing SMT arithmetic and graph representations remaining inefficient.These are reported compiler-performance limitations rather than failures of the verified compilation guarantees.Source: §6.2 · p. 21

6.3 Verification Effort

  • The Lean formalization contains 797 lines of verified executable code, 1,534 specification lines, and 14,819 proof lines, a proof-to-code/spec ratio of about 6.4:1.Control-flow conversion and determinacy each required approximately two person-months of work.Source: §6.3 · p. 21

7 Related and Future Work

Wavelet connects formally verified asynchronous-dataflow compilation with prior work on CGRAs, HLS, synchronous dataflow, stream processing, affine permissions, and compiler verification. The authors identify richer control flow and capability systems as future directions.

Dataflow and HLS

  • Wavelet differs from FlowCert by providing stronger formal guarantees, while its fine-grained capabilities enable more pipelining than FlowCert’s simple permission tokens.FlowCert targets CGRA compiler correctness through translation validation.Source: §7 · p. 22
  • Unlike prior Dynamatic-inspired calculi, Wavelet verifies compilation from sequential programs and supports shared memory, while remaining complementary to graph-rewrite verification.Connecting Wavelet with Graphiti is identified as a future direction.Source: §7 · p. 22

Synchronous Data Flow

  • Wavelet addresses asynchronous-dataflow challenges such as determinacy and shared memory that do not arise in the same form in more restricted synchronous dataflow.The comparison includes Kind 2, Lustre model checking, and Vélus.Source: §7 · p. 22

Stream Processing

  • Stream-processing and functional-reactive approaches target higher-order streams and abstract determinism or liveness, rather than Wavelet’s low-level shared-memory concerns.The cited approaches are therefore not directly applicable to Wavelet’s compilation challenges.Source: §7 · p. 22

Affine Types and Ghost Permissions

  • Wavelet’s capability system adapts affine types and permissions specifically to memory-access ordering and pipelining in dataflow architectures.The authors propose richer capability types and stronger program logics as future work.Source: §7 · p. 22

Compiler Verification

  • Wavelet builds on compositional compiler-verification work, including semantic linking ideas inspired by CompCert and interaction trees.These foundations support the paper’s modular verification framing.Source: §7 · p. 22

Handling Complex Control Flow

  • The formalized ordered-dataflow model leaves tagged dataflow unverified, limiting support for more expressive control flow such as higher-order functions in Id.Prior unverified work in this model handles only single-function compilation.Source: §7 · pp. 22–23

Data Availability Statement

Wavelet’s source code, proofs, and artifact-evaluation materials are publicly available for reproducing the evaluation.

Data Availability Statement

  • The GitHub repository contains Wavelet’s source code and proofs, while the Docker artifact includes scripts and instructions for reproducing Section 6 results.The statement identifies both implementation and evaluation-reproduction resources.Source: Data Availability Statement · p. 23

Related papers

Loading 2608.05451v1…