Large-scale modern datacenters and cloud computing have turned system configuration into a challenging and urgent problem. Several widely-publicized outages have been blamed not on software bugs, but on software configuration issues. To cope, thousands of organizations now use system configuration languages to manage their computing infrastructure. Of these languages, Puppet is the most widely used with over 18,000 paying customers and several more open-source users. The heart of Puppet is a declarative domain-specific language that describes the state of a system. Although Puppet performs some basic static checks, there are several opportunities for errors to occur. Furthermore, testing is ineffective because many errors are only triggered under specific machine states that are difficult to predict and reproduce.

This paper presents Rehearsal, a verification tool for Puppet configurations. We first illustrate the kinds of errors that occur in Puppet with several examples. We show that the key issue is that configurations can easily be non-deterministic, thus Rehearsal implements a sound, complete, and scalable determinacy analysis for Puppet. To develop it, we (1) present a formal model for Puppet configurations, (2) use two different program analyses to prune our models to a tractable size, and (3) frame determinism-checking as an SMT problem. Rehearsal then leverages the determinacy analysis to check other important properties, such as idempotency. Finally, we apply Rehearsal to several real-world Puppet configurations.