Name
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. |
Year | Venue | Field |
|---|---|---|
2017 | arXiv: Logic in Computer Science | Discrete mathematics,Algebra,Critical system,Combinatorial optimization,Mathematical proof,Rotation formalisms in three dimensions,Mathematics,Scripting language |
DocType | Volume | Citations |
Journal | abs/1712.04982 | 0 |
PageRank | References | Authors |
0.34 | 0 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chong Tang | 1 | 31 | 4.02 |
| Kevin Sullivan | 2 | 1724 | 180.24 |
| Jian Xiang | 3 | 0 | 2.70 |
| Trent Weiss | 4 | 0 | 0.34 |
| Baishakhi Ray | 5 | 737 | 34.84 |