PI: James Mckinna, Co-I: Perdita Stevens, University of Edinburgh

  • Build systems form part of the critical infrastructure of modern software development.
  • Unlike for compilers, there has been little formal modelling or verification of build systems.
  • This is a pilot project to explore the development of formal models of some existing systems (make, pluto) in an interactive theorem proving system. 
  • The aim is to develop new conceptual, and formal foundations in this area

Build systems form part of the critical infrastructure of modern software development, but unlike compilers they have not been so much the focus of formal modelling or verification. Many users might be familiar with the Unix workhouse tool ‘make’, but notwithstanding superficial advances, progress beyond it has been slow. This 9-month pilot project aims to develop formal models of some existing systems (make, pluto) in an interactive theorem proving system, with a view to providing more secure foundations for future work in this area. The ultimate aim is to develop new conceptual, and formal foundations in this area, and use them to increase confidence in contemporary software engineering practices.

The project focussed on the pluto build system, with the aim of formalising of the basic algorithm as a collection of mutually inductive definitions, following McKinna et al. (2009) “Programming Reachability Algorithms in Coq”, which is unusual in being an approach to imperative program verification in a type-theoretic setting. An initial formalisation of the basic pluto algorithms and data-structures in Agda was created: this revealed many subtleties resulting from the impedance (mis)match between the set-theoretic/object-oriented model underlying pluto, and its realisation in constructive type theory.

Further work was done on trying to match the object-oriented model underlying pluto with the functional decomposition identified in the Mokhov et al. “A la carte“ paper, with difficulties arising with respect to identifying a distinct “scheduler” component or scheduling policy in the pluto model.

Little progress has been made on the general abstract proof search model of build systems, and its relation to extensions of the ‘compiler forest’ model. In retrospect, the proposal was too ambitious in aiming to tackle this problem at this stage.

PUBLICATIONS. P. Stevens, “Connecting Software Build with Maintaining Consistency between Models: Towards Sound, Optimal, and Flexible Building from Megamodels”, Software and Systems Modeling volume 19, pages 935–958 (2020).