Abstract
System configuration languages are now widely used to drive the deployment and evolution of large computing infrastructures. Most such languages are highly informal, making it difficult to reason about configurations, and introducing an important source of failure. We claim that a more rigorous approach to the development and specification of these languages will help to avoid these difficulties and bring a number of additional benefits. In order to test this claim, we present a formal semantics for the core of the SmartFrog configuration language. We demonstrate how this can be used to prove important properties such as termination of the compilation process. To show that this also contributes to the practical development of clear and correct compilers, we present three independent implementations, and verify their equivalence with each other, and with the semantics. Supported by an extended example from a real configuration scenario, we demonstrate how the process of develo** the semantics has improved understanding of the language, highlighted problem areas, and suggested alternative interpretations. This leads us to advocate this approach for the future development of practical configuration languages.
Similar content being viewed by others
Notes
The concrete syntax of this formal representation is a:c.
This is equivalent to a map data structure.
References
Ansible: http://ansibleworks.com. Accessed 25 Feb 2014
Cfengine: http://cfgengine.com. Accessed 25 Feb 2014
Chef: http://getchef.com. Accessed 25 Feb 2014
LCFG: http://www.lcfg.org. Accessed 25 Feb 2014
Puppet: http://puppetlabs.com. Accessed 25 Feb 2014
Vervloesem, K.: FOSDEM Configuration Management Meeting Report, Feb 2011
Oppenheimer, D., Ganapathy, G., Patterson, D.: Why do internet services fail and what can be done about it? In: 4th Usenix Symposium on Internet Technologies and Systems (2003)
Anderson, P., Cheney, J.: Toward provenance-based security for configuration languages. In: The 4th Usenix Workshop on the Theory and Practice of Provenance (2012)
SmartFrog: http://www.smartfrog.org. Accessed 25 Feb 2014
Herry, H., Anderson, P.: Planning with global constraints for computing infrastructure reconfiguration. In: CP4PS-12—The AAAI-12 Workshop on Problem Solving using Classical Planners (2012)
Hewson, J.A., Anderson, P., Gordon, A.D.: Constraint-based autonomic configuration. In: Proceedings of 2013 Self-adaptive and Self-organizing Systems Conference (SASO), Sept 2013
Self: http://selflanguage.org. Accessed 1 March 2014
YAML: http://www.yaml.org/spec/. Accessed 10 April 2014
Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Boston (1986)
Stoy, J.E.: Denotational Semantics: The Scott–Strachey Approach to Programming Language Theory. The MIT Press, Cambridge (1977)
Hewson, J.A., Anderson, P., Gordon, A.D.: A declarative approach to automated configuration. In: Proceedings of the 2012 LISA Conference. Usenix Association (2012)
Couch, A.: From x-1 to (setf x 1): what does configuration management mean? USENIX Login 33(1), 12–18 (2008)
Couch, A., Sun, Y.: On observed reproducibility in network configuration management. Sci Comput Program 53(2), 215–253 (2004). Topics in System Administration
Bekezhanova, A.: Denotational semantics of puppet. Master’s thesis, School of Informatics, University of Edinburgh (2013)
Hilty, M., Pretschner, A., Basin, D., Schaefer, C., Walter, T.: A policy language for distributed usage control. In: Biskup, J., López, J. (eds.) Computer Security—ESORICS 2007, Volume 4734 of Lecture Notes in Computer Science, pp. 531–546. Springer, Berlin (2007)
Aktug, I., Naliuka, K.: Conspec—a formal language for policy specification. Sci Comput Program 74(1–2), 2–12 (2008). Special Issue on Security and Trust
Damianou, N.: A policy framework for management of distributed systems. PhD thesis, Imperial College (2002)
Classen, A., Hubaux, A., Heymans, P.: A formal semantics for multi-level staged configuration. Technical report, University of Namur (2009)
Favre, J.-M.: CPP denotational semantics. In: Proceedings of the Third International Workshop on Source Code Analysis and Manipulation, p. 22. IEEE Computer Society (2003)
Herry, H.: Automated Planning for Cloud Service Configurations. PhD thesis, School of Informatics, University of Edinburgh (2014)
Demonstration SmartFrog compilers based on the formal semantics. https://github.com/herry13/smartfrog-lang. Accessed 28 March 2014
Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP ’00, pp. 268–279. ACM, New York. (2000)
Microsoft Desired State Configuration. http://technet.microsoft.com/en-us/library/dn249912.aspx. Accessed 13 Nov 2014
DMTF MOF Format. http://www.dmtf.org/sites/default/files/standards/documents/dsp0221_3.0.0.pdf. Accessed 13th Nov 2014
Unruh, I., Bardas, A.G., Zhuang, R., Ou, Z., DeLoach, S.A.: Compiling abstract specifications into concrete systems—bringing order to the cloud. In: Proceedings of the 28th Large Installation Systems Adminstration Conference (LISA14), pp. 17–33. Usenix Association (2014)
IPTables: http://en.wikipedia.org/wiki/iptables. Accessed 10 Nov 2014
Anderson, P.: LCFG: A Practical Tool for System Configuration, Volume 17 of Short Topics in System Administration. Usenix Association (2008)
Acknowledgments
This work has been partially supported by an HP Labs Innovation Research Program Award, and we would like to thank Patrick Goldsack for his help in clarifying the SmartFrog semantics and implementation. It is also partially sponsored by the Air Force Office of Scientific Research, Air Force Material Command, USAF, under Grant Number FA8655-13-1-3006. The U.S. Government and University of Edinburgh are authorized to reproduce and distribute reprints for their purposes notwithstanding any copyright notation thereon.
Author information
Authors and Affiliations
Corresponding author
Additional information
Herry Herry did part of the work for this paper while being a PhD student at School of Informatics, University of Edinburgh.
Appendices
Appendix 1: Concrete Syntax
Appendix 2: Manually Created Tests
The following examples show some of the manually-created test cases:
Appendix 3: Auto-Generated Tests
The following SF code is part of a randomly-generated, semantically-correct specification used for testing compatibility between the implementations:
Rights and permissions
About this article
Cite this article
Anderson, P., Herry, H. A Formal Semantics for the SmartFrog Configuration Language. J Netw Syst Manage 24, 309–345 (2016). https://doi.org/10.1007/s10922-015-9351-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10922-015-9351-y