Interpreted Formalisms for Configurations

TL;DR

This paper proposes interpreted formalisms based on real-world types in Coq to improve configuration specification, checking, and validation, reducing errors and enhancing safety in complex systems.

Contribution

It introduces a formal approach using subset types in Coq for richer, proof-based configuration validation with automated proof scripts.

Findings

Enhanced configuration validation through proof-based checking

Automated proof scripts streamline configuration consistency verification

Case study demonstrates improved configuration optimization in Hadoop

Abstract

Imprecise and incomplete specification of system \textit{configurations} threatens safety, security, functionality, and other critical system properties and uselessly enlarges the configuration spaces to be searched by configuration engineers and auto-tuners. To address these problems, this paper introduces \textit{interpreted formalisms based on real-world types for configurations}. Configuration values are lifted to values of real-world types, which we formalize as \textit{subset types} in Coq. Values of these types are dependent pairs whose components are values of underlying Coq types and proofs of additional properties about them. Real-world types both extend and further constrain \textit{machine-level} configurations, enabling richer, proof-based checking of their consistency with real-world constraints. Tactic-based proof scripts are written once to automate the construction of proofs, if proofs exist, for configuration fields and whole configurations. \textit{Failures to prove} reveal real-world type errors. Evaluation is based on a case study of combinatorial optimization of Hadoop performance by meta-heuristic search over Hadoop configurations spaces.