Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Thu 3 Nov 2016 14:20 - 14:45 at Matterhorn 2 - Principles, Across the Compilation Stack Chair(s): Adam Chlipala

Beneath the surface, software usually depends on complex linker behaviour to work as intended. Even linking hello_world.c is surprisingly involved, and systems software such as libc and operating system kernels rely on a host of linker features. But linking is poorly understood by working programmers and has largely been neglected by language researchers.

In this paper we survey the many use-cases that linkers support and the poorly specified linker-speak by which they are controlled: metadata in object files, command-line options, and linker-script language. We provide the first validated formalisation of a realistic executable and linkable format (ELF), and capture aspects of the Application Binary Interfaces for four mainstream platforms (AArch64, AMD64, Power64, and IA32). Using these, we develop an executable specification of static linking, covering (among other things) enough to link small C programs (we use the example of bzip2) into a correctly running executable. We provide our specification in Lem and Isabelle/HOL forms. This is the first formal specification of mainstream linking. We have used the Isabelle/HOL version to prove a sample correctness property for one case of AMD64 ABI relocation, demonstrating that the specification supports formal proof, and as a first step towards the much more ambitious goal of verified linking.

Our work should enable several novel strands of research, including linker-aware verified compilation and program analysis, and better languages for controlling linking.

Thu 3 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:10
Principles, Across the Compilation StackOOPSLA at Matterhorn 2
Chair(s): Adam Chlipala MIT CSAIL
13:30
25m
Talk
Semantic Subtyping for Imperative Object-Oriented LanguagesAEC
OOPSLA
Davide Ancona University of Genova, Andrea Corradi
DOI
13:55
25m
Talk
Parsing with First-Class DerivativesAEC
OOPSLA
Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Tillmann Rendel University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
DOI
14:20
25m
Talk
The Missing Link: Explaining ELF Static Linking, SemanticallyAEC
OOPSLA
Stephen Kell University of Cambridge, Dominic P. Mulligan University of Cambridge, Peter Sewell University of Cambridge
DOI
14:45
25m
Talk
Type Soundness for Dependent Object Types (DOT)AEC
OOPSLA
Tiark Rompf Purdue University, USA, Nada Amin EPFL
DOI Pre-print