Into the depths of C: elaborating the de facto standards | ACM SIGPLAN Notices

skip to main content

ACM is now Open Access

×

As part of the Digital Library's transition to Open Access, new features for researchers are available in the Premium Edition. Click here to learn more.
You are currently in the Basic Edition. Features requiring a subscription appear in grey.

Sign In
Upgrade

Sign in

Register

Advanced SearchJournalsMagazinesProceedingsBooksSIGsConferencesInstitutionsPeopleMore

SearchSearch

Search ACM Digital LibrarySearchSearch
Advanced Search (Premium feature)Advanced Search

ACM SIGPLAN NoticesNewsletter HomeLatest Issue

ArchiveAuthorsAffiliationsAward WinnersMore

Export CitationsSelect Citation formatBibTeXEndNoteACM RefPlease download or close your previous search result export first before starting a new bulk export.Preview is not available.By clicking download,a status dialog will open to start the export process. The process may takea few minutes but once it finishes a file will be downloadable from your browser. You may continue to browse the DL while the export process is in progress.Download citationCopy citation
Several features on this page require Premium Access.Learn moreSign in

HomeSIGsACM SIGPLAN NoticesVol. 51, No. 6Into the depths of C: elaborating the de facto standards
You are using the Basic Edition. Features requiring a subscription appear in grey.Sign in to your subscription or learn moreUpgrade
articleFree access
Share on
Into the depths of C: elaborating the de facto standardsAuthors: Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, + 3, David Chisnall, Robert N. M. Watson, Peter Sewell (Less)Authors Info & ClaimsACM SIGPLAN Notices, Volume 51, Issue 6Pages 1 - 15https://doi.org/10.1145/2980983.2908081Published: 02 June 2016 Publication History
Additional metrics (Premium feature)84citation5,874Downloads

New Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsAdd a Citation AlertTo add a citation alert, please log in to your account
PDF/eReaderContentsACM SIGPLAN NoticesVolume 51, Issue 6NEXT ARTICLELiving on the edge: rapid-toggling probes with cross-modification on x86NextAbstractReferences

Information & ContributorsBibliometrics & CitationsReading OptionsReferencesFiguresTablesMediaShareAbstractC remains central to our computing infrastructure. It is notionally defined by ISO standards, but in reality the properties of C assumed by systems code and those implemented by compilers have diverged, both from the ISO standards and from each other, and none of these are clearly understood. We make two contributions to help improve this error-prone situation. First, we describe an in-depth analysis of the design space for the semantics of pointers and memory in C as it is used in practice. We articulate many specific questions, build a suite of semantic test cases, gather experimental data from multiple implementations, and survey what C experts believe about the de facto standards. We identify questions where there is a consensus (either following ISO or differing) and where there are conflicts. We apply all this to an experimental C implemented above capability hardware. Second, we describe a formal model, Cerberus, for large parts of C. Cerberus is parameterised on its memory model; it is linkable either with a candidate de facto memory object model, under construction, or with an operational C11 concurrency model; it is defined by elaboration to a much simpler Core language for accessibility, and it is executable as a test oracle on small examples. This should provide a solid basis for discussion of what mainstream C is now: what programmers and analysis tools can assume and what compilers aim to implement. Ultimately we hope it will be a step towards clear, consistent, and accepted semantics for the various use-cases of C.Formats availableYou can view the full content in the following formats:PDF/eReaderReferences[1]Programming Languages — C. 2011.Google Scholar[2]ISO/IEC 9899:2011. A non-final but recent version is available at www.open-std.org/jtc1/sc22/wg14/docs/n1539.pdf.Google Scholar[3]ANSI. Programming Languages – C: ANSI X3.159-1989. 1989.Google Scholar[4]M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In Proc. POPL, 2011.Digital LibraryGoogle Scholar[5]P. Becker, editor. Programming Languages — C++. 2011. ISO/IEC 14882:2011.Google Scholar[6]A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM, 53(2), 2010.Digital LibraryGoogle Scholar[7]F. Besson, S. Blazy, and P. Wilke. A precise and abstract memory model for C using symbolic values. In APLAS, 2014.CrossrefGoogle Scholar[8]F. Besson, S. Blazy, and P. Wilke. A concrete memory model for CompCert. In Proc. ITP, 2015.CrossrefGoogle Scholar[9]H.-J. Boehm and S. Adve. Foundations of the C++ concurrency memory model. In Proc. PLDI, 2008.Digital LibraryGoogle Scholar[10]G. Canet, P. Cuoq, and B. Monate. A value analysis for C programs. In Proc. 9th IEEE Intl. Working Conference on Source Code Analysis and Manipulation, SCAM ’09, 2009.Digital LibraryGoogle Scholar[11]D. Chisnall, J. Matthiesen, K. Memarian, K. Nienhuis, P., and R.N.M. Watson. C memory object and value semantics: the space of de facto and ISO standards, 2016. http://www.cl.cam.ac.uk/~pes20/cerberus/.Google Scholar[12]D. Chisnall, C. Rothwell, R. N. M. Watson, J. Woodruff, M. Vadera, S. W. Moore, M. Roe, B. Davis, and P. G. Neumann. Beyond the PDP-11: Architectural support for a memory-safe C abstract machine. In Proc. ASPLOS, 2015.Digital LibraryGoogle Scholar[13]E. Cohen, M. Moskal, S. Tobies, and W. Schulte. A precise yet efficient memory model for C. Electron. Notes Theor. Comput. Sci. (SSV 2009), 254:85–103, October 2009.Digital LibraryGoogle Scholar[14]J. Cook and S. Subramanian. A formal semantics for C in Nqthm. Technical Report 517D, Trusted Information Systems, October, 1994.Google Scholar[15]J. Criswell, N. Geoffray, and V. Adve. Memory safety for low-level software/hardware interactions. In Proceedings of the Eighteenth Usenix Security Symposium, August 2009.Digital LibraryGoogle Scholar[16]J. Devietti, C. Blundell, M. M. K. Martin, and S. Zdancewic. Hardbound: Architectural support for spatial safety of the C programming language. In Proc. ASPLOS, 2008.Digital LibraryGoogle Scholar[17]C. Ellison and G. Ro¸su. An executable formal semantics of C with applications. In Proc. POPL, 2012.Digital LibraryGoogle Scholar[18]Y. Gurevich and J. K. Huggins. The semantics of the C programming language. In Proc. CSL ’92, 1993.Digital LibraryGoogle Scholar[19]C. Hathhorn, C. Ellison, and G. Rosu. Defining the undefinedness of C. In Proc. PLDI, 2015.Digital LibraryGoogle Scholar[20]Charles McEwen Ellison III. A Formal Semantics of C with Applications. PhD thesis, University of Illinois at Urbana-Champaign, 2012.Google Scholar[21]Runtime Verification Inc. Rv-match v0.1. https://runtimeverification.com/match/download/, 2016. Downloaded 2016-03-11.Google Scholar[22]Intel Plc. Introduction to Intel memory protection extensions, July 2013.Google Scholar[23]T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In Proc. USENIX ATC, 2002.Digital LibraryGoogle Scholar[24]J. Kang, C.-K. Hur, W. Mansky, D. Garbuzov, S. Zdancewic, and V. Vafeiadis. A formal C memory model supporting integer-pointer casts. In Proc. PLDI, 2015.Digital LibraryGoogle Scholar[25]B. W. Kernighan and D. M. Ritchie. The C Programming Language (ANSI C). Prentice Hall, 2nd edition, 1988.Digital LibraryGoogle Scholar[26]R. Krebbers. Aliasing restrictions of C11 formalized in Coq. In Proc. CPP, LNCS 8307, 2013.Digital LibraryGoogle Scholar[27]R. Krebbers. An operational and axiomatic semantics for nondeterminism and sequence points in C. In Proc. POPL, 2014.Digital LibraryGoogle Scholar[28]R. Krebbers. The C standard formalized in Coq. PhD thesis, Radboud University Nijmegen, December 2015.Google Scholar[29]R. Krebbers and F. Wiedijk. Separation logic for non-local control flow and block scope variables. In FoSSaCS, 2013.Digital LibraryGoogle Scholar[30]R. Krebbers and F. Wiedijk. A typed C11 semantics for interactive theorem proving. In Proc. CPP, 2015.Digital LibraryGoogle Scholar[31]X. Leroy, A. W. Appel, S. Blazy, and G. Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012.Google Scholar[32]X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41(1):1–31, 2008.Digital LibraryGoogle Scholar[33]K. Memarian, J. Matthiesen, K. Nienhuis, V. B. F. Gomes, J. Lingard, D. Chisnall, R. N. M. Watson, and P. Sewell. Cerberus, 2016.Google Scholar[34]www.cl.cam.ac.uk/~pes20/cerberus, www.repository.cam.ac.uk/handle/1810/255730.Google Scholar[35]D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell. Lem: reusable engineering of real-world semantics. In Proc. ICFP, 2014.Digital LibraryGoogle Scholar[36]S. Nagarakatte, J. Zhao, M. M.K. Martin, and S. Zdancewic. SoftBound: highly compatible and complete spatial memory safety for C. In Proc. PLDI, 2009.Digital LibraryGoogle Scholar[37]G. C. Necula, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy code. In Proc. POPL, 2002.Digital LibraryGoogle Scholar[38]N. Nethercote and J. Seward. Valgrind: A framework for heavyweight dynamic binary instrumentation. In PLDI, 2007.Digital LibraryGoogle Scholar[39]K. Nienhuis, K. Memarian, and P. Sewell. An operational semantics for C/C++11 concurrency, 2016. Draft available at www.cl.cam.ac.uk/~pes20/cerberus.Digital LibraryGoogle Scholar[40]M. Norrish. C formalised in HOL. Technical Report UCAMCL-TR-453, U. Cambridge, Computer Laboratory, 1998.Google Scholar[41]M. Norrish. Deterministic expressions in C. In ESOP, 1999.Digital LibraryGoogle Scholar[42]N. S Papaspyrou. A formal semantics for the C programming language. PhD thesis, National Technical University of Athens, 1998.Google Scholar[43]F. Pottier and Y. Régis-Gianas. Menhir. gallium.inria.fr/~fpottier/menhir/.Google Scholar[44]J. Regehr. blog.regehr.org/archives/721, 2012.Google Scholar[45]J. Regehr, April 2015. blog.regehr.org/archives/1234.Google Scholar[46]TrustInSoft. trust-in-soft.com/tis-interpreter, 2015.Google Scholar[47]H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic. In Proc. POPL, 2007.Digital LibraryGoogle Scholar[48]J. Ševˇcík, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell. CompCertTSO: A verified compiler for relaxedmemory concurrency. J. ACM, 60(3), June 2013.Digital LibraryGoogle Scholar[49]X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich, and M. F. Kaashoek. Undefined behavior: what happened to my code? In Proc. APSYS, 2012.Digital LibraryGoogle Scholar[50]X. Wang, N. Zeldovich, M. F. Kaashoek, and A. Solar-Lezama. Towards optimization-safe systems: Analyzing the impact of undefined behavior. In Proc. SOSP, 2013.Digital LibraryGoogle Scholar[51]R. N. M. Watson, P. G. Neumann, J. Woodruff, M. Roe, J. Anderson, D. Chisnall, B. Davis, A. Joannou, B. Laurie, S. W. Moore, S. J. Murdoch, and R. Norton. Capability hardware enhanced RISC instructions: CHERI instruction-set architecture. Technical Report UCAM-CL-TR-864, University of Cambridge, Computer Laboratory, November 2015.Google Scholar[52]R. N. M. Watson, J. Woodruff, P. G. Neumann, S. W. Moore, J. Anderson, D. Chisnall, N. H. Dave, B. Davis, K. Gudka, B. Laurie, S. J. Murdoch, R. Norton, M. Roe, S. Son, and M. Vadera. CHERI: A hybrid capability-system architecture for scalable software compartmentalization. In IEEE Symposium on Security and Privacy, SP, 2015.Digital LibraryGoogle Scholar[53]WG14. Defect report summary for ISO/IEC 9899:1999.Google Scholar[54]WG14. ISO/IEC 9899:2011.Google Scholar[55]WG14. Defect report 260, September 2004.Google Scholar[56]www.open-std.org/jtc1/sc22/wg14/www/docs/dr_260.htm.Google Scholar[57]J. Woodruff, R. N. M. Watson, D. Chisnall, S. W. Moore, J. Anderson, B. Davis, B. Laurie, P. G. Neumann, R. Norton, and M. Roe. The CHERI capability model: revisiting RISC in an age of risk. In ISCA, 2014.Digital LibraryGoogle Scholar[58]X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In Proc. PLDI, 2011.Digital LibraryGoogle Scholar[59]J. Zhao, S. Nagarakatte, M. M.K. Martin, and S. Zdancewic. Formalizing the LLVM intermediate representation for verified program transformations. In Proc. POPL, 2012.Digital LibraryGoogle Scholar

Cited ByView allHansen RLarsen AAskarov A(2026)The Downgrading Semantics of Memory SafetyProceedings of the ACM on Programming Languages10.1145/380826010:PLDI(328-355)Online publication date: 8-Jun-2026https://dl.acm.org/doi/10.1145/3808260Grisafi MRamponi CAmmar MVlasceanu SCrispo B(2026)TAGShield: Persistent Tagging for Robust Stack Memory Error ProtectionProceedings of the ACM Asia Conference on Computer and Communications Security10.1145/3779208.3785279(986-999)Online publication date: 1-Jun-2026https://dl.acm.org/doi/10.1145/3779208.3785279Du KSharma ALi LMansky W(2026)A Formal Semantics of C with OpenMP ParallelismNASA Formal Methods10.1007/978-3-032-28079-4_20(436-455)Online publication date: 5-May-2026https://dl.acm.org/doi/10.1007/978-3-032-28079-4_20Show More Cited By

Index Terms
Index Terms (Premium feature)Into the depths of C: elaborating the de facto standardsTheory of computationSemantics and reasoningProgram semantics

Recommendations
Recommendations (Premium feature)Into the depths of C: elaborating the de facto standardsPLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
C remains central to our computing infrastructure. It is notionally defined by ISO
standards, but in reality the properties of C assumed by systems code and those implemented
by compilers have diverged, both from the ISO standards and from each other, ...
Read MoreInfluences on standards adoption in de facto standardizationSpecial issue on New Theories and Methods for Technology Adoption Research
In the IT industry, de facto standards emerge from standards competition as firms
offer incompatible technologies, and user choices determine the outcome of the competition.
The standards literature suggests that strong network effects create a bias ...
Read MoreANSI's role in standards development
ANSI is the American National Standards Institute, the US national coordinating institute
for voluntary standards. Typically, you will see ANSI in a standard's name followed
by some letters and numbers such as X3.181-1980. These characters represent the ...
Read More

Comments
Comments (Premium feature)Please enable JavaScript to view thecomments powered by Disqus.

Information & ContributorsInformationPublished In
ACM SIGPLAN Notices  Volume 51, Issue 6PLDI '16June 2016726 pagesISSN:0362-1340EISSN:1558-1160DOI:10.1145/2980983Editor: Andy GillIssue’s Table of ContentsPLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationJune 2016726 pagesISBN:9781450342612DOI:10.1145/2908080General Chair: Chandra Krintz,Program Chair: Emery Berger
Copyright © 2016 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]PublisherAssociation for Computing MachineryNew York, NY, United StatesPublication HistoryPublished: 02 June 2016Published in SIGPLAN Volume 51, Issue 6Check for updatesAuthor TagCQualifiersArticleFunding SourcesAFRLEngineering and Physical Sciences Research CouncilDefense Advanced Research Projects AgencyContributors

Other MetricsView Article MetricsBibliometrics & CitationsBibliometrics

Article Metrics

84Total CitationsView Citations5,874Total DownloadsDownloads (Last 12 months)Advanced metrics (Premium feature)...Downloads (Last 6 weeks) Advanced metrics (Premium feature)...Reflects downloads up to 05 Sep 2026

Other MetricsView Author MetricsCitations
Cited ByView allHansen RLarsen AAskarov A(2026)The Downgrading Semantics of Memory SafetyProceedings of the ACM on Programming Languages10.1145/380826010:PLDI(328-355)Online publication date: 8-Jun-2026https://dl.acm.org/doi/10.1145/3808260Grisafi MRamponi CAmmar MVlasceanu SCrispo B(2026)TAGShield: Persistent Tagging for Robust Stack Memory Error ProtectionProceedings of the ACM Asia Conference on Computer and Communications Security10.1145/3779208.3785279(986-999)Online publication date: 1-Jun-2026https://dl.acm.org/doi/10.1145/3779208.3785279Du KSharma ALi LMansky W(2026)A Formal Semantics of C with OpenMP ParallelismNASA Formal Methods10.1007/978-3-032-28079-4_20(436-455)Online publication date: 5-May-2026https://dl.acm.org/doi/10.1007/978-3-032-28079-4_20Delaët ABlazy SMerigoux D(2025)Abstract machines and small-step semantics: a winning ticket for proof automation?Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming10.1145/3756907.3756926(1-14)Online publication date: 10-Sep-2025https://dl.acm.org/doi/10.1145/3756907.3756926Lawall JNishimura KLozi J(2024)Should We Balance? Towards Formal Verification of the Linux Kernel SchedulerStatic Analysis10.1007/978-3-031-74776-2_8(194-215)Online publication date: 20-Oct-2024https://dl.acm.org/doi/10.1007/978-3-031-74776-2_8Li LLiu YPostol DLampropoulos LVan Horn DHicks M(2023)A formal model of Checked C1Journal of Computer Security10.3233/JCS-23004031:5(581-614)Online publication date: 13-Oct-2023https://doi.org/10.3233/JCS-230040Anderson SNaaktgeboren ATolmach A(2023)Flexible Runtime Security Enforcement with Tagged CRuntime Verification10.1007/978-3-031-44267-4_12(231-250)Online publication date: 3-Oct-2023https://dl.acm.org/doi/10.1007/978-3-031-44267-4_12Michael AGollamudi ABosamiya JJohnson EDenlinger ADisselkoen CWatt CParno BPatrignani MVassena MStefan D(2023)MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe CodeProceedings of the ACM on Programming Languages10.1145/35712087:POPL(425-454)Online publication date: 11-Jan-2023https://dl.acm.org/doi/10.1145/3571208Colvin R(2022)Separation of Concerning Things: A Simpler Basis for Defining and Programming with the C/C++ Memory ModelFormal Methods and Software Engineering10.1007/978-3-031-17244-1_5(71-89)Online publication date: 24-Oct-2022https://dl.acm.org/doi/10.1007/978-3-031-17244-1_5Li LLiu YPostol DLampropoulos LVan Horn DHicks M(2022)A Formal Model of Checked C2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919657(49-63)Online publication date: Aug-2022https://doi.org/10.1109/CSF54842.2022.9919657Show More Cited By
ShareShareShare this Publication linkCopy LinkCopied!Copying failed.Share on social mediaXLinkedInRedditFacebookThreadsemail

AffiliationsKayvan MemarianUniversity of Cambridge, UKView ProfileJustus MatthiesenUniversity of Cambridge, UKView ProfileJames LingardUniversity of Cambridge, UKView ProfileKyndylan NienhuisUniversity of Cambridge, UKView ProfileDavid ChisnallUniversity of Cambridge, UKView ProfileRobert N. M. WatsonUniversity of Cambridge, UKView ProfilePeter SewellUniversity of Cambridge, UKView ProfileDownload PDF

View Issue’s Table of Contents

Footer

Categories

Journals
Magazines
Books
Proceedings
SIGs
Conferences
Collections
People

About

About ACM Digital Library
ACM Digital Library Board
Author Guidelines
All Holdings within the ACM Digital Library
ACM Computing Classification System
Accessibility Statement

Join

Join ACM
Join SIGs
Subscribe to Publications
Institutions and Libraries

Connect

Contact us via email
ACM on Facebook
ACM DL on X
ACM on Linkedin

Send Feedback
Submit a Bug Report

The ACM Digital Library is published by the Association for Computing Machinery. Copyright © 2026 ACM, Inc.

Terms of Usage
Privacy Policy
Code of Ethics

Your Search Results Download Request We are preparing your search results for download ...We will inform you here when the file is ready.Download now!Your Search Results Download RequestYour file of search results citations is now ready.Download now!Your Search Results Download RequestYour search export query has expired. Please try again.

C remains foundational to modern computing infrastructure, yet the actual properties of C assumed by systems code and those implemented by compilers have diverged not only from formal ISO standards but also from one another, leading to an ambiguous and error-prone situation regarding its semantics. The authors address this divergence by making two primary contributions aimed at clarifying these realities. First, they provide an in-depth analysis of the design space for the semantics of pointers and memory as used in practice within C. This involves articulating specific questions, developing a suite of semantic test cases, gathering experimental data from multiple implementations, and surveying the opinions of C experts regarding de facto standards, thereby identifying areas of consensus, points of conflict, and discrepancies between formal definitions and practical implementation. This analysis is applied to an experimental C implementation running on capability hardware. Second, the authors introduce Cerberus, a formal model designed for large portions of C. Cerberus is parameterized by its underlying memory model, allowing it to be linked either with a candidate de facto memory object model or with operational concurrency models such as C11. It is defined through elaboration onto a simpler Core language for accessibility and is executable as a test oracle on small examples. The ultimate goal of these efforts is to establish a solid foundation for discussions concerning what programmers and analysis tools can consistently assume about mainstream C, and what compilers are tasked with implementing, ultimately seeking clear, consistent, and accepted semantics across various use cases of C.