Flow-Sensitive Type Qualifiers
Jeffrey S. Foster, Tachio Terauchi and Alex Aiken
EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-01-1162
November 2001
http://www.eecs.berkeley.edu/Pubs/TechRpts/2001/CSD-01-1162.pdf
We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled flow-sensitively -- the underlying standard types are unchanged, which allows us to obtain an efficient constraint-based inference algorithm that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates. We demonstrate the usefulness of flow-sensitive type qualifiers by finding a number of new locking bugs in the Linux kernel.
BibTeX citation:
@techreport{Foster:CSD-01-1162,
Author = {Foster, Jeffrey S. and Terauchi, Tachio and Aiken, Alex},
Title = {Flow-Sensitive Type Qualifiers},
Institution = {EECS Department, University of California, Berkeley},
Year = {2001},
Month = {Nov},
URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2001/5718.html},
Number = {UCB/CSD-01-1162},
Abstract = {We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled flow-sensitively -- the underlying standard types are unchanged, which allows us to obtain an efficient constraint-based inference algorithm that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates. We demonstrate the usefulness of flow-sensitive type qualifiers by finding a number of new locking bugs in the Linux kernel.}
}
EndNote citation:
%0 Report %A Foster, Jeffrey S. %A Terauchi, Tachio %A Aiken, Alex %T Flow-Sensitive Type Qualifiers %I EECS Department, University of California, Berkeley %D 2001 %@ UCB/CSD-01-1162 %U http://www.eecs.berkeley.edu/Pubs/TechRpts/2001/5718.html %F Foster:CSD-01-1162