Forward Build Systems, Formally

TL;DR

This paper formally defines the correctness of forward build systems, proves the correctness of systems like Rattle, Fabricate, and Memoize, and models them in Agda to ensure reliable dependency management in software builds.

Contribution

It provides a formal correctness definition for forward build systems and verifies the correctness of several systems using Agda, addressing a gap in build system reliability.

Findings

Rattle's optimizations preserve correctness

Fabricate and Memoize are also correct

Formal modeling in Agda supports build system correctness

Abstract

Build systems are a fundamental part of software construction, but their correctness has received comparatively little attention, relative to more prominent parts of the toolchain. In this paper, we address the correctness of \emph{forward build systems}, which automatically determine the dependency structure of the build, rather than having it specified by the programmer. We first define what it means for a forward build system to be correct -- it must behave identically to simply executing the programmer-specified commands in order. Of course, realistic build systems avoid repeated work, stop early when possible, and run commands in parallel, and we prove that these optimizations, as embodied in the recent forward build system \textsc{Rattle}, preserve our definition of correctness. Along the way, we show that other forward build systems, such as \textsc{Fabricate} and \textsc{Memoize}, are also correct. We carry out all of our work in \Agda, and describe in detail the assumptions underlying both \textsc{Rattle} itself and our modeling of it.