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.
| Original language | English |
|---|---|
| Pages | 1-12 |
| Number of pages | 12 |
| DOIs | |
| Publication status | Published - 2002 |
| Externally published | Yes |
| Event | Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02) - Berlin, Germany Duration: 2002 Jun 17 → 2002 Jun 19 |
Other
| Other | Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02) |
|---|---|
| Country/Territory | Germany |
| City | Berlin |
| Period | 02/6/17 → 02/6/19 |
Keywords
- Alias analysis
- Constraints
- Effect inference
- Flow-sensitivity
- Linux kernel
- Locking
- Restrict
- Type qualifiers
- Types
ASJC Scopus subject areas
- Software