Osprey: a practical type system for validating dimensional unit correctness of C programs

ABSTRACT

Misuse of measurement units is a common source of errors in scientific applications, but standard type systems do not prevent such errors. Dimensional analysis in physics can be used to manually detect such errors in physical equations. It is, however, not feasible to perform such manual analysis for programs computing physical equations because of code complexity. In this paper, we present a type system to automatically detect potential errors involving measurement units. It is constraint-based: we model units as types and flow of units as constraints. However, standard type checking algorithms are not powerful enough to handle units because of their abelian group nature (e.g., being commutative, multiplicative, and associative). Our system combines techniques such as type inference and Gaussian Elimination to overcome this problem. We have implemented Osprey, a prototype of the system for C programs, and evaluated it on various test programs, including computational physics and mechanical engineering applications. Osprey discovered unknown errors in mature code; it is precise with few false positives; it is also efficient and scales to large programs---we have successfully used it to analyze programs with hundreds of thousands of lines of code.

REFERENCES

• 1: Eric Allen , David Chase , Victor Luchangco , Jan-Willem Maessen , Guy L. Steele, Jr., Object-oriented units of measurement, Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 24-28, 2004, Vancouver, BC, Canada
• 2: E. Anderson , Z. Bai , C. Bischof , L. S. Blackford , J. Demmel , Jack J. Dongarra , J. Du Croz , S. Hammarling , A. Greenbaum , A. McKenney , D. Sorensen, LAPACK Users' guide (third ed.), Society for Industrial and Applied Mathematics, Philadelphia, PA, 1999
• 3: Tudor Antoniu , Paul A. Steckler , Shriram Krishnamurthi , Erich Neuwirth , Matthias Felleisen, Validating the Unit Correctness of Spreadsheet Programs, Proceedings of the 26th International Conference on Software Engineering, p.439-448, May 23-28, 2004
• 4: W. E. Brown. Applied template meta-programming in SIUNITS: the library of unit-based computation, 2001.
• 5: UIUC. Maude. http://maude.cs.uiuc.edu/.
• 6: Roman Cunis, A package for handling units of measure in Lisp, Lisp and Symbolic Computation, v.V n.2, p.27-34, April–June, 1992
• 7: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 8: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 9: H. Hanche-Olsen. Buckingham's π Theorem. http://www.math.ntnu.no/~hanche/notes/buckingham/buckingham-a5.pdf, 2004.
• 10: C. Harrelson. Program Analysis Mode (PAM) for Emacs. http://www.cs.berkeley.edu/~chrishtr/pam/.
• 11: Paul N. Hilfinger, An Ada package for dimensional analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.189-203, April 1988 [doi>10.1145/42190.42346]
• 12: International Systems of Units (SI). http://physics.nist.gov/cuu/Units/.
• 13: L. Jiang and Z. Su. Osprey: A practical type system for validating unit correctness of C programs. http://www.cs.ucdavis.edu/~su/unitfull.pdf, 2005.
• 14: R. Johnson and D. Wagner. Finding user/kernel pointer bugs with type inference. In USENIX Security Symposium, pages 119--134, 2004.
• 15: M. Keller. Eiffel Library for Units of Measurement. http://se.inf.ethz.ch/projects/markus_keller/EiffelUnits.html.
• 16: Andrew Kennedy, Dimension Types, Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems, p.348-362, April 11-13, 1994
• 17: J. Kodumal. Banshee--A toolkit for building constraint-based analysis. http://banshee.sourceforge.net/.
• 18: Mars Climate Orbiter Mishap Investigation. ftp://ftp.hq.nasa.gov/pub/pao/reports/1999/MCO_report.pdf.
• 19: Gordon S. Novak, Jr., Conversion of Units of Measurement, IEEE Transactions on Software Engineering, v.21 n.8, p.651-661, August 1995 [doi>10.1109/32.403789]
• 20: W. H. Press, S. A. Teukolsky, W. T. Vetterling, and B. P. Flannery. Numerical Recipes. Cambridge University Press, http://www.nr.com/, 2002.
• 21: D. Quinlan, M. Schordan, R. Vuduc, and Q. Yi. ROSE: A Compiler Framework. http://www.llnl.gov/CASC/rose/, release soon.
• 22: Jakob Rehof , Manuel Fähndrich, Type-base flow analysis: from polymorphic subtyping to CFL-reachability, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 2001, London, United Kingdom
• 23: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 24: G. Rosu and F. Chen. Certifying measurement unit safety policy. ASE, 2003.
• 25: SoftIntegration©. Ch User's Guide and Ch Mechanism Toolkit User's Guide. http://www.softintegration.com/.
• 26: M. Wand and P. O'Keefe. Automatic dimensional inference. In Computational Logic--Essays in Honor of Alan Robinson, pages 479--483, 1991.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Reliability, Verification

Keywords:
Gaussian elimination, constraint-based analysis, dimensional analysis, measurement units, type systems