Metraipolis › archive › dc_f97c445a4db6

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

Source: arXiv (en)
Original: https://arxiv.org/abs/2608.05451
License (as archived): CC0-1.0
Archived: 2026-10-31T10:50:28.216Z
SHA-256 of the archived text: 95cc441ddfd2fb8f689d7e43ef3d43e73b2457888da3b5f676c3136ee1d4b575
Stable URL of this page: https://metraipolis.com/documento/dc_f97c445a4db6

How to cite

Let it Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow — arXiv:2608.05451 — arXiv (en), https://arxiv.org/abs/2608.05451 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_f97c445a4db6 (Metraipolis archive dc_f97c445a4db6, sha256 95cc441ddfd2fb8f689d7e43ef3d43e73b2457888da3b5f676c3136ee1d4b575)

BibTeX

@misc{dcf97c445a4db6,
  title = {Let it Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow — arXiv:2608.05451},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.05451},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_f97c445a4db6; sha256 95cc441ddfd2fb8f689d7e43ef3d43e73b2457888da3b5f676c3136ee1d4b575},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2608.05451. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-08-07 in cs.LO).
Categorie arXiv: Programming Languages (cs.PL) ; Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2608.05451 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-31T10:38:07.105Z dalla pagina https://arxiv.org/catchup/cs.LO/2026-08-07?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).