Puppet is a popular computer system configuration management tool. It provides abstractions that model system resources, enabling administrators to set up their computer systems. Its use suffers from two potential pitfalls. First, if ordering constraints are not correctly specified whenever a Puppet resource depends on another, the non-deterministic application of resources can lead to race conditions and consequent failures. Second, if a service is not tied to its resources (through the notification construct), the system may operate in a stale state whenever a resource gets modified and the update is not propagated to the corresponding service. Such faults can degrade a computing infrastructure’s availability and functionality.

We have developed an approach that identifies these issues through the analysis of a Puppet program and its system call trace. Specifically, we present a formal model for traces, which allows us to capture the interactions of Puppet resources with the file system. By analyzing these interactions we identify (1) resources that are related to each other (e.g., operate on the same file), and (2) resources that should act as notifiers so that changes are correctly propagated. We then check the relationships from the trace’s analysis against the program’s dependency graph: a representation containing all the ordering constraints and notifications declared in the program. If a mismatch is detected, our system reports a potential fault.

We have evaluated our method on a large set of popular Puppet modules, and discovered 66 previously unknown issues in 30 of them. Benchmarking further shows that our approach can analyze in seconds real-world configurations with a magnitude measured in thousands of lines and millions of system calls.