Checking and inferring local non-aliasing

Abstract

In prior work [15] we studied a language construct <tt>restrict</tt> 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 <tt>restrict</tt> and introduce the construct <tt>confine</tt>. 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 <tt>restrict</tt> and <tt>confine</tt> in practice, we show how to automatically infer such annotations without programmer assistance. In experiments on locking in 589 Linux device drivers, <tt>confine</tt> inference can automatically recover strong updates to eliminate 95% of the type errors resulting from weak updates.