Repository logo
 

Into the depths of C: Elaborating the de facto standards

Accepted version
Peer-reviewed

Repository DOI


Type

Conference Object

Change log

Authors

Matthiesen, J 
Lingard, J 
Nienhuis, K 
Chisnall, D 

Abstract

jats:pC 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.</jats:p>

Description

Keywords

C

Journal Title

ACM SIGPLAN Notices

Conference Name

37th annual ACM SIGPLAN conference on Programming Language Design and Implementation

Journal ISSN

1523-2867
1558-1160

Volume Title

Publisher

Association for Computing Machinery (ACM)
Sponsorship
Engineering and Physical Sciences Research Council (EP/K008528/1)
Engineering and Physical Sciences Research Council (EP/H005633/1)
We acknowledge funding from EPSRC grants EP/H005633 (Leadership Fellowship, Sewell) and EP/K008528 (REMS Programme Grant), and a Gates Cambridge Scholarship (Nienhuis). This work is also part of the CTSRD projects sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237.