Checking Programmer-Specified Non-Aliasing

Jeffrey S. Foster and Alex Aiken

EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-01-1160
October 2001

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2001/CSD-01-1160.pdf

We study the new ANSI C type qualifier restrict, which allows programmers to specify pointers that are not aliased to other pointers. The main contribution of this paper is a formal semantics for restrict and a type and effect system for checking that restrict-annotated programs are correct with respect to our semantics. We give an efficient inference algorithm for our type system and describe natural extensions of our type system to include subtyping, parametric polymorphism, and affects clauses that capture the effects of calling a function. We also discuss ways in which our type system differs from the ANSI C standard.


BibTeX citation:

@techreport{Foster:CSD-01-1160,
    Author = {Foster, Jeffrey S. and Aiken, Alex},
    Title = {Checking Programmer-Specified Non-Aliasing},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2001},
    Month = {Oct},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2001/5762.html},
    Number = {UCB/CSD-01-1160},
    Abstract = {We study the new ANSI C type qualifier restrict, which allows programmers to specify pointers that are not aliased to other pointers. The main contribution of this paper is a formal semantics for restrict and a type and effect system for checking that restrict-annotated programs are correct with respect to our semantics. We give an efficient inference algorithm for our type system and describe natural extensions of our type system to include subtyping, parametric polymorphism, and affects clauses that capture the effects of calling a function.  We also discuss ways in which our type system differs from the ANSI C standard.}
}

EndNote citation:

%0 Report
%A Foster, Jeffrey S.
%A Aiken, Alex
%T Checking Programmer-Specified Non-Aliasing
%I EECS Department, University of California, Berkeley
%D 2001
%@ UCB/CSD-01-1160
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2001/5762.html
%F Foster:CSD-01-1160