Wed 15 Jun 2016 10:30 - 11:00 at Grand Ballroom Santa Ynez - Down to the Metal I Chair(s): Stephen McCamant

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, 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.

Wed 15 Jun

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Down to the Metal IResearch Papers at Grand Ballroom Santa Ynez
Chair(s): Stephen McCamant University of Minnesota
10:30
30m
Talk
Into the depths of C: elaborating the de facto standards
Research Papers
Kayvan Memarian University of Cambridge, Justus Matthiesen University of Cambridge, James Lingard University of Cambridge (when this work was done), Kyndylan Nienhuis University of Cambridge, David Chisnall University of Cambridge, Robert N. M. Watson University of Cambridge, Peter Sewell University of Cambridge
Link to publication Media Attached
11:00
30m
Talk
Living on the edge: Rapid-toggling probes with cross modification on x86
Research Papers
Buddhika Chamith , Bo Joel Svensson Indiana University, Luke Dalessandro Indiana University, Ryan R. Newton Indiana University
Pre-print Media Attached
11:30
30m
Talk
Polymorphic Type Inference for Machine Code
Research Papers
Matt Noonan GrammaTech, Inc, Alexey Loginov GrammaTech, Inc, David Cok GrammaTech, Inc
Pre-print Media Attached