This project is building a post-hoc transformation system inside a full scale Haskell compiler. This will improve the connections between Haskell models and Haskell implementations, as well allow the exploration of the powerful worker/wrapper transformation. The project is funded by the NSF.
|Title||Improving the Applicability of Haskell-Hosted Semi-Formal Models to High Assurance Development|
|Funded by||The National Science Foundation|
|Period of Performance||August 2011 - July 2015|
|Amount||$527,750 ($495,750 + 2 REUs of 16,000)|
In engineering practice, models are an essential part of understanding how to build complex systems. In this project, high-level models and efficient implementations of computer systems will be developed side-by-side under a single framework that bridges the gap between them using a high degree of automation. This is possible due to the use of a modern functional language for both the model and implementation, and the deployment of a new and powerful general-purpose and semi-automatic refinement technology. The functional language Haskell has already enjoyed considerable success as a platform for high-level modeling of complex systems with its mathematical-style syntax, state-of-the-art type system, and powerful abstraction mechanisms.
In this project, Haskell will be used to express a semi-formal model and an efficient implementation, taking the form of two distinct expressions of computation with the same mathematical foundation. The project develops tools and methodologies that use transformations like the worker/wrapper transformation to construct links between these models and implementations, lowering the cost of the development of high-assurance software and hardware components in application areas like security kernels and critical control systems. Lowering the cost of linking semi-formal specifications and models to real implementations will have considerable impact. For example, Evaluation Assurance Level (EAL) 5 and 6 of the Common Criteria call for semi-formal methods to construct such links, and this project addresses keys part of this requirement.
In engineering practice, models are an essential part of understanding how to build complex systems. In this investigation, we constructed a tool we called HERMIT, which mechanized the connections between a specific class of software models, and their programmatic counterparts. We have used HERMIT on a number of case studies, pushing the state-of-the-art in semi-formal mathematical reasoning for software development.
Functional programming is a promising approach to writing programs which are both correct and efficient. Functional programming is based on the idea of using mathematical functions to construct programs. With effort, it is possible to establish a connection between a model written in a functional language, and a fast implementation, via program transformation.
HERMIT is a software artifact that fits in the gap between mathematically formal tools for reasoning about programs, and informal techniques such as pen-and-paper derivations. HERMIT attached to the popular Glasgow Haskell compiler, the premier compiler for the lazy functional language Haskell, providing new tools and techniques for mechanizing reasoning and program transformations. This architecture allowed HERMIT to be the first system capable of directly reasoning about the full Haskell language.
Using HERMIT, we completed five case studies that connected models with implementations. These included verifying that specific critical properties of a software library hold in the given cases, running efficient simulations of cellular automata, and mechanizing a proof of program correctness. Further, two case studies improved the state-of-the-art in optimized implementations, resulting in a solution to an open problem in optimization, and providing a way to write more expressive programs without compromising the speed of the final program.
This project resulted in 11 peer-reviewed publications, one PhD dissertation, and one MS thesis. The project also supported one postdoctoral researcher. HERMIT has also been used by a number of other researchers, as a basis for prototyping advanced optimizations and compiler enhancements.
A. Gill, N. Sculthorpe, J. Dawson, A. Eskilson, A. Farmer, M. Grebe, J. Rosenbluth, R. Scott, and J. Stanton, “The remote monad design pattern,” in Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, (New York, NY, USA), pp. 59–70, ACM, 2015.
A. Farmer, N. Sculthorpe, and A. Gill, “Reasoning with the HERMIT: Tool support for equational reasoning on GHC Core programs,” in Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, (New York, NY, USA), pp. 23–34, ACM, 2015.
M. D. Adams, A. Farmer, and J. P. Magalhães, “Optimizing SYB Traversals Is Easy!,” Science of Computer Programming, vol. 112, Part 2, pp. 170 – 193, 2015. Selected and extended papers from Partial Evaluation and Program Manipulation 2014.
A. Farmer, HERMIT: Mechanized Reasoning during Compilation in the Glasgow Haskell Compiler. PhD thesis, The University of Kansas, April 2015.
B. Torrence, “The Life Changing HERMIT: A Case Study of the Worker/Wrapper Transformation,” Master’s thesis, The University of Kansas, January 2015.
N. Sculthorpe, N. Frisby, and A. Gill, “The Kansas University Rewrite Engine: A Haskell-embedded strategic programming language with custom closed universes,” Journal of Functional Programming, vol. 24, pp. 434–473, 7 2014.
A. Gill, “Domain-specific languages and code synthesis using Haskell,” Commun. ACM, vol. 57, pp. 42–49, June 2014. Also appeared in ACM Queue, Vol 12(4), April 2014.
A. Farmer, C. Höner zu Siederdissen, and A. Gill, “The HERMIT in the Stream,” in Proceedings of the 2014 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’14, ACM, 2014.
M. D. Adams, A. Farmer, and J. P. Magalhães, “Optimizing SYB Is Easy!,” in Proceedings of the 2014 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’14, ACM, 2014. Won Best Paper Award.
N. Sculthorpe, A. Farmer, and A. Gill, “The HERMIT in the tree: Mechanizing program transformations in the GHC core language,” in Proceedings of the 24th Symposium on Implementation and Application of Functional Languages, vol. 8241 of Lecture Notes in Computer Science, pp. 86–103, 2013.
N. Sculthorpe, J. Bracker, G. Giorgidze, and A. Gill, “The constrained-monad problem,” in Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, pp. 287–298, ACM, 2013.
A. Farmer, A. Gill, E. Komp, and N. Sculthorpe, “The HERMIT in the machine: A plugin for the interactive transformation of GHC core language programs,” in Proceedings of the ACM SIGPLAN Haskell Symposium, Haskell ’12, pp. 1–12, ACM, 2012.
These publications supported the original proposal.
“Deriving an efficient FPGA …” was a case study of using worker/wrapper, applied to hardware synthesis.
A. Gill and A. Farmer, “Deriving an efficient FPGA implementation of a low density parity check forward error corrector,” in Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, ICFP ’11, pp. 209–220, ACM, Sep 2011.
“The worker/wrapper transformation” was the first formalization of worker/wrapper.
A. Gill and G. Hutton, “The worker/wrapper transformation,” Journal of Functional Programming, vol. 19, pp. 227–251, March 2009.