Submitted to the Dept. of Computer Science and Engineering, Seoul National University, Korea
Abstract
To improve the performance of C programs, mainstream compilers perform aggressive optimizations
that may change the behaviors of programs that use low-level features in unidiomatic
ways. Unfortunately, despite many years of research and industrial efforts, it has proven very
difficult to adequately balance the conflicting criteria for low-level features and compiler
optimizations in the design of the C programming language. On the one hand, C should support the
common usage patterns of the low-level features in systems programming. On the other hand, C
should also support the sophisticated and yet effective optimizations performed by mainstream
compilers. None of the existing proposals for C semantics, however, sufficiently support
low-level features and compiler optimizations at the same time.
In this dissertation, we resolve the conflict between some of the low-level features crucially
used in systems programming and major compiler optimizations. Specifically, we develop the first
formal semantics of relaxed-memory concurrency, separate compilation, and cast between integers
and pointers that (1) supports their common usage patterns and reasoning principles for
programmers, and (2) provably validates major compiler optimizations at the same time. To
establish confidence in our formal semantics, we have formalized most of our key results in the
Coq theorem prover, which automatically and rigorously checks the validity of the results.