Rehearsal: A Configuration Verification Tool for Puppet
Rian Shambaugh, Aaron Weiss, Arjun Guha

TL;DR
Rehearsal is a verification tool that analyzes Puppet configurations for determinism and correctness, helping prevent configuration-related outages in large-scale data centers.
Contribution
It provides a sound, complete, and scalable determinacy analysis for Puppet configurations using formal semantics and SMT solving techniques.
Findings
Rehearsal successfully detects non-deterministic configurations.
It verifies idempotency and other properties of Puppet scripts.
Applied to real-world configurations, it improves reliability.
Abstract
Large-scale data centers and cloud computing have turned system configuration into a challenging problem. Several widely-publicized outages have been blamed not on software bugs, but on configuration bugs. To cope, thousands of organizations use system configuration languages to manage their computing infrastructure. Of these, Puppet is the most widely used with thousands of paying customers and many more open-source users. The heart of Puppet is a domain-specific language that describes the state of a system. Puppet already performs some basic static checks, but they only prevent a narrow range of errors. Furthermore, testing is ineffective because many errors are only triggered under specific machine states that are difficult to predict and reproduce. With several examples, we show that a key problem with Puppet is that configurations can be non-deterministic. This paper presents…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware System Performance and Reliability · Software Engineering Research · Advanced Software Engineering Methodologies
