Safe Programming at the C Level of Abstraction
Abstract
Memory safety and type safety are invaluable features for building
robust software. However, most safe programming languages are at a
high level of abstraction; programmers have little control over
data representation and memory management. This control is one reason
C remains the de facto standard for writing systems software or
extending legacy systems already written in C. The Cyclone language
aims to bring safety to C-style programming without sacrificing the
programmer control necessary for low-level software. A combination of
advanced compile-time techniques, run-time checks, and modern language
features helps achieve this goal.
This dissertation focuses on the advanced compile-time techniques. A
type system with quantified types and effects prevents
incorrect type casts, dangling-pointer dereferences, and data races.
An intraprocedural flow analysis prevents dereferencing NULL
pointers and uninitialized memory, and extensions to it can prevent
array-bounds violations and misused unions. Formal abstract machines
and rigorous proofs demonstrate that these compile-time techniques are
sound: The safety violations they address become impossible.
A less formal evaluation establishes two other design goals of equal
importance. First, the language remains expressive. Although it
rejects some safe programs, it permits many C idioms regarding generic
code, manual memory management, lock-based synchronization,
NULL-pointer checking, and data initialization. Second, the language
represents a unified approach. A small collection of techniques
addresses a range of problems, indicating that the problems are more
alike than they originally seem.
dvi pdf ps dvi.gz ps.gz