Incremental units-of-measure verification

TL;DR

This paper introduces a lightweight, scalable static verification system for units-of-measure in Fortran programs, enabling incremental annotation and modular constraint solving for large scientific codebases.

Contribution

It presents a novel global constraint-based approach for units verification that supports incremental annotation and scalable modular analysis in Fortran.

Findings

Supports partial program annotation and inference of units.

Enables modular verification by partitioning global constraints.

Implemented as an extension to an open-source Fortran analysis tool.

Abstract

Despite an abundance of proposed systems, the verification of units-of-measure within programs remains rare in scientific computing. We attempt to address this issue by providing a lightweight static verification system for units-of-measure in Fortran programs which supports incremental annotation of large projects. We take the opposite approach to the most mainstream existing deployment of units-of-measure typing (in F#) and generate a global, rather than local, constraints system for a program. We show that such a system can infer (and check) polymorphic units specifications for under-determined parts of the program. Not only does this ability allow checking of partially annotated programs but it also allows the global constraint problem to be partitioned. This partitioning means we can scale to large programs by solving constraints for each program module independently and storing inferred units at module boundaries (separate verification). We provide an implementation of our approach as an extension to an open-source Fortran analysis tool.