Checking and inferring local non-aliasing

Alex Aiken, Jeffrey S. Foster, John Kodumal, Tachio Terauchi

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

45 Citations (Scopus)

Abstract

In prior work [15] we studied a language construct restrict that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other applications, programming with these constructs helps program analysis tools locally recover strong updates, which can improve the tracking of state in flow-sensitive analyses. In this paper we continue the study of restrict and introduce the construct confine. We present a type and effect system for checking the correctness of these annotations, and we develop efficient constraint-based algorithms implementing these type checking systems. To make it easier to use restrict and confine in practice, we show how to automatically infer such annotations without programmer assistance. In experiments on locking in 589 Linux device drivers, confine inference can automatically recover strong updates to eliminate 95% of the type errors resulting from weak updates.

Original languageEnglish
Title of host publicationProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Pages129-140
Number of pages12
Publication statusPublished - 2003
Externally publishedYes
EventACM SIGPLAN Conference on Programming Language Design and Implementation - San Diego, CA, United States
Duration: 2003 Jun 92003 Jun 11

Other

OtherACM SIGPLAN Conference on Programming Language Design and Implementation
CountryUnited States
CitySan Diego, CA
Period03/6/903/6/11

Fingerprint

Experiments
Linux

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this

Aiken, A., Foster, J. S., Kodumal, J., & Terauchi, T. (2003). Checking and inferring local non-aliasing. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (pp. 129-140)

Checking and inferring local non-aliasing. / Aiken, Alex; Foster, Jeffrey S.; Kodumal, John; Terauchi, Tachio.

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2003. p. 129-140.

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

Aiken, A, Foster, JS, Kodumal, J & Terauchi, T 2003, Checking and inferring local non-aliasing. in Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). pp. 129-140, ACM SIGPLAN Conference on Programming Language Design and Implementation, San Diego, CA, United States, 03/6/9.
Aiken A, Foster JS, Kodumal J, Terauchi T. Checking and inferring local non-aliasing. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2003. p. 129-140
Aiken, Alex ; Foster, Jeffrey S. ; Kodumal, John ; Terauchi, Tachio. / Checking and inferring local non-aliasing. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2003. pp. 129-140
@inproceedings{f6298e39c64e4736a9f4a07c1d11690c,
title = "Checking and inferring local non-aliasing",
abstract = "In prior work [15] we studied a language construct restrict that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other applications, programming with these constructs helps program analysis tools locally recover strong updates, which can improve the tracking of state in flow-sensitive analyses. In this paper we continue the study of restrict and introduce the construct confine. We present a type and effect system for checking the correctness of these annotations, and we develop efficient constraint-based algorithms implementing these type checking systems. To make it easier to use restrict and confine in practice, we show how to automatically infer such annotations without programmer assistance. In experiments on locking in 589 Linux device drivers, confine inference can automatically recover strong updates to eliminate 95{\%} of the type errors resulting from weak updates.",
keywords = "Alias analysis, Confine, Constraints, Effect inference, Flow-sensitivity, Linux kernel, Locking, Restrict, Type qualifiers, Types",
author = "Alex Aiken and Foster, {Jeffrey S.} and John Kodumal and Tachio Terauchi",
year = "2003",
language = "English",
pages = "129--140",
booktitle = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",

}

TY - GEN

T1 - Checking and inferring local non-aliasing

AU - Aiken, Alex

AU - Foster, Jeffrey S.

AU - Kodumal, John

AU - Terauchi, Tachio

PY - 2003

Y1 - 2003

N2 - In prior work [15] we studied a language construct restrict that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other applications, programming with these constructs helps program analysis tools locally recover strong updates, which can improve the tracking of state in flow-sensitive analyses. In this paper we continue the study of restrict and introduce the construct confine. We present a type and effect system for checking the correctness of these annotations, and we develop efficient constraint-based algorithms implementing these type checking systems. To make it easier to use restrict and confine in practice, we show how to automatically infer such annotations without programmer assistance. In experiments on locking in 589 Linux device drivers, confine inference can automatically recover strong updates to eliminate 95% of the type errors resulting from weak updates.

AB - In prior work [15] we studied a language construct restrict that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other applications, programming with these constructs helps program analysis tools locally recover strong updates, which can improve the tracking of state in flow-sensitive analyses. In this paper we continue the study of restrict and introduce the construct confine. We present a type and effect system for checking the correctness of these annotations, and we develop efficient constraint-based algorithms implementing these type checking systems. To make it easier to use restrict and confine in practice, we show how to automatically infer such annotations without programmer assistance. In experiments on locking in 589 Linux device drivers, confine inference can automatically recover strong updates to eliminate 95% of the type errors resulting from weak updates.

KW - Alias analysis

KW - Confine

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=0038716509&partnerID=8YFLogxK

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

M3 - Conference contribution

SP - 129

EP - 140

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

ER -