Checking Programmer-Specified Non-Aliasing
Jeffrey S. Foster and Alex Aiken
EECS Department, University of California, Berkeley
Technical Report No. UCB/CSD-01-1160
, 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}, 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