Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Incremental units-of-measure verification

Matthew Danish, Dominic Orchard, Andrew Rice

TL;DR

This paper addresses the challenge of verifying units-of-measure in scientific Fortran programs by introducing a lightweight, incrementally adoptable static verification system. It adopts a global constraint-solving approach over unit variables and uses a modified Hermite Normal Form to infer and check polymorphic units across modular Fortran code, enabling interprocedural polymorphism and scalable analysis. The authors implement the approach as an extension of CamFort, demonstrate module-based partitioning with fsmod files, and show practical improvements in scalability and real-world case studies such as the Weather Research and Forecast Model, including detection of undocumented unit conversions. The work significantly reduces the burden of annotating large legacy codebases while providing precise, static guarantees about unit consistency, with potential to prevent costly numerical errors in scientific computing.

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.

Incremental units-of-measure verification

TL;DR

This paper addresses the challenge of verifying units-of-measure in scientific Fortran programs by introducing a lightweight, incrementally adoptable static verification system. It adopts a global constraint-solving approach over unit variables and uses a modified Hermite Normal Form to infer and check polymorphic units across modular Fortran code, enabling interprocedural polymorphism and scalable analysis. The authors implement the approach as an extension of CamFort, demonstrate module-based partitioning with fsmod files, and show practical improvements in scalability and real-world case studies such as the Weather Research and Forecast Model, including detection of undocumented unit conversions. The work significantly reduces the burden of annotating large legacy codebases while providing precise, static guarantees about unit consistency, with potential to prevent costly numerical errors in scientific computing.

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.
Paper Structure (37 sections, 3 theorems, 21 equations, 14 figures, 2 tables)

This paper contains 37 sections, 3 theorems, 21 equations, 14 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Overview
  3. Annotating and Checking Units-of-Measure
  4. Polymorphic Units Annotation
  5. Modular Fortran
  6. Inference algorithm
  7. Units Constraints
  8. Expressions
  9. Literals
  10. Casting
  11. Monomorphism restriction for nonzero literals
  12. Function calls
  13. Statements and Blocks
  14. Program Units
  15. Interprocedural Polymorphic Instantiation
  16. ...and 22 more sections

Key Result

lemma 1

For every pivot $p_{i,j}$ detected that does not divide every integer in its row, the resulting matrix after the loop body completes will have two additional pivots equal to 1. One of them will be at column $j$ and one will be at some column greater than $j$.

Figures (14)

  • Figure 1: Annotation syntax: units specification and aliases
  • Figure 2: Simplified Fortran syntax
  • Figure 3: Rules for expressions (apart from literals, see Figure \ref{['fig:literalrules']})
  • Figure 4: Rules for literal expressions
  • Figure 5: Rules for statements
  • ...and 9 more figures

Theorems & Definitions (10)

  • definition 1: Units syntax and representation
  • definition 2
  • definition 3: Instantiation
  • definition 4: Hermite Normal Form
  • lemma 1
  • proof
  • theorem 1
  • proof
  • theorem 2
  • proof