Jeremy Paul Condit

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2007-117

September 19, 2007

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-117.pdf

The C language is the dominant language for writing systems software, but it permits large classes of programming errors that could be prevented with a more modern language. Unfortunately, it is impractical to simply rewrite all of our existing software; rather, we must focus on a transition path to a more reliable systems programming language. As the first step in an incremental transition to a new language, we must allow programmers to annotate higher-level idioms typically used by C programmers, such as bounded pointers and tagged unions.

This thesis presents Deputy, a dependent type framework that allows programmers to annotate existing C code with more refined types. In particular, dependent types allow programmers to relate multiple state elements, such as a pointer and its bounds, or a union and its tag. In doing so, we address several technical hurdles involved with dependent types. First, we address the issue of mutation in the presence of dependencies by using insights from axiomatic semantics. Second, we handle the problem of undecidability by using run-time checks where necessary. Third, we address usability challenges with a novel inference mechanism called automatic dependencies.

Once this framework is established, we show how it can be instantiated to support the dependent types required by modern systems code. In addition, we discuss several real-world applications of Deputy, including small and medium-size benchmarks as well as the Linux kernel itself. These benchmarks allow us to evaluate Deputy's annotation burden and performance in the context of real-world code.

Advisors: George Necula

---

BibTeX citation:

@phdthesis{Condit:EECS-2007-117,
    Author= {Condit, Jeremy Paul},
    Title= {Dependent Types for Safe Systems Software},
    School= {EECS Department, University of California, Berkeley},
    Year= {2007},
    Month= {Sep},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-117.html},
    Number= {UCB/EECS-2007-117},
    Abstract= {The C language is the dominant language for writing systems software, but it permits large classes of programming errors that could be prevented with a more modern language.  Unfortunately, it is impractical to simply rewrite all of our existing software; rather, we must focus on a transition path to a more reliable systems programming language.  As the first step in an incremental transition to a new language, we must allow programmers to annotate higher-level idioms typically used by C programmers, such as bounded pointers and tagged unions.

This thesis presents Deputy, a dependent type framework that allows programmers to annotate existing C code with more refined types.  In particular, dependent types allow programmers to relate multiple state elements, such as a pointer and its bounds, or a union and its tag.  In doing so, we address several technical hurdles involved with dependent types.  First, we address the issue of mutation in the presence of dependencies by using insights from axiomatic semantics.  Second, we handle the problem of undecidability by using run-time checks where necessary.  Third, we address usability challenges with a novel inference mechanism called automatic dependencies.

Once this framework is established, we show how it can be instantiated to support the dependent types required by modern systems code.  In addition, we discuss several real-world applications of Deputy, including small and medium-size benchmarks as well as the Linux kernel itself.  These benchmarks allow us to evaluate Deputy's annotation burden and performance in the context of real-world code.},
}

EndNote citation:

%0 Thesis
%A Condit, Jeremy Paul 
%T Dependent Types for Safe Systems Software
%I EECS Department, University of California, Berkeley
%D 2007
%8 September 19
%@ UCB/EECS-2007-117
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-117.html
%F Condit:EECS-2007-117