Lightweight annotations for program optimisation

Performance is often critical in scientific computing particularly in large simulation models. This project looks at supporting the optimisation of Fortran programs. Our experience is that many research groups in the sciences use Fortran for large computer models, and have done so for decades. Many high-profile models in active use are also still developed in Fortran, e.g. the Met Office Unified Model used for weather and climate prediction (which now contains around 1 million lines of code). In industry, any company which began software development in the 1960-70s is also likely to have a significant investment in the language.
The work proposed for this studentship comprises three parts. The first two concern themselves with preserving and unlocking new optimisations. The third concerns itself with preserving safety by controlling the scope of potentially unsafe optimisations. Scientific computing models tend to be developed over long periods of time by multiple teams of people and so we are particularly interested in supporting software longevity and reuse. Supporting software maintenance in this environment is challenging. Indeed, the literature talks of a widening chasm between software engineering and scientific computing.
Part 1: Annotations to preserve program properties for optimisation
In order to apply an optimisation without changing program behaviour the compiler must first establish various program properties. For example, the compiler must check that there are no loop-carried dependencies before generating code to exe-cute the body of a loop in parallel on multiple cores. An expert programmer will of-ten deliberately write code to allow such optimisations to apply. However, future maintainers of the code could easily overlook these more subtle aspects of a pro-gram and thus unwittingly remove optimisations. We hypothesise that there are a relatively small number of fundamental properties which unlock many of the optimisations in modern compilers. Once identified a set of source-level annotations (and accompanying verification) could be developed which will allow programmers to assert particular optimisation properties of their program and thus better communicate their intent to future maintainers of their software.
Part 2: Annotations to assert program properties
Compilers such as GCC provide annotations to allow a programmer to assert that a property holds. For example #pragma GCC ivdep asserts that there are no loop-carried dependencies. This is used to allow a compiler to apply an optimisation in situations which normally it cannot show to be safe. However, there is little to no interaction between the programmer and the compiler as to where these annotations are required. This work would involve identifying parts of the program where optimisation properties might, but cannot be shown, to hold and providing a suitable interface to allow a programmer to select the ones which are safe. This might be combined with automated test generation to test such assertions at runtime.
Part 3: Annotations to preserve safety
Some classes of program optimisation are mostly safe. For example, floating-point arithmetic is not associative but in very many cases it is safe to reorder terms because the effect is below the level of precision required by the answer. Currently developers can choose which optimisations to apply per compilation unit but it would be safer to allow the programmer to annotate sensitive code so as to disable particular optimisations for that region. Again, this might be combined with automated test generation which establishes at runtime that unsafe optimisations have not been applied, or to establish the effect of unsafe optimisations.
The main scientific novelty of this project is to improve communication between compilers and programmers.