Meeting on Testing and Verification for Computational Science
By Dominic Orchard, Research Associate, Computer Laboratory, University of Cambridge and Institute Fellow.
The need for more rigorous software verification in science is well known. The presence of software errors can seriously undermine results leading to paper retractions, bad policy decisions, and even catastrophic technological failures. Often the responsibility is placed on the programmer, but simply trying to be more careful is not enough. There is a wealth of research in computer science aimed at automating testing and verification, yet little of this has crossed over into practice in the sciences. In April 2016, we held a meeting in Cambridge on Testing and Verification for Computational Science to bridge the gap between computer scientists and natural scientists concerned with software correctness.
Before computer science became a discipline, computing existed mainly as a service to science, providing fast and accurate calculation. As computer science developed, it pulled in philosophy, logic, mathematics, semantics, and engineering but has largely moved away from its roots in science. This has lead to a gulf between computer science and the natural and physical sciences. While there have been many advances in program verification, little of this is applied to address the correctness of scientific software. This meeting was organised to bring together computer scientists and natural/physical scientists to discuss recent work and new ideas in this area.
The Software Sustainability Institute sponsored the meeting through Dominic Orchard, a 2015 Institute fellow and researcher in this area. The meeting lasted a full afternoon at the Computer Laboratory in the University of Cambridge, followed by dinner in the evening at Queens' College. Roughly 30 academics attended, with approximately half from a computer science background and half from science. Attendees came from Cambridge, Oxford, Southampton, Bath, London, and Paris. We had ten talks, with five from computer science and High-Performance Computing experts, and five from research scientists. To emphasise the breadth of work being undertaken, we deliberately alternated between computer science and science-oriented talks. A brief summary is included here (not in order of presentation), but full abstracts and slides are available at the meeting website.
Sylvie Boldo (INRIA, Orsay, France) gave the keynote presentation From mathematics to programs: a verification journey. Sylvie overviewed her work on fully verifying numerical code end-to-end, that is, from the mathematical model, its discretisation and approximation, through to the implementation and all the low-level details (e.g., floating-point errors). This showed what is possible with state-of-the-art tools and techniques, but the effort required is still very high (taking several advanced researchers many months). This raises open questions about how to make such techniques plausible for non-experts in the future.
David Shorthouse (MRC Cancer Unit, Cambridge) showed his work on modelling cancer metastasis using Linear Temporal Logic (LTL) to describe and check stability properties of the model. This showed the application of logic-based techniques from computer science to verify models in a biological domain. Benjamin Hall (also of MRC Cancer Unit) later showed the BioModelAnalyzer tool for rapid development of gene and protein-interaction models that allows users to query properties of models expressed as LTL formulae. This allows biologists to verify complex model properties with an easy-to-use graphical tool.
Alessandro Abate (Department of Computer Science, University of Oxford) described his work on using statistical techniques to verify properties of abstract models of complex physical systems (in, for example, systems biology and avionics). He gave an overview of techniques used to refine complex models into more simple models that still reflect the desired properties of a system. These techniques are provided in the FAUST tool for abstracting discrete time Markov processes. Related to the stochastic model world, Matthew Patrick (Department of Plant Sciences, University of Cambridge) discussed his work on testing stochastic models in epidemiology. Normal testing techniques cannot be used as-is for stochastic models since they exhibit a different behaviour on each run. Instead, testing tools must produce multiple executions and provide statistical results, rather than a binary pass/fail. Matthew’s work includes automatic parameter search techniques for identifying the parameter ranges that produce results with particular (statistical) characteristics.
Stephen Kell (Computer Laboratory, University of Cambridge) presented an overview of different dynamic monitoring and tracing technologies that could aid the development of numerical algorithms in science. For example, he demonstrated his libcrunch C library which provides more detailed error messages than usual (e.g., replacing the classic ‘Segmentation Fault’ error with a trace of where the error arises). He proposed that there is a lot of unexploited potential for useful testing, bug finding, and reproducibility features to be provided lower down in the software stack (at the level of operating systems, compilers, and linkers).
James Davenport (Computer Science and Mathematical Sciences, University of Bath, and 2016 SSI Fellow) gave an overview of research data classifying programming errors common in software. He went on to discuss problem associated with optimising compilers changing the results of numerical programs and proposed (amongst other ideas) documenting more carefully when a piece of code is sensitive to certain algebraic optimisations.
Filippo Spiga (High Performance Computing Service, University of Cambridge) gave a discussion of problems faced in High Performance Computing and lessons learnt on what working practices need improving in the community, including the use of versioning, better documentation, automated test frameworks to allow frequent testing, using common data representations, and sharing data more widely.
Nick Maclaren (University of Cambridge) gave a historical overview of developments in verification over the years for C, C++, and Fortran (all popular in science) and discussed various ideas on future directions. He argued that, in an ideal world, there would be simpler languages that more clearly separate concerns to reduce human error and aid verification, for example, not allowing arbitrary pointer manipulation, or having a way to mark code as free-from side effects. He also suggested that compilers could do more program verification themselves since they already have to do various internal checks as part of the optimisation logic.
Luke Abraham (Department of Chemistry and Centre for Atmospheric Science, Cambridge) gave an insight into the testing methodology employed by the Met Office Unified Model (which has over a million lines of code and 200 developers).
Overall, the breadth and depth of the talks gave a sense of the challenges faced and an exciting glimpse at the state-of-the-art in verification and testing techniques applied to numerical and scientific domains. There are many solutions which have yet to be applied widely and many problems without a solution yet. For example, the verification techniques explained by Sylvie Boldo in the keynote provide a very high-level of assurance but require significant user effort: her talk showed a 32 line C program whose full verification relies on 154 lines of manual specification and 33 out of 150 theorems to be proved manually using the Coq proof tool. An open question therefore is how to make such techniques more accessible, or whether greater automation is possible to ease the adoption effort. A problem without a clear solution yet, highlighted in a number of talks, is how to understand and manage the numerical sensitivity of models with respect to compiler optimisations, choice of platform, their particular input parameters, and parallelisation strategy. These outstanding problems and underused solutions highlight the need for further interaction, meetings, workshops, collaborations, and projects bringing together computer scientists with natural and physical scientists. We hope to run the event again next year and are considering a mixture of informal talks and more formal talks with publications.
Thanks to the Software Sustainability Institute for supporting this workshop, as well as the EPSRC via the grant CamFort: Automated evolution and verification of computational science models.
Since writing this blog post, Dominic has taken up a lectureship in the School of Computing at the University of Kent and continues to work on the CamFort grant with the team at Cambridge.