| |
Mainstream software interfaces describe types, sets of accessible
functions, fields, and the expected and returned types of such
operations. They lack any indication of requirements or effects on the
underlying state of the system. Since most programming environments
are stateful, important data and control invariants are not
specified. This lack of stateful specifications opens up these systems
to a myriad of reliability problems that manifest in possible runtime
failures. In these lectures we will examine how advanced type systems
based on forms of linear logic can capture many such stateful
invariants concisely and naturally. We will describe how such systems
can be integrated in novel programming language or existing language
extension and some experience with several systems we built in the
past .
| Improving Software Quality with Type Qualifiers |
Jeff Foster |
Software continues to increase in size and complexity, yet programmers
have few practical tools and techniques to ensure its quality and
reliability. In these lectures, we will explore a general technique
based on type qualifiers that allows
programmers to write annotations in their source code describing
additional program properties that should be maintained during
execution. Type qualifiers have a number of advantages as a mechanism
for specifying and checking properties of programs: They are a simple,
natural extension of the standard types present in typical programming
languages; they support efficient inference algorithms, so that
programmers need only write a few annotations and the rest are
inferred automatically; and the results of type qualifier inference
can be intuitively presented to the programmer to justify any errors
that are detected.
We will discuss theoretical foundations and practical implementation
issues for type qualifiers, including efficient inference algorithms
that scale to large programs such as the Linux kernel. We will also
discuss particular issues in adding type qualifiers to C. We will
discuss examples of qualifiers, such as ANSI C's
const , security-related qualifiers for
finding format-string vulnerabilities , and qualifiers to
support transparent proxies in Java . If
time permits, we will also discuss qualifiers for deadlock
detection in the Linux kernel.
Domain-specific languages can dramatically improve the reliability of
software by providing highly-tailored abstractions. Such abstractions
can significantly reduce code sizes, making maintenance easier. In
addition, tricky or extensive "boilerplate" code can be generated by
the compiler rather than hand-coded, making user-code more reliable.
(Presumably the compiler-writers know what they are doing, or at
least, the code can be debugged once and then reused by many!) An
additional benefit of domain-specific languages is that they provide
an opportunity for programming languages research to affect other
aspects of computer science in a much shorter time-frame than general
purpose languages can. This immediacy makes programming language work
obviously relevant to our colleagues, provides a wonderful platform
for experimenting with language technology, and poses new research
challenges.
This series of talks will describe two different domain-specific
languages that have been developed at AT&T. Each of these languages
endeavors to improve the reliability of software and have an immediate
impact on a user group. The first of these languages,
Hancock , facilitates writing programs to construct and
maintain "customer" profiles from high-volume transactional data
streams. Hancock programs have been used in production fraud and
marketing applications for several years to significant financial
effect. The second language, PADS , allows users to describe ad hoc
data declaratively, including physical layout information and semantic
constraints. The PADS compiler then generates a library and various
tools for parsing and manipulating the data. In the talks, we will
motivate the need for Hancock and PADS, describe and evaluate the
designs, discuss their use at AT&T, and point out possible areas for
future research.
|
|
