Automating System Configuration

TL;DR

This paper introduces a flexible, automated framework for configuring complex systems modeled as state machines, utilizing model checking and SMT solving to enhance scalability, optimize configurations, and improve human understandability.

Contribution

The paper presents a novel, modular framework that automates system configuration using SMT-based model checking, applicable across various domains and capable of optimization.

Findings

Successfully configured a CGRA memory tile for image processing applications.

Demonstrated scalability and flexibility of the framework across different system configurations.

Showed that optimized configurations are more understandable to humans.

Abstract

The increasing complexity of modern configurable systems makes it critical to improve the level of automation in the process of system configuration. Such automation can also improve the agility of the development cycle, allowing for rapid and automated integration of decoupled workflows. In this paper, we present a new framework for automated configuration of systems representable as state machines. The framework leverages model checking and satisfiability modulo theories (SMT) and can be applied to any application domain representable using SMT formulas. Our approach can also be applied modularly, improving its scalability. Furthermore, we show how optimization can be used to produce configurations that are best according to some metric and also more likely to be understandable to humans. We showcase this framework and its flexibility by using it to configure a CGRA memory tile for various image processing applications.