skip to main content
10.1145/1134285.1134323acmconferencesArticle/Chapter ViewAbstractPublication PagesicseConference Proceedingsconference-collections
Article

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

Published: 28 May 2006 Publication History

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]
E. E. Allen, D. Chase, V. Luchangco, J.-W. Maessen, and G. L. Steele Jr. Object-oriented units of measurement. In OOPSLA, pages 384--403, 2004.
[2]
E. Anderson, Z. Bai, C. Bischof, S. Blackford, J. Demmel, J. Dongarra, J. Du Croz, A. Greenbaum, S. Hammarling, A. McKenney, and D. Sorensen. LAPACK Users' Guide. Society for Industrial and Applied Mathematics, third edition, 1999.
[3]
T. Antoniu, P. A. Steckler, S. Krishnamurthi, E. Neuwirth, and M. Felleisen. Validating the unit correctness of spreadsheet programs. In ICSE, pages 439--448, 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]
R. Cunis. A package for handling units of measure in lisp. Lisp Symb. Comput., V(2):27--34, 1992.
[7]
M. Das, S. Lerner, and M. Seigle. ESP: path-sensitive program verification in polynomial time. In PLDI, pages 57--68, 2002.
[8]
J. S. Foster, M. Fähndrich, and A. Aiken. A theory of type qualifiers. In PLDI, pages 192--203, 1999.
[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]
P. N. Hilfinger. An Ada package for dimensional analysis. ACM Trans. Program. Lang. Syst., 10(2):189--203, 1988.
[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]
A. Kennedy. Dimension types. In ESOP, pages 348--362, 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]
G. S. Novak. Conversion of units of measurement. IEEE Trans. Softw. Eng., 21(8):651--661, 1995.
[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]
J. Rehof and M. Fähndrich. Type-based flow analysis: From polymorphic subtyping to CFL-reachability. In POPL, pages 54--66, 2001.
[23]
T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, pages 49--61, 1995.
[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.

Cited By

View all
  • (2023)Managing Quantities and Units of Measurement in Code BasesUpdates on Software Usability10.5772/intechopen.108014Online publication date: 22-Feb-2023
  • (2023)Fail through the Cracks: Cross-System Interaction Failures in Modern Cloud SystemsProceedings of the Eighteenth European Conference on Computer Systems10.1145/3552326.3587448(433-451)Online publication date: 8-May-2023
  • (2023)Acknowledging Implementation Trade-Offs When Developing with Units of MeasurementModel-Driven Engineering and Software Development10.1007/978-3-031-38821-7_2(25-47)Online publication date: 4-Aug-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ICSE '06: Proceedings of the 28th international conference on Software engineering
May 2006
1110 pages
ISBN:1595933751
DOI:10.1145/1134285
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 May 2006

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Gaussian elimination
  2. constraint-based analysis
  3. dimensional analysis
  4. measurement units
  5. type systems

Qualifiers

  • Article

Conference

ICSE06
Sponsor:

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)11
  • Downloads (Last 6 weeks)0
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Managing Quantities and Units of Measurement in Code BasesUpdates on Software Usability10.5772/intechopen.108014Online publication date: 22-Feb-2023
  • (2023)Fail through the Cracks: Cross-System Interaction Failures in Modern Cloud SystemsProceedings of the Eighteenth European Conference on Computer Systems10.1145/3552326.3587448(433-451)Online publication date: 8-May-2023
  • (2023)Acknowledging Implementation Trade-Offs When Developing with Units of MeasurementModel-Driven Engineering and Software Development10.1007/978-3-031-38821-7_2(25-47)Online publication date: 4-Aug-2023
  • (2022)SA4U: Practical Static Analysis for Unit Type Error DetectionProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3556937(1-11)Online publication date: 10-Oct-2022
  • (2022)High Assurance Software for Financial Regulation and Business PlatformsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_6(108-126)Online publication date: 14-Jan-2022
  • (2021)An Empirical Study on Type AnnotationsACM Transactions on Software Engineering and Methodology10.1145/343977530:2(1-29)Online publication date: 10-Feb-2021
  • (2021)Understanding Bounding Functions in Safety-Critical UAV SoftwareProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00119(1311-1322)Online publication date: 22-May-2021
  • (2021)How Do Programmers Express High-Level Concepts using Primitive Data Types?2021 28th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC53868.2021.00043(360-368)Online publication date: Dec-2021
  • (2021)Fortress Abstractions in X10 FrameworkInternational Journal of Parallel Programming10.1007/s10766-021-00719-wOnline publication date: 15-Jul-2021
  • (2020)Precise inference of expressive units of measurement typesProceedings of the ACM on Programming Languages10.1145/34282104:OOPSLA(1-28)Online publication date: 13-Nov-2020
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media