research-article

A theory of platform-dependent low-level software

Authors:

Craig ChambersAuthors Info & Claims

ACM SIGPLAN Notices, Volume 43, Issue 1

Pages 209 - 220

https://doi.org/10.1145/1328897.1328465

Published: 07 January 2008 Publication History

Abstract

The C language definition leaves the sizes and layouts of types partially unspecified. When a C program makes assumptions about type layout, its semantics is defined only on platforms (C compilers and the underlying hardware) on which those assumptions hold. Previous work on formalizing C-like languages has ignored this issue, either by assuming that programs do not make such assumptions or by assuming that all valid programs target only one platform. In the latter case, the platform's choices are hard-wired in the language semantics.

In this paper, we present a practically-motivated model for a C-like language in which the memory layouts of types are left largely unspecified. The dynamic semantics is parameterized by a platform's layout policy and makes manifest the consequence of platform-dependent (i.e., unspecified) steps. A type-and-effect system produces a layout constraint: a logic formula encoding layout conditions under which the program is memory-safe. We prove that if a program type-checks, it is memory-safe on all platforms satisfying its constraint.

Based on our theory, we have implemented a tool that discovers unportable layout assumptions in C programs. Our approach should generalize to other kinds of platform-dependent assumptions.

References

[1]

Amal Ahmed and David Walker. The logical approach to stack typing. In International Workshop on Types in Language Design and Implementation, 2003.

Digital Library

[2]

Aleph One Limited. The ARMLinux Book Online, Chapter 10. 2005. http://www.aleph1.co.uk/armlinux/book.

[3]

Robert M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15 (4), 1993.

Digital Library

[4]

David F. Bacon. Kava: a Java dialect with a uniform object model for lightweight classes. Concurrency and Computation: Practice and Experience, 15 (3--5), 2003.

[5]

Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In 14th International Symposium on Formal Methods, 2006.

Digital Library

[6]

C Standard 1999. ISO/IEC 9899:1999, International Standard-Programming Languages-C. International Standards Organization, 1999.

[7]

Satish Chandra and Tom Reps. Physical type checking for C. In Workshop on Program Analysis for Software Tools and Engineering, 1999.

Digital Library

[8]

Juan Chen, Dinghao Wu, Andrew W. Appel, and Hai Fang. A provably sound TAL for back-end optimization. In ACM Conference on Programming Language Design and Implementation, 2003.

Digital Library

[9]

Jeremy Condit, Matthew Harren, Scott McPeak, George Necula, and Westley Weimer. CCured in the real world. In ACM Conference on Programming Language Design and Implementation, 2003.

Digital Library

[10]

Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George Necula. Dependent types for low-level programming. In European Symposium on Programming, 2007.

Digital Library

[11]

Karl Crary. Toward a foundational typed assembly language. In 30th ACM Symposium on Principles of Programming Languages, 2003.

Digital Library

[12]

Dinakar Dhurjati, Sumant Kowshik, and Vikram Adve. SAFECode: Enforcing alias analysis for weakly typed languages. In ACM Conference on Programming Language Design and Implementation, 2006.

Digital Library

[13]

Dan Grossman. Type-safe multithreading in Cyclone. In International Workshop on Types in Language Design and Implementation, 2003.

Digital Library

[14]

Dan Grossman. Quantified types in imperative languages. ACM Transactions on Programming Languages and Systems, 28 (3), 2006.

Digital Library

[15]

Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based memory management in Cyclone. In ACM Conference on Programming Language Design and Implementation, 2002.

Digital Library

[16]

Thomas Hallgren, Mark P. Jones, Rebekah Leslie, and Andrew Tolmach. A principled approach to operating system construction in Haskell. In 10th ACM International Conference on Functional Programming, 2005.

Digital Library

[17]

Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. A syntactic approach to foundational proof-carrying code. Journal of Automated Reasoning, 31 (3--4), 2003.

Digital Library

[18]

IBM. Developing embedded software for the IBM PowerPC 970FX processor. Application Note 970, IBM, 2004. http://www.ibm.com/chips/techlib/.

[19]

Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, and Yanling Wang. Cyclone: A safe dialect of C. In USENIX Annual Technical Conference, 2002.

Digital Library

[20]

Xavier Leroy. Formal certification of a compiler back-end. In 33rd ACM Symposium on Principles of Programming Languages, 2006.

Digital Library

[21]

Robert Love. Linux Kernel Development, Second Edition. Novell Press, 2005. Page 328.

Digital Library

[22]

Brad Martin, Anita Rettinger, and Jasmit Singh. Multiplatform porting to 64 bits. Dr. Dobb's Journal, 2005.

[23]

Antoine Mine. Field-sensitive value analysis of embedded c programs with union types and pointer arithmetics. In Conference on Language, Compilers, and Tool Support for Embedded Systems, 2006.

Digital Library

[24]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21 (3), 1999.

Digital Library

[25]

George Necula. Proof-carrying code. In 24th ACM Symposium on Principles of Programming Languages, 1997.

Digital Library

[26]

George Necula, Scott McPeak, Shree Prakash Rahul, and Westley Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Conference on Compiler Construction, 2002.

Digital Library

[27]

George Necula, Scott McPeak, and Westley Weimer. CCured: Type-safe retrofitting of legacy code. In 29th ACM Symposium on Principles of Programming Languages, 2002.

Digital Library

[28]

George Necula, Jeremy Condit, Matthew Harren, Scott McPeak, and Westley Weimer. CCured: Type-safe retrofitting of legacy software. ACM Transactions on Programming Languages and Systems, 27 (3), 2005.

Digital Library

[29]

Marius Nita, Dan Grossman, and Craig Chambers. A theory of platform-dependent low-level software (extended version). 2007. Available at http://www.cs.washington.edu/homes/marius/papers/tpd/.

[30]

Michael Norrish. C formalised in HOL. PhD thesis, University of Cambridge, 1998.

[31]

Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning. A type theory for memory allocation and data layout. In 30th ACM Symposium on Principles of Programming Languages, 2003.

Digital Library

[32]

Norman Ramsey, Simon~Peyton Jones, and Christian Lindig. The C-language specification version 2.0, 2005. http://www.cminusminus.org/extern/man2.pdf.

[33]

Micahel Siff, Satish Chandra, Thomas Ball, Krishna Kunchithapadam, and Thomas Reps. Coping with type casts in C. In 7th European Software Engineering Conference 7th ACM Symposium on the Foundations of Software Engineering, 1999.

Digital Library

[34]

Robert P. Wilson and Monica S. Lam. Efficient context-sensitive pointer analysis for C programs. In ACM Conference on Programming Language Design and Implementation, 1995.

Digital Library

Cited By

Krebbers R(2013)Aliasing Restrictions of C11 Formalized in CoqCertified Programs and Proofs10.1007/978-3-319-03545-1_4(50-65)Online publication date: 2013
https://doi.org/10.1007/978-3-319-03545-1_4
Greenberg MBlatt A(2019)Executable formal semantics for the POSIX shellProceedings of the ACM on Programming Languages10.1145/33711114:POPL(1-30)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371111
Bijo SJohnsen EPun KTapia Tarifa S(2017)A Formal Model of Parallel Execution on Multicore Architectures with Multilevel CachesFormal Aspects of Component Software10.1007/978-3-319-68034-7_4(58-77)Online publication date: 14-Sep-2017
https://doi.org/10.1007/978-3-319-68034-7_4
Show More Cited By

Recommendations

A theory of platform-dependent low-level software
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

The C language definition leaves the sizes and layouts of types partially unspecified. When a C program makes assumptions about type layout, its semantics is defined only on platforms (C compilers and the underlying hardware) on which those assumptions ...
Bypassing portability pitfalls of high-level low-level programming
VMIL '12: Proceedings of the sixth ACM workshop on Virtual machines and intermediate languages

Program portability is an important software engineering consideration. However, when high-level languages are extended to effectively implement system projects for software engineering gain and safety, portability is compromised--high-level code for ...
Blame for all
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Several programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLT Scheme), Perl 6, and C# 4.0 and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 43, Issue 1

POPL '08

January 2008

420 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1328897

Issue’s Table of Contents

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2008
448 pages
ISBN:9781595936899
DOI:10.1145/1328438
General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

Copyright © 2008 ACM.

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Published in SIGPLAN Volume 43, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
466
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Krebbers R(2013)Aliasing Restrictions of C11 Formalized in CoqCertified Programs and Proofs10.1007/978-3-319-03545-1_4(50-65)Online publication date: 2013
https://doi.org/10.1007/978-3-319-03545-1_4
Greenberg MBlatt A(2019)Executable formal semantics for the POSIX shellProceedings of the ACM on Programming Languages10.1145/33711114:POPL(1-30)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371111
Bijo SJohnsen EPun KTapia Tarifa S(2017)A Formal Model of Parallel Execution on Multicore Architectures with Multilevel CachesFormal Aspects of Component Software10.1007/978-3-319-68034-7_4(58-77)Online publication date: 14-Sep-2017
https://doi.org/10.1007/978-3-319-68034-7_4
Affeldt RMarti NMight MVan Horn DGiacobazzi RAbel ASheard T(2013)Towards formal verification of TLS network packet processing written in CProceedings of the 7th workshop on Programming languages meets program verification10.1145/2428116.2428124(35-46)Online publication date: 22-Jan-2013
https://dl.acm.org/doi/10.1145/2428116.2428124
Ellison CRosu GField JHicks M(2012)An executable formal semantics of C with applicationsProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2103656.2103719(533-544)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103656.2103719
Zhao JNagarakatte SMartin MZdancewic SField JHicks M(2012)Formalizing the LLVM intermediate representation for verified program transformationsProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2103656.2103709(427-440)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103656.2103709
Ellison CRosu G(2012)An executable formal semantics of C with applicationsACM SIGPLAN Notices10.1145/2103621.210371947:1(533-544)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103621.2103719
Zhao JNagarakatte SMartin MZdancewic S(2012)Formalizing the LLVM intermediate representation for verified program transformationsACM SIGPLAN Notices10.1145/2103621.210370947:1(427-440)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103621.2103709
Balakrishnan GReps T(2010)WYSINWYXACM Transactions on Programming Languages and Systems10.1145/1749608.174961232:6(1-84)Online publication date: 13-Aug-2010
https://dl.acm.org/doi/10.1145/1749608.1749612
Nita MGrossman D(2008)Automatic transformation of bit-level C code to support multiple equivalent data layoutsProceedings of the Joint European Conferences on Theory and Practice of Software 17th international conference on Compiler construction10.5555/1788374.1788382(85-99)Online publication date: 29-Mar-2008
https://dl.acm.org/doi/10.5555/1788374.1788382
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents