Flow-sensitive type qualifiers

Jeffrey S. Foster, Tachio Terauchi, Alex Aiken

Research output: Chapter in Book/Report/Conference proceedingConference contribution

240 Citations (Scopus)

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 languageEnglish
Title of host publicationProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Pages1-12
Number of pages12
Publication statusPublished - 2002
Externally publishedYes
EventProceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02) - Berlin, Germany
Duration: 2002 Jun 172002 Jun 19

Other

OtherProceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02)
CountryGermany
CityBerlin
Period02/6/1702/6/19

Fingerprint

Linux

Keywords

  • Alias analysis
  • Constraints
  • Effect inference
  • Flow-sensitivity
  • Linux kernel
  • Locking
  • Restrict
  • Type qualifiers
  • Types

ASJC Scopus subject areas

  • Software

Cite this

Foster, J. S., Terauchi, T., & Aiken, A. (2002). Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (pp. 1-12)

Flow-sensitive type qualifiers. / Foster, Jeffrey S.; Terauchi, Tachio; Aiken, Alex.

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2002. p. 1-12.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Foster, JS, Terauchi, T & Aiken, A 2002, Flow-sensitive type qualifiers. in Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). pp. 1-12, Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02), Berlin, Germany, 02/6/17.
Foster JS, Terauchi T, Aiken A. Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2002. p. 1-12
Foster, Jeffrey S. ; Terauchi, Tachio ; Aiken, Alex. / Flow-sensitive type qualifiers. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2002. pp. 1-12
@inproceedings{214692a9879c4855be445854378e42bb,
title = "Flow-sensitive type qualifiers",
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.",
keywords = "Alias analysis, Constraints, Effect inference, Flow-sensitivity, Linux kernel, Locking, Restrict, Type qualifiers, Types",
author = "Foster, {Jeffrey S.} and Tachio Terauchi and Alex Aiken",
year = "2002",
language = "English",
pages = "1--12",
booktitle = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",

}

TY - GEN

T1 - Flow-sensitive type qualifiers

AU - Foster, Jeffrey S.

AU - Terauchi, Tachio

AU - Aiken, Alex

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

KW - Alias analysis

KW - Constraints

KW - Effect inference

KW - Flow-sensitivity

KW - Linux kernel

KW - Locking

KW - Restrict

KW - Type qualifiers

KW - Types

UR - http://www.scopus.com/inward/record.url?scp=0036036247&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0036036247&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0036036247

SP - 1

EP - 12

BT - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

ER -