Sharing Analysis in the Pawns Compiler
Lee Naish




Pawns sharing  

L. Naish   
Lee Naish
Computing and Information Systems,

University of Melbourne, Melbourne 3010, Australia

dr.lee.naish@gmail.com,

 

Sharing analysis in the Pawns compiler
    Lee Naish
    
======================================








§ ABSTRACT 

Pawns is a programming language under development that supports algebraic
data types, polymorphism, higher order functions and “pure” declarative
programming.  It also supports impure imperative features including
destructive update of shared data structures via pointers, allowing
significantly increased efficiency for some operations.  A novelty of
Pawns is that all impure “effects” must be made obvious in the source
code and they can be safely encapsulated in pure
functions in a way that is checked by the compiler.  Execution of a pure
function can perform destructive updates on data structures that are local
to or eventually returned from the function without risking modification
of the data structures passed to the function.  This paper describes the
sharing analysis which allows impurity to be encapsulated.  Aspects of the
analysis are similar to other published work, but in addition it handles
explicit pointers and destructive update, higher order functions including
closures and pre- and post-conditions concerning sharing for functions.

Keywords: functional programming language, destructive update, mutability,
effects, algebraic data type, sharing analysis, aliasing analysis




§ INTRODUCTION



This paper describes the sharing analysis done by the compiler for Pawns
<cit.>, a programming language that is currently under development.
It is a slightly updated version of <cit.>, with a section
that briefly describes a new abstract domain used for the analysis,
implemented since the original publication.
Pawns supports both declarative and imperative styles of programming.
It supports algebraic data types, polymorphism, higher order programming
and “pure” declarative functions, allowing very high level reasoning
about code.  It also allows imperative code, where programmers can
consider the representation of data types, obtain pointers to the
arguments of data constructors and destructively update them.  Such code
requires the programmer to reason at a much lower level and consider
aliasing of pointers and sharing of data structures.  Low level “impure”
code can be encapsulated within a pure interface and the compiler checks
the purity.  This requires analysis of pointer aliasing and data structure
sharing, to distinguish data structures that are only visible to the
low level code (and are therefore safe to update) from data structures
that are passed in from the high level code (for which update would
violate purity).  The main aim of Pawns is to get the benefits of purity
for most code but still have the ability to write some key components
using an imperative style, which can significantly improve efficiency
(for example, a more than twenty-fold increase in the speed of inserting
an element into a binary search tree).

There are other functional programming languages, such as ML <cit.>,
Haskell <cit.> and Disciple <cit.>, that allow
destructive update of shared data structures but do not allow this
impurity to be encapsulated.  In these languages the ability to update
the data structure is connected to its type[Disciple uses
“region” information to augment types, with similar
consequences.].  For a data structure to be
built using destructive update its type must allow destructive update
and any code that uses the data structure can potentially update it
as well.  This prevents simple declarative analysis of the code and can
lead to a proliferation of different versions of a data structure, with
different parts being mutable. For example, there are four different
versions of lists, since both the list elements and the “spine” may
(or may not) be mutable, and sixteen different versions of lists of
pairs.  There is often an efficiency penalty as
well, with destructive update requiring an extra level of indirection
in the data structure (an explicit “reference” in the type with most
versions of ML and Haskell).  Pawns avoids this inefficiency and separates
mutability from type information, allowing a data structure to be mutable
in some contexts and considered “pure” in others.  The main cost from
the programmer perspective is the need to include extra annotations and
information in the source code.  This can also be considered a benefit,
as it provides useful documentation and error checking.  The main
implementation cost is additional analysis done by the compiler, which
is the focus of this paper.

The rest of this paper assumes some familiarity with
Haskell and is structured as follows.
Section <ref> gives a brief overview of the relevant
features of Pawns.  An early pass of the compiler translates Pawns
programs into a simpler “core” language; this is
described in Section <ref>.
Section <ref> describes the abstract domain originally used for
the sharing analysis algorithm,
Section <ref> describes the new abstract domain that is
now used,
Section <ref> defines the algorithm itself and
Section <ref> gives an extended example.
Section <ref> briefly discusses precision and efficiency
issues.
Section <ref> discusses related work and
Section <ref> concludes.




§ AN OVERVIEW OF PAWNS 



A more detailed introduction to Pawns is given in <cit.>.
Pawns has many similarities with other functional languages.  It supports
algebraic data types with parametric polymorphism, higher order
programming and curried function definitions.  It uses strict evaluation.
In addition, it supports destructive update via “references” (pointers)
and has a variety of extra annotations to make impure effects more clear
from the source code and allow them to be encapsulated in pure code.
Pawns also supports a form of global variables (called state variables)
which support encapsulated effects, but we do not discuss them further
here as they are handled in essentially the same way as other variables
in sharing analysis.  Pure code can be thought of in a declarative way,
were values can be viewed abstractly, without considering how they
are represented.  Code that uses destructive update must be viewed at a
lower level, considering the representation of values, including sharing.
We discuss this lower level view first, then briefly present how impurity
can be encapsulated to support the high level view.  We use Haskell-like
syntax for familiarity.



 §.§ The low level view



Values in Pawns are represented as follows.  Constants (data constructors
with no arguments) are represented using a value in a single word.
A data constructor with N>0 arguments is represented using a word
that contains a tagged pointer to a block of N words in main memory
containing the arguments.  For simple data types such as lists the tag
may be empty.  In more complex cases some bits of the pointer may be used
and/or a tag may be stored in a word in main memory along with the arguments.
Note that constants and tagged pointers are not always stored in main
memory and Pawns variables may correspond to registers that contain
the value.  Only the arguments of data constructors are guaranteed to
be in main memory.  An array of size N is represented in the same
way as a data constructor with N arguments, with the size given by
the tag. Functions are represented as either a constant (for functions
that are known statically) or a closure which is a data constructor
with a known function and a number of other arguments.

Pawns has a  type constructor, representing a
reference/pointer to a value of type  (which must be stored
in memory).  Conceptually we can think of a corresponding 
data constructor with a single argument, but this is never explicit
in Pawns code.  Instead, there is an explicit dereference operation:
 denotes the value  points to.  There are two
ways references can be created: let bindings and pattern bindings.  A let
binding  allocates a word in main memory, initializes it
to  and makes  a reference to it (Pawns omits
Haskell's  and  keywords; the scope is the
following sequence of statements/expressions).  In a pattern
binding, if  is the argument of a data constructor pattern,
 is bound to a reference to the corresponding argument of the
data constructor if pattern matching succeeds (there is also a primitive
that returns a reference to the i^th element of an array).
Note it is not possible
to obtain a reference to a Pawns variable: variables do not denote memory
locations.  However, a variable  of type  denotes
a reference to a memory location containing a value of type  and
the memory location can be destructively updated by .

Consider the following code.  Two data types are defined. The code
creates a reference to  ( is stored in a newly
allocated memory word) and a reference to that reference (a pointer
to the word containing  is put in another allocated word).
It also creates a list containing constants  and 
(requiring the allocation of two cons cells in memory; the 
is copied).  It deconstructs the list to obtain pointers to the head and
tail of the list (the two words in the first cons cell) then destructively
updates the head of the list to be .




The memory layout after the assignment can be pictured as follows,
where boxes represent main memory words and  and 
followed by an arrow represent pointers (no tag is used in either case):


[scale=1.0]
at (0,1.5) (c1) ;
at (3.5,1.5) (c2)
        [4em][4em];
at (7.5,1.5) (ct)
        [4em][4em];
[->] (c1) – (c2);
at (2.8,1.2) (h) ;
at (4.5,1.5) (t1) ;
at (4.0,1.2) (t) ;
at (8.2,0.7) (nb)
        [4em];
at (4.4,0.7) (np) ;
at (3.4,0) (npp) ;
at (6.0,0) (npb)
        [4em];
at (6.2,0.0) (r) ;
[->] (npp) – (npb);
[->] (r) – (nb);
[->] (np) – (nb);
at (0,0.7) (hp) ;
at (1,0.7) (hp1) ;
at (0,0) (tp) ;
at (1,0) (tp1) ;
[->] (hp1) – (h);
[->] (t1) – (ct);
[->] (tp1) – (t);



The destructive update above changes the values of both  and
 (the representations are shared).  One of the novel features
of Pawns is that the source code must be annotated with “!” to make it
obvious when each “live” variable is updated.  If both 
and  are used later, the assignment statement above must
be written as follows, with  prefixed with “!” and an
additional annotation attached to the whole statement indicating
 may be updated:



We say that the statement directly updates 
and indirectly updates , due to sharing of
representations.  Similarly, if  was passed to a
function that may update it, additional annotations are required.
For example,  makes the direct
update of  and indirect update of  clear.
Sharing analysis is used to ensure that source code contains all the
necessary annotations.  One aim of Pawns is that any effects of code
should be made clear by the code.  Pawns is an acronym for Pointer
Assignment With No Surprises.


Pawns functions have extra annotations in type signatures to
document which arguments may be updated.  For additional documentation,
and help in sharing analysis, there are annotations to declare what
sharing may exist between arguments when the function is called
(a precondition) and what extra sharing may be added by executing the
function (called a postcondition, though it is the union of the pre- and
post-condition that must be satisfied after a function is executed).
For example, we may have:
[4]


The “!” annotation on parameter  declares the first
argument of  is mutable.  The default is that arguments
are not mutable.
As well as checking for annotations on assignments and function calls,
sharing analysis is used to check that all parameters which may be
updated are declared mutable in type signatures, and pre- and post-conditions
are always satisfied.  For example, assuming the previous code which
binds , the call  annotates all
modified variables but violates the precondition of 
because there is sharing between  and  at the
time of the call.  Violating this precondition allows cyclic structures
to be created, which is important for understanding the code.
If the precondition was dropped, the second argument of 
would also need to be declared mutable in the type signature and the
assignment to  would require  to be annotated.
In general, there is an inter-dependence between “!” annotations in the
code and pre- and post-conditions.  More possible sharing at a call means
more “!” annotations are needed, more sharing in (recursive) calls and
more sharing when the function returns.

Curried functions and higher order code are supported by attaching
sharing and destructive update information to each arrow in a type,
though often the information is inferred rather than being given
explicitly in the source code.  For example, implicit in the declaration
for  above is that  called with a single
argument of type  creates a closure of type 
containing that argument (and thus sharing the object of type
).  The explicit sharing information describes applications
of this closure to another argument.  There is a single argument in
this application, referred to with the formal parameter .
The other formal parameter, , refers to the argument of the
closure.  In general, a type with N arrows in the “spine” has K+N
formal parameters in the description of sharing, with the first K
parameters being closure arguments.

The following code defines binary search trees of integers
and defines a function that takes a pointer to a tree and
inserts an integer into the tree.  It uses destructive update, as would
normally be done in an imperative language.  The declarative alternative
must reconstruct all nodes in the path from the root down to the new node.
Experiments using our prototype implementation of Pawns indicate that for
long paths this destructive update version is as fast as hand-written
C code whereas the “pure” version is more than twenty times slower,
primarily due to the overhead of memory allocation.

[4]






 §.§ The high level view



Whenever destructive update is used in Pawns, programmers must be aware
of potential sharing of data representations and take a low level view.
In other cases it is desirable to have a high level view of values,
ignoring how they are represented and any sharing that may be present.
For example, in the two trees  and  depicted below,
it is much simpler if we do not have to care or know about the sharing
between the trees and within tree .  The high level view
is they are both just .


[scale=1.0]
at (-0.5,1.8) (t1) ;
at (2.5,1.8) (t2) ;
at (1.0,1.0) (t1a)
  [4em][4em][4em];
[->] (-0.2,1.6) – (-0.6,1.3);
[->] (2.9,1.6) – (4.5, 1.3);
at (6.5,1.0) (t2a)
  [4em][4em][4em];
at (3.0,0.0) (l1a)
  [4em][4em][4em];
[->] (-0.4,0.8) – (1.0,0.4);
[->] (2.4,0.8) – (1.2, 0.4);
at (8.5,0.0) (l2a)
  [4em][4em][4em];
[->] (5.1,0.8) – (1.6,0.4);
[->] (7.9,0.8) – (7.0, 0.4);



Pawns has a mechanism to indicate that the high level view is
taken.  Pre- and post-conditions can specify sharing with a special
pseudo-variable named [There is conceptually
a different  variable for each distinct type.].
The sharing analysis of the Pawns compiler allows a distinction between
“abstract” variables, which share with  and for which
the programmer takes a high level view, and “concrete” variables for
which the programmer must understand the representation and explicitly
declare all sharing in pre- and post-conditions.  The analysis checks
that no live abstract variables can be destructively updated.  Thus if a
function has a parameter which is updated, it must be declared mutable and
must not be declared to share with  in the precondition
(non-mutable parameters may or may not share with ).
Checking of preconditions ensures that abstract variables are not
passed to functions which expect concrete data structures.  For example,
an abstract tree cannot be passed to  because the
precondition allows no sharing with .  It is important
that the tree structure is known when  is used
because the result depends on it.  For example, inserting into the right
subtree of  only affects this subtree whereas inserting into
the right subtree of  (which has the same high level value)
also changes the left subtree of both  and .
Note that concrete variables can be passed to functions which allow
abstract arguments.  Pawns type
signatures that have no annotations concerning destructive update or
sharing implicitly indicate no arguments are destructively updated and
the arguments and result share with . Thus a subset of
Pawns code can look like and be considered as pure functional code.

The following code defines a function that takes a list of integers and
returns a binary search tree containing the same integers.  Though it uses
destructive update internally, this impurity is encapsulated and it can
therefore be viewed as a pure function.  The list that is passed in as an
argument is never updated and the tree returned is abstract so it is
never subsequently updated (a concrete tree could be returned if an
explicit postcondition without  was given).
An initially empty tree is created locally.
It is destructively updated by inserting each integer of the list into it
(using , which calls ), then the
tree is returned.  Within the execution of  it is important
to understand the low level details of how the tree is represented,
but this information is not needed outside the call.






§ CORE PAWNS



An early pass of the Pawns compiler converts all function definitions
into a core language by flattening nested expressions, introducing extra
variables et cetera.  A variable representing the return value of the
function is introduced and expressions are converted to bindings for
variables.  A representation of the core language version of code is
annotated with type, liveness and other information prior to sharing
analysis.  We just describe the core language here.  The right side of
each function definition is a statement (described using the definition
of type  below), which may contain variables, including
function names (), data constructors ()
and pairs containing a pattern () and statement for case
statements.  All variables are distinct except for those in recursive
instances of  and variables are renamed to avoid any
ambiguity due to scope.




Patterns in the core language only bind references to arguments — the
arguments themselves must be obtained by explicit dereference operations.
Pawns supports “default” patterns but for simplicity of presentation
here we assume all patterns are covered in core Pawns and we include an
error primitive.  Similarly, we just give the general case for application
of a variable to N>0 arguments; our implementation distinguishes some
special cases.  Memory is allocated for , 
(for non-constants) and  (for unsaturated applications which
result in a closure).
The runtime behaviour of  is identical to 
but it is treated differently in type analysis.

Sharing and type analysis
cannot be entirely separated.  Destructive update in the presence of
polymorphic types can potentially violate type safety or “preservation”
— see <cit.>, for example.  For a variable whose type is
polymorphic (contains a type variable), we must avoid assigning a value
with a less general type.  For example, in  the type
of  is “list of ”, where  is a type variable.
Without destructive update it should be possible to use 
wherever a list of any type is expected.  However, if  is
then assigned a list containing integers (which has a less general type),
passing it to a function that
expects a list of functions violates type safety (“calling” an arbitrary
integer is not safe).  Pawns allows expressions to have their inferred
types further instantiated using “::”, and the type checking pass of
the compiler also inserts some type instantiation.  The type checking
pass ensures that direct update does not involve type instantiation but
to improve flexibility, indirect update is checked during the sharing
analysis.



§ THE ABSTRACT DOMAIN



The representation of the value of a variable includes some set of main
memory words (arguments of data constructors).  Two variables share if
the intersection of their sets of main memory words is not empty. The
abstract domain for sharing analysis must maintain a conservative
approximation to all sharing, so we can tell if two variables possibly
share (or definitely do not share).  The abstract domain we use is a
set of pairs (representing possibly intersecting sets of main memory
locations) of variable components.  The different components of
a variable partition the set of main memory words for the variable.

The components of a variable depend on its type.  For non-recursive
types other than arrays, each possible data constructor argument is
represented separately.  For example,
the type  can have an argument
of an outer  data constructor, an inner 
and  and .  A component can be represented
using a list of  pairs containing a data constructor and an
argument number, giving the path from the outermost data constructor
to the given argument.  For example, the components of the type above
can be written as: , ,
 and .
If variable  has value , the expression
 represents the single main memory word containing the
occurrence of .

For  types we proceed as if there was a 
data constructor, so  represents the word 
points to.  For function types, values may be closures.  A closure that
has had K arguments supplied is represented as a data constructor
𝙲𝚕_K with these K arguments; these behave in the same way as
other data constructor arguments with respect to sharing,
except Pawns provides no way to obtain a pointer to a closure argument.
Closures also
contain a code pointer and an integer which are not relevant to sharing so
they are ignored in the analysis.
We also ignore the subscript on the data constructor
for sharing analysis because type and sharing analysis only give a
lower bound on the number of closure arguments.  Our analysis orders
closure arguments so that the most recently supplied argument is first
(the reverse of the more natural ordering).  Consider the code below,
where  is a function that is defined with four or more
arguments.  The sharing analysis proceeds as if the memory layout was as
depicted in the diagram.  The pre- and post-conditions of 
are part of the type information associated with ,
 and .

[c]0.4


[c]0.5

[scale=1.0]
at (0,3.3) (ip1) ;
at (5.5,3.3) (ip2)
        [4em];
[->] (ip1) – (ip2);
at (0,2.6) (c1) ;
at (2.9,2.6) (c1a)
        [4em][4em];
[->] (c1) – (c1a);
at (2.8,2.6) (c1b) ;
at (0,1.9) (c2) ;
at (0.7,1.9) (c2a) ;
at (1.6,2.3) (c2b) ;
[->] (c2a) – (c2b);
[->] (4.1,2.6) – (ip2) ;
at (0,1.2) (c3) ;
at (3.5,1.2) (f2)
        [4em][4em][4em];
at (2.8,1.2) (f2a) ;
[->] (c3) – (f2);
[->] (5.2,1.3) – (ip2) ;
at (2.8,1.4) (f2c) ;




For arrays,  is used to represent all words in the array.
The expression,  represents the arguments of all
 elements in an array  of  values.
For recursive types, paths are “folded” <cit.>
so there are a finite number
of components.  Here we present the original published version of the
abstract domain, which is also used in later examples of the sharing
analysis algorithm.  The compiler now uses a more expressive abstract
domain for recursive types, described in Section <ref>.
If a type T has sub-component(s) of type T we use
the empty path to denote the sub-component(s).  In general, we construct
a path from the top level and if we come across a sub-component of type T
that is in the list of ancestor types (the top level type followed by the
types of elements of the path constructed so far) we just use the path
to the ancestor to represent the sub-component.  Consider the following
mutually recursive types that can be used to represent trees which
consist of a node containing an integer and a list of sub-trees:



For type  we have the components
 (this folded path represents both  and
, since they are of type ),
 and
.
The expression  represents the set of memory
words that
are the first argument of  in variable  of type
. 
For type  we have the components
 (for , of type ),
 and
 (which is also the folded version of
, of type ).
In our sharing analysis algorithm we use a function  (fold
component) which takes a v.c pair,
and returns v.c' where c' is the correctly folded component for the
type of variable v.  For example,  =
, assuming  has type .

As well as containing pairs of components for distinct variables which may
alias, the abstract domain contains “self-alias” pairs for
each possible component of a variable which may exist.  Consider the
following two bindings and the corresponding diagram (as with
, no tag is used for ):

[c]0.4


[c]0.5

[scale=1.0]
at (0,1.7) (c1) ;
at (3.5,1.7) (c2)
        [4em][4em];
[->] (c1) – (c2);
at (0,0.7) (d1) ;
at (3.5,0.7) (d2)
        [4em][4em];
at (2.8,1.5) (c2a) ;
at (2.8,0.7) (d2a) ;
[->] (d1) – (d2);
[->] (d2a) – (c2a);




With our domain, the most precise description of sharing after
these two bindings is as follows.  We represent an alias pair as a set
of two variable components.  The first five are self-alias pairs and
the other two describe the sharing between  and .

[4]
	

Note there is no self-alias pair for  since there is no strict
sub-part of  that is an .  Similarly, there
is no alias between  and any part of .
Although the value  is used as the first argument of
 in , this is not a main memory word that is
used to represent the value of  (indeed, the value of 
has no  cells).  The tagged pointer value stored in variable
 (which may be in a register) is copied into the cons cell. 
Such descriptions of sharing are an abstraction of computation states.
The set above abstracts all computation states in which 
is a tree with a single node,  is a list of trees, elements
of  may be  or have  as a subtree, and
there are no other live variables with non-atomic values.



§ THE NEW ABSTRACT DOMAIN



The Pawns compiler no longer uses empty paths to represent components
of variables with recursive types.  One of the motivations was to get
more precise sharing analysis for code such as the following, which
repeatedly assigns different RTrees to a single pointer variable
(similar imprecision occured for other recursively defined types).

With the original domain, the memory word  is represented
by , which also represents words that are the first
argument of a  cells within the tree.  The compiler
concludes the assignments may update  and  and
introduce sharing between ,  and .
The code can be re-written by renaming  for each assignment
to get more precised analysis, but it can be inconvenient for programmers
to repeatedly rename variables and ideally it should not be necessary.

The new abstract domain used by the compiler contains all non-empty paths
that avoid repetitions corresponding to recursion in the type. Thus
 will typically have four components: ,
 (instead of ), and both 
and . Only paths with repeated data constructors
are folded.  For example,  is folded
to become . Note that 
represents memory words that arguments of  whereas
 represents memory words that arguments of
, and these must be distinct, even though they have the
same type. This distinction was not made in the old domain.  Similarly,
there will typically be five components of , 
plus the four tree components prefixed by , so there is a
distinction made between the memory word used for  and those
used by the tree. With the new abstract domain, sharing analysis for
let bound ref variables loses no information unless there is recursion
through the  type. Note that the examples below use the old
abstract domain.  Also, the sharing algorithm given below treats empty
paths as special in some places so the current compiler uses a some small
modifications to this algorithm.



§ THE SHARING ANALYSIS ALGORITHM



We now describe the sharing analysis algorithm.  Overall, the compiler
attempts to find a proof that for a computation with a depth D of
(possibly recursive) function calls, the following condition C holds,
assuming C holds for all computations of depth less than D.  This
allows a proof by induction that C holds for all computations that
terminate normally.



C: For all functions f, if the precondition of
f is satisfied (abstracts the computation state)
whenever f is called, then


  * for all function calls and assignment statements in f, any live
variable that may be updated at that point in an execution of f is
annotated with “!”,

  * there is no update of live “abstract” variables when executing
f,

  * all parameters of f which may be updated when
executing f are declared mutable in the type signature of f,

  * the union of the pre- and post-conditions of f abstracts
the state when f returns plus the values
of mutable
parameters in all states during the execution of f,

  * for all function calls and assignment statements in f, any live
variable that may be directly updated at that point is updated with a value
of the same type or a more general type, and

  * for all function calls and assignment statements in f, any live
variable that may be indirectly updated at that point only shares with
variables of the same type or a more general type.


The algorithm is applied to each function definition
in core Pawns to compute an approximation to the sharing before and
after each statement (we call it the alias set).  This can be used to
check points 1, 2, 4 and 6 above. The algorithm checks that
preconditions are satisfied for each function call, allowing
the induction hypothesis to be used.  Point 3
is established using point 1 and a simple syntactic check that any
parameter of f that is annotated “!” in the definition is declared
mutable in the type signature (parameters are considered live throughout
the definition).  Point 5 relies on 3 and the type checking pass.
The core of the algorithm is to compute the alias set
after a statement, given the alias set before the statement.  This is
applied recursively for compound statements in a form of abstract
execution.  Note that for point 4, if a statement changes the set of
memory cells used to represent a mutable parameter, the algorithm computes
the sharing for the union of the two sets of cells.

We do not prove correctness of the algorithm but hope our presentation
is sufficiently detailed to have uncovered any bugs.  A proof would
have a separate case for each kind of statement in the core language,
showing that if the initial alias set abstracts the execution state
before the statement the resulting alias set abstracts the execution
state after the statement.  This would require a more formal description
of execution states and their relationship with the core language and
the abstract domain.  The abstract domain relies on type information so
the sharing analysis relies on type preservation in the execution. Type
preservation also relies on sharing analysis.  Thus a completely formal
approach must tackle both problems together.  Although our approach is not
formal, we do state the key condition C, which has points relating to
both sharing and types, and we include  in the core language.

The alias set used at the start of a definition is the precondition
of the function.  This implicitly includes self-alias pairs
for all variable components of the arguments of the function and
the pseudo-variables 𝚊𝚋𝚜𝚝𝚛𝚊𝚌𝚝_T for each type T used.
Similarly, the postcondition implicitly includes self-alias pairs for
all components of the result (and the 𝚊𝚋𝚜𝚝𝚛𝚊𝚌𝚝_T variable if
the result is abstract)[Self-aliasing for arguments and results is
usually desired.  For the rare cases it is not, we may provide a mechanism
to override this default in the future.].  As abstract execution proceeds,
extra variables from the function body are added to the alias set and
variables that are no longer live can be removed to improve efficiency.
For each program point, the computed alias set abstracts the computation
state at that point in all concrete executions of the function that
satisfy the precondition.  For mutable parameters of the function, the
sharing computed also includes the sharing from previous program points.
The reason for this special treatment is explained when we discuss the
analysis of function application.  The alias set computed for the end
of the definition, with sharing for local variables removed, must be a
subset of the union of the pre- and post-condition of the function.

Before sharing analysis, a type checking/inference pass is completed which
assigns a type to each variable and function application.  This
determines the components for each variable.  Polymorphism is also
eliminated as follows.  Suppose we have a function ,
which returns the list containing the first  elements of
:

[4]

For each call to , the pre- and post-conditions
are determined based on the type of the application.  An application to
lists of Booleans will have two components for each variable whereas an
application to lists of lists of Booleans will have four.  When analysing
the definition of  we instantiate type variables such as
 above to .  This type has a single component
which can be shared to represent possible sharing of arbitrary components
of an arbitrary type.
Type checking prevents sharing between non-identical types, such as
 and .  Finally, we assume there is no type which is
an infinite chain of refs, for example, 
(for which type folding results in an empty component rather than a
 component; this is not a practical limitation).

Suppose a_0 is the alias set just before statement s.  The following
algorithm computes 𝚊𝚕𝚒𝚊𝚜(s, a_0), the alias set just after
statement s.  The algorithm structure follows the recursive definition
of statements and we describe it using pseudo-Haskell, interspersed with
discussion. The empty list is written , non-empty lists
are written [𝚊,𝚋,𝚌] or  and ++
denotes list concatenation.
At some points we use high level declarative set
comprehensions to describe what is computed and naive implementation may
not lead to the best performance.


mmm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄m

 



  

  
    {{𝚟1.c_1,𝚟1.c_2}|{𝚟2.c_1,𝚟2.c_2}∈𝚊0} 

  
    {{𝚟1.c_1,v.c_2}|{𝚟2.c_1,v.c_2}∈𝚊0} 

  

  𝚊0∪𝚜𝚎𝚕𝚏1∪𝚜𝚑𝚊𝚛𝚎1 



  

  
    {{𝚟1.[𝚁𝚎𝚏.1],𝚟1.[𝚁𝚎𝚏.1]}} ∪ 


    {{𝚏𝚌 (𝚟1.(𝚁𝚎𝚏.1:c_1)),
		𝚏𝚌 (𝚟1.(𝚁𝚎𝚏.1:c_2))}|{𝚟2.c_1,𝚟2.c_2}∈𝚊0} 

  
    {{𝚏𝚌 (𝚟1.(𝚁𝚎𝚏.1:c_1)),v.c_2}|{𝚟2.c_1,v.c_2}∈𝚊0} 

  

  𝚊0∪𝚜𝚎𝚕𝚏1∪𝚜𝚑𝚊𝚛𝚎1 



Sequencing is handled by function composition.  To bind a fresh variable
 to a variable  the self-aliasing of 
(including aliasing between different components of )
is duplicated for  and the aliasing for each component
of  (which includes self-aliasing) is duplicated for .
Binding  to
 is done in a similar way, but the components of 
must have  prepended to them and the result folded, and
the  component of  self-aliases.
Folding is
only needed for the rare case of types with recursion through .

[4]

mmm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄m

  

  

  
    { v_a.c_a |{𝚟1.[𝚁𝚎𝚏.1],v_a.c_a}∈𝚊0} 

  

  

  
    {{𝚏𝚌 (v_a.(c_a++c_1)),
		𝚏𝚌 (v_b.(c_b++c_2))}|

v_a.c_a ∈∧ v_b.c_b ∈∧{𝚟2.c_1,𝚟2.c_2}∈𝚊0} 

  
    {{𝚏𝚌 (v_a.(c_a++c_1)),v.c_2}| 

v_a.c_a ∈∧{𝚟2.c_1,v.c_2}∈𝚊0}

 

 𝚊0∪𝚜𝚎𝚕𝚏1𝚊𝚕∪𝚜𝚑𝚊𝚛𝚎1𝚊𝚕 

  

  

  
    {{𝚟1.(𝚁𝚎𝚏.1:d:c_1),v.c_2}|{𝚟1.(𝚁𝚎𝚏.1:d:c_1),v.c_2}∈𝚊0} 

 (𝚊0∖) ∪𝚜𝚎𝚕𝚏1𝚊𝚕∪𝚜𝚑𝚊𝚛𝚎1𝚊𝚕 



Assignment to an existing variable differs from binding a fresh variable
in three ways.  First, self-sharing for  is not
added since it already exists.  Second,  may
alias several variable components (the live subset of these variables
must be annotated with “!” on the
assignment statement; checking such annotations is a primary purpose
of the analysis).  All these variables end up sharing with 
and what  shares with (via ) plus themselves
and each other (via ).  The components must be concatenated
and folded appropriately.  Third, if  is not a mutable
parameter the existing sharing with a path strictly longer than
 (that is, paths of the form 𝚁𝚎𝚏.1:d:c_1)
can safely be removed, improving precision.
The component  represents the single memory word
that is overwritten and whatever the old contents shared with is no
longer needed to describe the sharing for .  For mutable
parameters the old value may share with variables from the calling
context and we retain this information, as explained later.
Consider the example below, where  and  are as
before and local variables  and  are references to
the element of . The value assigned, , is
.


[c]0.5

[scale=1.0]
at (2.2,4.2) (l1) Initial state;
at (0,3.7) (c1) ;
at (3.5,3.7) (c2)
        [3em][3em];
at (3.0,3.5) (c2a) ;
[->] (c1) – (c2);
at (0,2.7) (d1) ;
at (3.5,2.7) (d2)
        [3em][3em];
at (3.0,2.7) (d2a) ;
[->] (d1) – (d2);
at (0,2.2) (e1) ;
at (0.7,2.2) (e1a) ;
at (2.4,2.5) (e1b) ;
[->] (e1a) – (e1b);
at (0,1.7) (g1) ;
at (0.7,1.7) (g1a) ;
at (2.7,2.4) (g1b) ;
[->] (g1a) – (g1b);
at (0,1.2) (f1) ;
at (3.5,1.2) (f2)
        [3em][3em];
at (2.8,1.2) (f2a) ;
[->] (f1) – (f2);
at (3.0,1.4) (f2c) ;
at (2.5,0.4) (h2)
        [3em][3em];
at (3.5,-0.2) (h3)
        [3em][3em];
[->] (4.0,1.1) – (2.2,0.7);
[->] (2.0,0.3) – (2.4,-0.1);
[->] (d2a) – (c2a);



[c]0.5

[scale=1.0]
at (2.2,4.2) (l1) After ;
at (0,3.7) (c1) ;
at (3.5,3.7) (c2)
        [3em][3em];
at (3.0,3.5) (c2a) ;
[->] (c1) – (c2);
at (0,2.7) (d1) ;
at (3.5,2.7) (d2)
        [3em][3em];
at (3.0,2.7) (d2a) ;
[->] (d1) – (d2);
at (0,2.2) (e1) ;
at (0.7,2.2) (e1a) ;
at (2.4,2.5) (e1b) ;
[->] (e1a) – (e1b);
at (0,1.7) (g1) ;
at (0.7,1.7) (g1a) ;
at (2.7,2.4) (g1b) ;
[->] (g1a) – (g1b);
at (0,1.2) (f1) ;
at (3.5,1.2) (f2)
        [3em][3em];
at (2.8,1.2) (f2a) ;
[->] (f1) – (f2);
at (3.0,1.4) (f2c) ;
at (2.5,0.4) (h2)
        [3em][3em];
at (3.5,-0.2) (h3)
        [3em][3em];
[->] (4.0,1.1) – (2.2,0.7);
[->] (2.0,0.3) – (2.4,-0.1);
[->] (d2a) – (f2c);




There is aliasing of ,  and
 so all these variables have the sharing of 
and self-sharing added.  Generally we must also add sharing between all
pairs of these variables.  For example,


must be added because the  component of  did
not previously exist.  The old sharing of  with  is
discarded.  Note that we cannot discard the old sharing of  and
 with  for two reasons.  First, no definite
aliasing information is maintained, so we cannot be sure 
or  are modified at all.  Second, the assignment updates
only one memory word whereas there may be other words also represented
by .  In some cases the old sharing of 
is discarded and immediately added again.  Consider the following example,
which creates a cyclic list.

[c]0.5

[scale=1.0]
at (2.2,2.9) (l1) Initial state;
at (0,2.5) (v1) ;
at (0,1.5) (v2) ;
at (3.0,1.5) (c2)
        [4em][4em];
[->] (v2) – (c2);
at (3.5,1.8) (tt) ;
[->] (v1) – (tt);
at (3.8,1.5) (t) ;
at (2.3,1.3) (h) ;
at (0,0.5) (v3) ;
at (3.0,0.5) (c3)
        [4em][4em];
[->] (v3) – (c3);
at (2.4,0.8) (h3) ;
at (3.8,1.4) (t2) ;
[->] (t2) – (h3);
at (2.0,0.6) (bot)  ;



[c]0.5

[scale=1.0]
at (2.2,2.9) (l1) After ;
at (0,2.5) (v1) ;
at (0,1.5) (v2) ;
at (3.0,1.5) (c2)
        [4em][4em];
[->] (v2) – (c2);
at (3.5,1.8) (tt) ;
[->] (v1) – (tt);
at (3.8,1.5) (t) ;
at (2.3,1.3) (h) ;
[->] (t) – (3.8,0.9) – (2.3,0.9) – (h);
at (0,0.5) (v3) ;
at (3.0,0.5) (c3)
        [4em][4em];
[->] (v3) – (c3);
at (2.4,0.8) (h3) ;
at (3.8,1.4) (t2) ;
at (2.0,0.6) (bot)  ;




The sharing between  and  is discarded but
added again (via ) because  also shares with
. Correctness of the algorithm when cyclic terms are created
depends on the abstract domain we use.  A more expressive domain could
distinguish between different cons cells in a list.  For example, if
types are “folded” at the third level of recursion rather than the
first, the domain can distinguish three classes of cons cells, where the
distance from the first cons cell, modulo three, is zero, one or two.
For a cyclic list with a single cons cell, that cons cell must be in all
three classes and our algorithm would need modification to achieve this.
However, in our domain types are folded at the first level of recursion so
we have a unique folded path for each memory cell in cyclic data structure
(cyclic terms can only be created with recursive types).  There is no
distinction between the first and second cons cell in a list, for example.


mmm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mv_1,… v_N

  

  
    {{𝚏𝚌 (𝚟.[𝚍𝚌.i]),𝚏𝚌 (𝚟.[𝚍𝚌.i])}| 1 ≤ i ≤ N }  ∪ 

{{𝚏𝚌 (𝚟.(𝚍𝚌.i:c_1)),
	𝚏𝚌 (𝚟.(𝚍𝚌.j:c_2)) }|{v_i.c_1,v_j.c_2}∈𝚊0} 

  
    {{𝚏𝚌 (𝚟.(𝚍𝚌.i:c_1)),
	w.c_2 }|{v_i.c_1,w.c_2}∈𝚊0} 

  

  𝚊0∪𝚜𝚎𝚕𝚏1∪𝚜𝚑𝚊𝚛𝚎1 



The  case can be seen as equivalent to  and binding a variable to a data constructor with N variable
arguments is a generalisation.  If there are multiple v_i that
share, the corresponding components of  must also share; these
pairs are included in . 

[4]

mmm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄m

  

  
    {{𝚟1.c_1,𝚟1.c_2}|{𝚏𝚌(𝚟2.(𝚁𝚎𝚏.1:c_1)),𝚏𝚌(𝚟2.(𝚁𝚎𝚏.1:c_2))}∈𝚊0} 

  
    {{𝚟1.c_1,v.c_2}|{𝚏𝚌(𝚟2.(𝚁𝚎𝚏.1:c_1)),v.c_2}∈𝚊0} 

  
    {{,v.c}|{,v.c}∈ (𝚜𝚎𝚕𝚏1∪𝚜𝚑𝚊𝚛𝚎1) } 

  

  

  𝚊0∪𝚜𝚎𝚕𝚏1∪𝚜𝚑𝚊𝚛𝚎1 

  

  (𝚊0∪𝚜𝚎𝚕𝚏1∪𝚜𝚑𝚊𝚛𝚎1)
∖𝚎𝚖𝚙𝚝𝚢1 



The  case is similar to the inverse of  in
that we are removing  rather than prepending it (the
definition implicitly uses the inverse of ).  However,
if the empty component results we must check that such a component exists
for the type of .


mmm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mv_1,… v_N

  

  “w_1, … w_K+N) = r” 

   

   

  

  

  .[.K],….[.1],v_1,… v_N  

   

   

  

  

   

  
	{{𝚟.[𝙲𝚕.i],𝚟.[𝙲𝚕.i]}| 1≤ i≤ N
} ∪


	{{𝚟.((𝙲𝚕.(N+1-i)):c_1),𝚟.((𝙲𝚕.(N+1-j)):c_2)} |
 {v_i.c_1,v_j.c_2}∈𝚊0} ∪ 


    {{𝚟.((𝙲𝚕.(i+N)):c_1),𝚟.((𝙲𝚕.(j+N)):c_2)}|
 {𝚏.((𝙲𝚕.i):c_1),𝚏.((𝙲𝚕.j):c_2)}∈𝚊0} 

  
	{{𝚟.((𝙲𝚕.(N+1-i)):c_1),x.c_2} |{v_i.c_1,x.c_2)}∈𝚊0} ∪ 


    {{𝚟.((𝙲𝚕.(i+N)):c_1),x.c_2}|{𝚏.((𝙲𝚕.i):c_1),x.c_2}∈𝚊0} 

   

  
    {{x_1.c_1,x_3.c_3}|{x_1.c_1,x_2.c_2}∈𝚙𝚘𝚜𝚝∧{x_2.c_2,x_3.c_3}∈𝚊0} 

  
    {{x_1.c_1,x_2.c_2}|{x_1.c_1,v_i.c_3}∈𝚊0∧{x_2.c_2,v_j.c_4}∈𝚊0 ∧

	{v_i.c_3,v_j.c_4}∈𝚙𝚘𝚜𝚝∧
	v_i ∈𝚖𝚞𝚝∧ v_j ∈𝚖𝚞𝚝} 

  

     𝚊0∪𝚜𝚎𝚕𝚏𝚌∪𝚜𝚑𝚊𝚛𝚎𝚌∪𝚙𝚘𝚜𝚝𝚝∪𝚙𝚘𝚜𝚝𝚖 



For many  occurrences the function is known statically and we can
determine if the function is actually called or a closure is created
instead.  However, in general we must assume either could happen and
add sharing for both.  If a closure is created, the first N closure
arguments share with the N arguments of the function call and any
closure arguments of  share with additional closure arguments of
the result (this requires renumbering of these arguments).

Analysis of
function calls relies on the sharing and mutability information attached
to all arrow types.  Because Pawns uses the syntax of statements to
express pre- and post-conditions, our implementation uses the sharing
analysis algorithm to derive an explicit alias set representation
(currently this is done recursively, with the level of recursion limited
by the fact than pre- and post-conditions must not contain function
calls).  Here we ignore the details of how the alias set representation
is obtained.  The compiler also uses the sharing information immediately
before an application to check that the precondition is satisfied,
all required “!” annotations are present and abstract variables are
not modified.

Given that the precondition is satisfied, the execution of a function
results in sharing of parameters that is a subset of the union of
the declared pre- and post-conditions (we assume the induction hypothesis
holds for the sub-computation, which has a smaller depth of recursion).
However, any sharing between non-mutable arguments that exists
immediately after the call must exist before the call.
The analysis algorithm does not add sharing between non-mutable
arguments in the precondition as doing so would unnecessarily restrict
how “high level” and “low level” code can be mixed.  It is important
we can pass a variable to a function that allows an abstract argument
without the analysis concluding the variable subsequently shares with
, and therefore cannot be updated.  Thus
 is just the declared
postcondition plus the subset of the precondition which involves mutable
parameters of the function, renamed appropriately.
The last N formal parameters,  
w_K+1… w_K+N are renamed as the arguments of the call,
v_1 … v_N and the formal result r is renamed .
The formal parameters w_1… w_K represent closure arguments
K … 1 of .  Thus a variable component such as
w_1 is renamed K.

It is also necessary to include one step of transitivity in the sharing
information: if variable components x_1.c_1 and x_2.c_2 alias in
 and x_2.c_2 and x_3.c_3 (may) alias before the function
call, we add an alias of x_1.c_1 and x_3.c_3 (in ).
Function parameters are proxies for
the argument variables as well as any variable components they may alias
and when functions are analysed these aliases are not known.
This is why the transitivity step is needed, and why mutable parameters
also require special treatment.  If before the call, x_1.c_1 and x_2.c_2
may alias with mutable parameter components v_i.c_3 and v_j.c_4,
respectively, and the two mutable parameter components alias in
 then x_1.c_1 and x_2.c_2 may alias after the call;
this is added in .  Consider the example below, where
we have a pair  (of references to references to integers)
and variables  and  share with the two elements
of , respectively.  When  is passed to function

as a mutable parameter, sharing between  and  is
introduced.  The sharing of the mutable parameter in the postcondition,
, results
in sharing between  and  being added in the analysis.

[c]0.5

[scale=0.9]
at (2.2,3.6) (l1) Initial state;
at (0,3.0) (x) ;
at (2.8,1.0) (ba)
        [2em];
at (3.8,1.0) (bb)
        [2em];
at (0,2.4) (v1) ;
at (3.3,2.4) (v1a) [2em][2em];
[->] (v1) – (v1a);
at (0,1.8) (y) ;
at (1.6,1.8) (ya) [2em];
at (4.8,1.8) (yb) [2em];
[->] (y) – (ya);
[->] (1.6,1.6) – (ba);
[->] (4.8,1.6) – (bb);
[->] (2.9,2.2) – (ya);
[->] (3.8,2.2) – (yb);
[->] (x) – (4.2,3.0) – (yb);
at (0,0.1) (bot) ;



[c]0.5

[scale=0.9]
at (2.2,3.6) (l1) After ;
at (0,3.0) (x) ;
at (2.8,1.0) (ba)
        [2em];
at (3.8,1.0) (bb)
        [2em];
at (0,2.4) (v1) ;
at (3.3,2.4) (v1a) [2em][2em];
[->] (v1) – (v1a);
at (0,1.8) (y) ;
at (1.6,1.8) (ya) [2em];
at (4.8,1.8) (yb) [2em];
[->] (y) – (ya);
[->] (1.9,1.8) – (3.4,1.3);
[->] (4.8,1.6) – (bb);
[->] (2.9,2.2) – (ya);
[->] (3.8,2.2) – (yb);
[->] (x) – (4.2,3.0) – (yb);
at (0,0.1) (bot) ;






The need to be conservative with the sharing of mutable parameters
in the analysis of function definitions (the special treatment in
) is illustrated by the example below.  Consider the
initial state, with variables  and  which share
with  and , respectively.  After  is
called  and  share, even though the parameters
 and  do not share at any point in the execution
of .  If mutable parameters were not treated specially in
the  case,  would be accepted as the
postcondition of  and the analysis of the call to 
would then be incorrect.  The sharing is introduced between memory cells
that were once shared with  and others that were once shared
with .  Thus in our algorithm, the sharing
of mutable parameters reflects all memory cells that are reachable from
the parameters during the execution of the function.  Where the mutable
parameters are assigned in , the sharing of the parameters'
previous values ( and ) is retained.
Thus when the final assignment is processed, sharing between the
parameters is added and this must be included in the postcondition.
Although this assignment does not modify  or , the
“!” annotations are necessary and alert the reader to potential
modification of variables that shared with the parameters when the
function was called.

[c]0.5

[scale=0.9]
at (2.2,4.3) (l1) Initial state;
at (0,3.0) (v1) ;
at (1.8,3.0) (v1a)
        [2em];
at (3.2,3.0) (v1b)
        [2em];
at (4.6,3.0) (v1c)
        [2em];
[->] (v1) – (v1a);
[->] (3.5,3.0) – (v1c);
[->] (2.1,3.0) – (v1b);
at (0,1.2) (v2) ;
at (1.8,1.2) (v2a)
        [2em];
at (3.2,1.2) (v2b)
        [2em];
at (4.6,1.2) (v2c)
        [2em];
[->] (v2) – (v2a);
[->] (3.5,1.2) – (v2c);
[->] (2.1,1.2) – (v2b);
at (0,2.4) (x) ;
[->] (x) – (1.8,2.4) – (v1b);
at (0,1.8) (y) ;
[->] (y) – (1.8,1.8) – (v2b);
at (0,0.1) (bot) ;



[c]0.5

[scale=0.9]
at (2.2,4.3) (l1) After ;
at (0,3.0) (v1) ;
at (1.8,3.0) (v1a)
        [2em];
at (3.2,3.0) (v1b)
        [2em];
at (4.6,3.0) (v1c)
        [2em];
[->] (v1) – (v1a);
[->] (3.5,3.0) – (v2c);
at (3.2,3.8) (n1b)
        [2em];
at (4.6,3.8) (n1c)
        [2em];
[->] (2.1,3.0) – (n1b);
[->] (3.5,3.8) – (n1c);
at (0,1.2) (v2) ;
at (1.8,1.2) (v2a)
        [2em];
at (3.2,1.2) (v2b)
        [2em];
at (4.6,1.2) (v2c)
        [2em];
[->] (v2) – (v2a);
[->] (3.5,1.2) – (v2c);
at (3.2,0.4) (n2b)
        [2em];
at (4.6,0.4) (n2c)
        [2em];
[->] (2.1,1.2) – (n2b);
[->] (3.5,0.4) – (n2c);
at (0,2.4) (x) ;
[->] (x) – (1.8,2.4) – (v1b);
at (0,1.8) (y) ;
[->] (y) – (1.8,1.8) – (v2b);
at (0,0.1) (bot) ;




[4]



mmm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄m ∅

(p_1,s_1),…(p_N,s_N
	

  

  
    {{𝚟.c_1,v_2.c_2}|{𝚟.c_1,v_2.c_2}∈𝚊0} 

  

     ⋃_1≤ i≤
N𝚊𝚕𝚒𝚊𝚜𝙲𝚊𝚜𝚎  𝚊0  𝚘𝚕𝚍  𝚟  p_i s_i 



mmm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mv_1,… v_N
	

  

  𝚊𝚟𝚍𝚌
	{{𝚏𝚌(𝚟.(𝚍𝚌.i:c_1)),
	w.c_2}|{𝚏𝚌(𝚟.(𝚍𝚌.i:c_1)),w.c_2}∈𝚊𝚟} 

  𝚛𝚜𝚎𝚕𝚏
    {{v_i.[𝚁𝚎𝚏.1],v_i.[𝚁𝚎𝚏.1]}| 1≤ i≤ N} 

  𝚟𝚒𝚜𝚑𝚊𝚛𝚎
    {{𝚏𝚌 (v_i.(𝚁𝚎𝚏.1:c_1)),
		𝚏𝚌 (v_j.(𝚁𝚎𝚏.1:c_2))}|

 {𝚏𝚌(𝚟.(𝚍𝚌.i:c_1)),𝚏𝚌(𝚟.(𝚍𝚌.j:c_2))}∈𝚊𝚟} 

  𝚜𝚑𝚊𝚛𝚎
    {{𝚏𝚌 (v_i.(𝚁𝚎𝚏.1:c_1)),
		w.c_2}|{𝚏𝚌(𝚟.(𝚍𝚌.i:c_1)),w.c_2))}∈𝚊𝚟} 

  

   (
	𝚛𝚜𝚎𝚕𝚏∪𝚟𝚒𝚜𝚑𝚊𝚛𝚎∪𝚜𝚑𝚊𝚛𝚎∪
	(∖)
	∪
)




For a case expression we return the union of the alias sets obtained for
each of the different branches.  For each branch we only keep sharing
information for the variable we are switching on that is compatible
with the data constructor in that branch (we remove all the old sharing,
, and add the compatible sharing, ).
We implicitly use the inverse of .  To deal
with individual data constructors we consider pairs of components of
arguments i and j which may alias in order to compute possible
sharing between v_i and v_j, including self-aliases when i=j.
The corresponding component of v_i (prepended with  and
folded) may alias the component of v_j.  For example, if 
of type  is matched with  and
 self-aliases, we need to find the components which fold
to  ( and ) in order
to compute the sharing for  and .  Thus we compute
that ,
may alias . This can occur if the
data structure is cyclic, such as the example below where  is
a list containing a single tree with 2 in the node and  as the
children (hence it represents a single infinite branch).  Note that
 represents both the memory cell
containing the  pointer and the cell containing .


[scale=1.0]
at (3.5,3.7) (c2)
        [4em][4em];
at (2.8,3.5) (c2a) ;
at (0,2.7) (d1) ;
at (3.5,2.7) (d2)
        [4em][4em];
at (2.8,2.7) (d2a) ;
[->] (d1) – (d2);
at (0,1.9) (e1) ;
at (0.7,1.9) (e1a) ;
at (2.5,2.4) (e1b) ;
[->] (e1a) – (e1b);
at (0,1.2) (f1) ;
at (2.8,1.2) (f2a) ;
[->] (0.8,1.2) – (3.9,2.4);
[->] (4.1,3.6) – (3.0,3.0);
at (2.8,1.4) (f2c) ;
[->] (d2a) – (c2a);





mmm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄mm̄m

  

  

 


Type instantiation is dealt with in the same way as variable equality,
with the additional check that if any sharing is introduced, the variable
with the more general type is not implicitly updated later while still
live (it is sufficient to check there is no “” annotation
attached to a later statement).




§ EXAMPLE



We now show how this sharing analysis algorithm is applied to the binary
search tree code given earlier.  We give a core Pawns version of each
function and the alias set before and after
each statement, plus an additional set at the end which is the union of
the pre- and post-conditions of the function.  To save space, we write
the alias set as a set of sets where each inner set represents all sets
containing exactly two of its members.  Thus {{a,b,c}} represents a
set of six alias pairs: aliasing between all pairs of elements, including
self-aliases.  The return value is given by variable 
and variables  and  are the versions of
 for type  and , respectively.



We start with the precondition:
a_0 = {{},
{}}.
Binding to a constant introduces no sharing so a_1 = a_0.
a_2 = a_1 ∪ {}.
The function call has precondition a_0 ∪{{},
{}}, which is a superset of a_2.
Since  is a mutable argument the
precondition sharing for  is added:
a_3 = a_2 ∪ {{ }}.
The final sharing includes the return variable, :
a_4 = a_3 ∪ {{},
{}}.  After removing sharing
for the dead (local) variable  we obtain
a subset of the union of the pre- and post-conditions,
which is
a_0 ∪{{},
{, }}.



We start with the precondition,
a_0 = {{}, {},
{},
{}}.
The  branch of the case introduces sharing for  and
:
a_1 = a_0 ∪ {{, ,
, },
{ , }}.
The list elements are atomic so a_2 = a_1.
The next binding makes the sharing of  and  the
same:
a_3 = a_2 ∪ {{ ,
,
},
{ , , ,
}}.
This can be simplified by removing the dead variables  and
.
The precondition of the calls are satisfied and
a_6 = a_5 = a_4 = a_3.
For the  branch we remove the incompatible sharing for
 from a_0:
a_7 = {{}, {},
{},
{}}
and a_8 = a_7.  Finally, a_9 = a_6
∪ a_8. This contains all the sharing for mutable parameter  and,
ignoring local variables, is a
subset of the union of the pre- and post-conditions, a_0.



Here a_0 = {{},
{}} and
a_1 = a_0 ∪{{, }, 
{, }}.
For the  branch we remove the  sharing so a_4 =
a_3 = a_2 = a_0 and a_5 = a_4 ∪{{},
{}}.
After the destructive update, a_6 = a_5 ∪{{,
}, 
{,
}} ( is dead and can be
removed) and a_7 = a_6.
For the  branch we have a_8 = a_1 ∪{{, , ,
},
{, ,
, , }}.
The same set is retained for a_9 … a_17 (assuming the dead
variable  is retained), the preconditions
of the function calls are satisfied and the required annotations are
present.  Finally, a_18 = a_17∪
a_7, which contains all the sharing for ,
and after eliminating local variables we get the postcondition,
which is the same as the precondition.



§ DISCUSSION



Imprecision in the analysis of mutable parameters could potentially be
reduced by allowing the user to declare that only certain parts of a
data structure are mutable, as suggested in <cit.>.
It is inevitable we lose some precision with recursion in types, but
it seems that some loss of precision could be avoided relatively easily.
The use of the empty path to represent sub-components of recursive
types results in imprecision when references are created.  For example,
the analysis of  concludes that the empty
component of  may alias with itself and the 
component of  (in reality,  has no sharing). Instead
of the empty path, a dummy path of length one could be used.
Flagging data structures which are known to be acyclic could also
improve precision for .  A more
aggressive approach would be to unfold the recursion an extra level, at
least for some types.  This could allow us to express (non-)sharing of
separate subtrees and whether data structures are cyclic, at the cost
of more variable components, more complex pre- and post-conditions and
more complex analysis for  and .

Increasing the number of variable components also decreases efficiency.
The algorithmic complexity is affected by the representation of alias
sets.  Currently we use a naive implementation, using just ordered
pairs of variable components as the set elements and a set library
which uses an ordered binary tree.  The size of the set can be O(N^2),
where N is the maximum number of live variable components of the same
type at any program point (each such variable component can alias with
all the others).  In typical code the number of live variables at any
point is not particularly large.  If the size of alias sets does become
problematic, a more refined set representation could be used, such as the
set of sets of pairs representation we used in Section <ref>,
where sets of components that all alias with each other are optimised.
There are also simpler opportunities for efficiency gains, such as
avoiding sharing analysis for entirely pure code.
We have not stress tested our implementation or run substantial
benchmarks as it is intended to be a
prototype, but performance has been encouraging.
Translating the tree insertion code plus a test harness to C, which
includes the sharing analysis, takes less time than compiling
the resulting C code using GCC.  Total compilation time is less than half
that of GHC for equivalent Haskell code and less than one tenth that of
MLton for equivalent ML code.  The Pawns executable is around 3–4 times
as fast as the others.





§ RELATED WORK



Related programming languages are discussed in <cit.>; here we
restrict attention to work related to the sharing analysis algorithm.
The most closely related work is that done in the compiler for
Mars <cit.>, which extends similar work done for Mercury
<cit.> and earlier for Prolog <cit.>.  All use a
similar abstract domain based on the type folding method first proposed
in <cit.>.  Our abstract domain is somewhat more precise due
to inclusion of self-aliasing, and we have no sharing for constants.
In Mars it is assumed that constants other than numbers can share.
Thus for code such as  our analysis concludes
there is no sharing between  and  whereas the Mars
analysis concludes there may be sharing.

One important distinction is that in Pawns sharing (and mutability) is
declared in type signatures of functions so the Pawns compiler just has to
check the declarations are consistent, rather than infer all sharing from
the code.  However, it does have the added complication of destructive
update.  As well as having to deal with the assignment primitive, it
complicates handling of function calls and case statements (the latter
due to the potential for cyclic structures).
Mars, Mercury and Prolog are essentially declarative languages.
Although Mars has assignment statements the semantics is that values are
copied rather than destructively updated — the variable being assigned
is modified but other variables remain unchanged.  Sharing analysis
is used in these languages to make the implementation more efficient.
For example, the Mars compiler can often emit code to destructively update
rather than copy a data structure because sharing analysis reveals no
other live variables share it.  In Mercury and Prolog the analysis can
reveal when heap-allocated data is no longer used, so the code can reuse
or reclaim it directly instead of invoking a garbage collector.

These sharing inference systems use an explicit graph representation
of the sharing behaviour of each segment of code.  For example, code
s_1 may cause aliasing between (a component of) variables  and
 (which is represented as an edge between nodes 
and ) and between  and  and code s_2 may
cause aliasing between  and  and between  and
.  To compute the sharing for the sequence s_1s_2
they use the “alternating closure” of the sharing for s_1 and s_2,
which constructs paths with edges alternating from s_1 and s_2, for
example  (from s_1),  (from s_2), 
(from s_1) and  (from s_2).

The sharing behaviour of functions in Pawns is represented explicitly,
by a pre- and post-condition and set of mutable arguments but there is
no explicit representation for sharing of statements.  The (curried)
function  represents the sharing behaviour of 
and the sharing behaviour of a sequence of statements is represented by
the composition of functions.  This representation has the advantage
that the function can easily use information about the current sharing,
including self-aliases, and remove some if appropriate.
For example, in the  branch of
the case in the code below the sharing for  is removed and
we can conclude the returned value does not share with the argument.




There is also substantial work on sharing analysis for logic programming
languages using other abstract domains, notably the set-sharing domain
of <cit.> (a set of sets of variables), generally with various
enhancements — see <cit.> for a good summary and evaluation.
Applications include avoiding the “occurs check” in unification
<cit.> and exploiting parallelism of independent sub-computations
<cit.>.  These approaches are aimed at identifying sharing of logic
variables rather than sharing of data structures.  For example, although
the two Prolog goals  and  share ,
they are considered independent if  is instantiated to a data
structure that is ground (contains no logic variables).  Ground data
structures in Prolog are read-only and cause no problem for parallelism
or the occurs check, whether they are shared or not.
The set-sharing domain is often augmented with extra information related
to freeness (free means uninstantiated), linearity (linear means
there are no repeated occurrences of any variable)
and/or groundness <cit.>.  In Pawns there are no logic variables
but data structures are mutable, hence their sharing is important.

However, the set-sharing domain (with enhancements) has been adapted
to analysis of sharing of data structures in object oriented languages
such as Java <cit.>.  One important distinction is that Pawns
directly
supports algebraic data types which allow a “sum of products”: there
can be a choice of several data constructors (a sum), where each one
consists of several values as arguments (a product).  In Java and most
other imperative and object oriented languages additional coding is
generally required to support such data types.  Products are
supported by objects containing several values but the only choice
(sum) supported directly
is whether the object is null or not.  Java objects and pointers
in most imperative languages are similar to a  algebraic
data type, with  corresponding to null.  A 
cannot be null.  The abstract domain of <cit.> uses set-sharing
plus additional information about what objects are definitely not null.
For Pawns code that uses s this information is given
by the data type — the more expressive types allow us to trivially
infer some information that is obscured in other languages.  For code
that uses , our domain can express the fact that a
variable is definitely  by not having a self-alias of
the  component.  The rich structural information in our
domain fits particularly well with algebraic data types.
There are also other approaches to and
uses of alias analysis for imperative languages, such as <cit.>
and <cit.>, but these are not aimed at precisely capturing
information about dynamically allocated data.  A more detailed discussion
of such approaches is given in <cit.>.



§ CONCLUSION



Purely declarative languages have the advantage of avoiding side effects,
such as destructive update of function arguments. This makes it easier
to combine program components, but some algorithms are hard to code
efficiently without flexible use of destructive update.  A function can
behave in a purely declarative way if destructive update is allowed,
but restricted to data structures that are created inside the function.
The Pawns language uses this idea to support flexible destructive update
encapsulated in a declarative interface.  It is designed to make all
side effects “obvious” from the source code.  Because there can be
sharing between the representations of different arguments of a function,
local variables and the value returned, sharing analysis is an essential
component of the compiler.  It is also used to ensure
“preservation” of types in computations.
Sharing analysis has been used in other
languages to improve efficiency and to give some feedback to programmers
but we use it to support important features of the programming language.

The algorithm operates on (heap allocated) algebraic data types,
including arrays and closures.  In common with other sharing analysis
used in declarative languages it supports binding of variables,
construction and deconstruction (combined with selection or “case”)
and function/procedure calls.  In addition, it supports explicit pointers,
destructive update via pointers, creation and application of closures and
pre- and post-conditions concerning sharing attached to type signatures
of functions.  It also uses an abstract domain with additional features
to improve precision.
Early indications are that the performance is acceptable: compared with
other compilers for declarative languages, the prototype
Pawns compiler supports encapsulated destructive update, is fast and
produces fast executables.



§ ACKNOWLEDGEMENTS

Feedback from reviewers, particularly Gianluca Amato, was very
helpful in ironing out some important bugs in the algorithm and
improving the presentation of this paper.


