Master 2 Internship Report - MPRI
20 March 2017 - 4 August 2017

Safe Pointers in SPARK 2014.

_Author:_

Georges-Axel Jaloyan

_Supervisor:_
Dr. Yannick Moy

AdaCore

École normale supérieure

21 August 2017

### The general context

This report is referring to an internship from the 20th of March 2017 to the
4th of August 2017 at _AdaCore_ located in Paris, France. AdaCore is a company
providing commercial software solutions for Ada, a language targeting safety-
critical applications. More specifically, SPARK Pro [12, 1, 2] is a static
analysis tool-suite using formal methods to deductively verify a subset of Ada
(called SPARK), commercialized in partnership with Altran. The tool can be
used to meet DO-178B/C (and the Formal Methods supplement DO-333), CENELEC
50128, IEC 61508, and DEFSTAN 00-56 standards. Its latest revision is called
SPARK 2014.

Deductive verification uses SMT solvers (CVC4, Z3, Alt-Ergo) and interactive
theorem provers (Coq and Isabelle) to check the validity of logical
propositions (called _verification conditions_) generated from the source code
and the specification. Those proofs are enough to give a strong guarantee that
the program meets its specification.

The tool is mainly based on Why3[6], an auto-active verification platform
using an intermediate language, WhyML, that uses deductive verification
techniques to prove user-specified properties (expressed as contracts in SPARK
code) or other automatically generated properties such as _absence of run-time
errors_ (AoRTE). The main limitation in SPARK 2014 is the absence of Ada
pointers (called _access types_ in Ada111A more precise definition is given in
Ada Reference Manual, section 3.10 [4].), which may require some complex
workarounds and code refactoring to make them accepted by SPARK Pro.

### The research problem

The main problem in adding access types to SPARK is to control aliasing (when
multiple pointers point to the same object in memory). This heavily
complicates proofs, and generally involves human-written annotations.222This
is the case for example with separation logic[16]. Cyclone and Rust are
examples of languages that control aliasing using compile-time restrictions
but none of them allows to prove programs.

SPARK already allows to control aliasing between ”references” (implicit
pointers created by the compiler for parameter passing), but not arbitrary
pointers. To the best of our knowledge, the proposed method in this report is
a novel approach for controlling aliasing introduced by arbitrary pointers in
a programming language supported by proof. Previous attempts have relied on a
combination of access policy enforced by proof mechanisms (like the so-called
Boogie methodology in Spec#). Our approach does not require user annotations
or proof of verification conditions, which makes it much simpler to adopt.

The aim of the internship is to design and implement an aliasing control
mechanism that would allow using pointers in SPARK. Such a design needs to be
(almost) fully automatic, to do not impact existing proofs of programs without
pointers, and should be expressive enough so that existing code (such as the
libraries of drivers and containers developed at AdaCore) could be verified
using SPARK. Some mathematical guarantees have to be given on the new design,
and its implementation should be tested against a large existing code-base in
SPARK and Ada.

### Your contribution

The main scientific contributions of this report are the following: the design
of rules for access types in SPARK, inspired by Rust’s _borrow-checker_ and
_affine typing_ , enforcing _Concurrent Read, Exclusive Write_ (_CREW_) and an
intra-procedural move semantics. We also present an implementation in Ada’s
compiler (called _GNAT_) front-end as a static analysis pass. Then we
formalize these rules on a subset of SPARK and give a proof of non-aliasing,
as done for a subset of Rust in [14] and [15]. Finally, we study these new
rules on existing code-base and examples, in order to check for their
applicability for real software, and compare them to Rust on some idiomatic
constructs.

### Arguments supporting its validity

The rules established by the author were validated at several levels. The
Language Design Committee of Ada/SPARK, an international board of experts in
Ada, validated the rules as a standard feature for a future version of SPARK
(most likely SPARK Pro 19). Comparison with Rust showed a great improvement on
aliasing control at the expense of not handling automatic reclamation and non-
null pointer coercion, being both checked by other passes in SPARK Pro.

Tests on industrial Ada code containing pointers (Ada drivers library, big
strings containers library) showed that this analysis only requires minor
changes to the code in order for it to be accepted in SPARK Pro.

### Summary and future work

First future step would consist in extending SPARK tool-chain to have its flow
analysis and proof mechanisms compatible with the new pointers added. Indeed,
during the internship, only the anti-aliasing rules have been implemented,
whereas the remaining part of the SPARK back-end needs modifications to
analyze SPARK code containing pointers. For this purpose, a post-doc has been
hired by AdaCore to work on those issues.

Next steps would consist in finalizing the implementation on corner-cases of
SPARK, and presenting the results at an international scientific conference. A
more general adoption of those rules by different customers as well as the
generalization of non-aliasing proofs to the complete SPARK language is
expected. A good evolution could also be to formalize those proofs in an
interactive theorem prover (such as Coq or Isabelle) in order to have stronger
guarantees on the system.

This internship gives us a better understanding of borrow-checkers and the
kind of guarantees they should give, not only theoretically (formalization of
what is a borrow-checker, proof of soundness), but also in practice (what a
borrow-checker should exactly take care of, how to make it understandable to
users, how to integrate it with other tools for static analysis).

A good next question is the study of the constructs that can be implemented
using this borrow-checker. How to make the most of a borrow-checker in order
to improve parallelism, compiler optimizations, automatic reclamation?
Answering these questions could lead to useful applications when transferring
the borrow-checker to full Ada, providing it as an additional feature of the
language.

### Acknowledgment

This work is partly supported by the Joint Laboratory ProofInUse
(ANR-13-LAB3-0007) and project VECOLIB (ANR-14-CE28-0018) of the French
National Research Agency (ANR).

A number of people have provided input and advice; we particularly thank
Claire Dross (AdaCore), Tucker Taft (AdaCore), Raphaël Amiard (AdaCore), Steve
Baird (AdaCore), Claude Marché (Inria), Andrei Paskevich (LRI), Jean-
Christophe Filliâtre (LRI), Jacques-Henri Jourdan (MPI-SWS), Sylvain Dailler
(AdaCore), Clément Fumex (AdaCore).

###### Contents

  1. 1 Preliminaries
    1. 1.1 Ada
    2. 1.2 SPARK 2014
    3. 1.3 Proofs in presence of aliasing
    4. 1.4 Rust
    5. 1.5 Main objective
  2. 2 Access types in $\mu$SPARK
    1. 2.1 Definitions
    2. 2.2 Moving
    3. 2.3 Borrowing
    4. 2.4 Observing
    5. 2.5 Control structures
  3. 3 Proofs of safety
    1. 3.1 Grammar and syntax
    2. 3.2 Operational semantics
    3. 3.3 Permission rules
    4. 3.4 Correctness of permission rules with respect to the operational semantics
  4. 4 Implementation and results
    1. 4.1 Laziness of permission trees
    2. 4.2 Complete SPARK
    3. 4.3 Test suites
    4. 4.4 Some use cases
    5. 4.5 Comparison with Rust
  5. 5 Conclusion
  6. A References
  7. B Grammar for $\mu$SPARK
  8. C Additional conditions on $\mu$SPARK
  9. D Typing $\mu$SPARK
  10. E Permission rules for µSPARk
  11. F Theorems and proofs

##  1 Preliminaries

###  1.1 Ada

Ada is a general purpose language originally standardized in 1983 for the
Department of Defense as a safety-oriented language targeting safety-critical
systems. Its latest revision, Ada 2012 is defined by ISO/IEC 8652:2012. It
features strong typing, objects and packages for modularity, and concurrency
handling (Ravenscar profile being the best known[5]). A typical Ada program is
made of several packages that can contain declarations (functions, procedures,
packages, variables, and types declarations) or initialization code, that will
be executed when the package is loaded.

A lot of features are unique to Ada amongst programming languages for safety-
critical applications, in particular modes of parameters, that can be of mode
in, out or in-out.333We added the dash to in-out for readability purposes. An
in parameter can be read but not modified by the callee whereas an in-out
parameter can be read and modified, and out parameters can only be modified
(and are considered uninitialized), their values being sent back to the
caller.

The language has many features inherited from older versions, and its safety
concerns require it to have a well-defined semantics detailed in the _Ada
Reference Manual_ [4].

###  1.2 SPARK 2014

SPARK 2014 is a subset of Ada designed and suited for static analysis using
formal methods. SPARK 2014 features specification constructs allowing writing
pre and post conditions, assertions, invariants, data dependencies. A SPARK
program is either made of fully written SPARK code, or is a subset of an Ada
program where some subprograms or packages have been marked with a special
annotation called SPARK_Mode, which allows mixing SPARK and non-SPARK code.

The main restrictions with respect to full Ada are the absence of pointers and
aliasing (some checks are already done in SPARK to prevent aliasing between
parameters and globals) and concurrency handling (only _extended Ravenscar
profile_ [9] is allowed). We also require that objects must fulfill the
_Liskov Substitution Principle_ (LSP) [10], which prevents a more specialized
subclass to have its invariants violated by the methods of the parent class.
More specifically this forces the more specialized subclass to implement sub-
behaviors of the parent class with respect to contracts expressed on the
parent methods.

In this report, we study a small subset of SPARK enriched with pointers,
called $\mu$SPARK, the grammar of which is given in Appendix B. Each
$\mu$SPARK program consists of a single file that contains a main procedure.
Each procedure starts with a list of definitions (type, procedure or variable)
followed by a body. This body is a sequence of statements, typically
assignments, allocations, procedure calls, conditional statements. We abstract
out the condition of the if statement, considering it as a non-deterministic
branching.

###  1.3 Proofs in presence of aliasing

To illustrate how aliasing can cause problems with proofs, let us consider the
following function with two parameters, that increases each of them. The
contract that could be expected of such a function (written in C annotated
with ACSL contracts [13]), ensures that the two parameters have their value
increased by one at the end of the function.

⬇

/*@

requires \valid(x) && \valid(y);

ensures (*x == \old(*x)+1 && *y == \old(*y)+1 );

*/

void inc (int* x, int* y) {

*x++; *y++;

}

This contract is false in presence of aliasing. Indeed if x and y point to the
same variable, then the final value of each parameter would get increased by
two instead of one. In ACSL, it is possible to use a logic function to express
separation of sets of pointers by adding annotations specifying that two
pointers should be considered as non-aliased. The contract hence becomes as
following, which gets easily proved using the WP or Jessie plug-in of Frama-C
toolset

⬇

/*@

requires \valid(x) && \valid(y);

requires \separated(x,y);

ensures (*x == \old(*x)+1 && *y == \old(*y)+1 );

*/

###  1.4 Rust

Rust is a new programming language created by Mozilla Foundation [11] and
intended for system programming. It focuses mainly on memory safety, with the
help of a powerful mechanism called a _borrow-checker_ , that prevents non-
safe aliasing through pointer analysis with techniques inspired by affine
types (in which resources can be used at most once) [8, 17].

The borrow-checker analyzes the source code looking for two different
constructs: moves and borrows.

Moves happen at the right-hand side of assignments as well as when passing
parameters to functions that are not borrowed (see after). Resources that are
moved are consumed (exactly as in affine types), which allows only a single
path to read or modify resources at a time.

Borrows are temporary grants of a given resource to another path, that can be
either _immutable_ (read-only, using the symbol &) or _mutable_ (read-write,
using the symbol &mut). The borrow checker verifies that when grants are
given, the CREW principle is respected, raising errors at each violation. As
an example, let us consider the following code which borrows mutably twice the
same path, triggering an error.

⬇

let mut r = String::from("hello");

let mut s = r; // move r to s

let mut s2 = r; // error: use of moved value: ‘r‘

let r1 = &mut s; // mutable borrow of s

let r2 = &mut s; // error[E0499]: cannot borrow ‘s‘ as mutable more than once

Rust’s borrow-checker also checks the lifetimes of pointers to make sure that
no dangling pointer is used, and to provide a compile-time garbage collector.

###  1.5 Main objective

The goal of this internship is to design a mechanism that controls aliasing in
SPARK, based on enforcing _CREW_. We use a model in which a syntactical
element has (full or partial) ownership of all data that is accessible from it
(e.g. a pointer owns the data pointed by it, …).

The CREW mechanism must ensure that two aliased paths do not have full
ownership of the underlying data. More specifically, either one path has the
full ownership (read-write) and the others have no ownership at all, or all of
them have at most partial ownership (read-only).

##  2 Access types in $\mu$SPARK

Three mechanisms have been created to ensure aliasing control, named
respectively move, borrow and observe. The first one consists in checking
assignments, whereas the two others focus on subprogram calls. We present the
aliasing rules for $\mu$SPARK, while explaining the main differences when
passing to complete SPARK in section 4.2.

###  2.1 Definitions

We define _paths_ as abstractions of left values (called _names_ in Ada). More
precisely, a path is a name in which all array indices have been abstracted
and all dereferences (or equivalently _indirections_) are made explicit.444Ada
has implicit pointer dereference. In the case of $\mu$SPARK, names and paths
are the same, given that implicit dereference as well as arrays are excluded
from the language. Note that in Ada, dereferences are written using the .all
selector.

By introducing the notion of prefixes and extensions of paths, we can use
trees to represent a set of paths, as shown in Figure 1. This tree is defined
as the following. Each node represents a path, with the root being the base
identifier. Those nodes can be of three different types: either an Integer
node (such as My_Var.all.z), a Pointer node (such as My_Var or My_Var.all.y),
or a Record node (such as My_Var.all).

Figure 1: Example of a tree representing the following paths: My_Var,
My_Var.all, My_Var.all.x, My_Var.all.y, My_Var.all.z, My_Var.all.y.all.

We will focus our analysis on types that can cause aliasing problems during
assignment or parameter passing, that we call _deep_ , that are intuitively
pointers and records having at least one deep type component. Formally, a type
is said to be _deep_ if it is a type having an access part.555See Ada
Reference Manual, section 3.2.(6/2). Types that are not deep are called
_shallow_.

####  2.1.1 Reading and writing a path

Let us consider a path (example My_Var.all). Our memory model gives to this
path the ownership of all its extensions (hence all the subtree that is rooted
at My_Var.all).

When reading this path (for example at a the right-hand side of an
assignment), every extension of this path is read (i.e. My_Var.all,
My_Var.all.x, My_Var.all.y, My_Var.all.y.all, My_Var.all.z).

Symmetrically, when writing this path (left-hand side of an assignment), only
extensions that have the same number of dereferences are written (My_Var.all,
My_Var.all.x, My_Var.all.y, My_Var.all.z but not My_Var.all.y.all). Every
pointer accessible from the path gets smashed (My_Var.all.y), hence the memory
areas designated by those pointers are replaced by new areas instead of being
written.

This asymmetry is fundamental when considering the rules for non-aliasing.
Reading follows the pointers underlying a data structure whereas writing is
stopped at those pointers, that get smashed instead.

####  2.1.2 Permissions

RWRWNO Figure 2: Hasse diagram for the permission lattice.

To explicitly control aliasing, we must restrict the readability and
writability of some paths to ensure that only one path can write a given
memory area at a time. For this, we add explicitly permissions on the previous
trees, that can be of four different values: RW (read-write), W (write-only),
R (read-only), NO (no permission). Those permissions form a lattice, whose
Hasse diagram is given in Figure 2.

Those trees enriched with permissions are called _permission trees_ , and
their formal definition is given is Appendix E. Note that those trees are of
infinite depth when a structure has a component of type access to itself
(linked lists, graphs, …).

###  2.2 Moving

Moving is a mechanism that transfers ownership from one or more paths (called
the _moved paths_ , the right-hand side) to another path (the _assigned path_
, the left-hand side).

In order to find all the paths present in the right-hand side that are
considered as moved, we first define the concept of _moved expression_ , and
then gather from those expressions every path on which we check the adequate
permissions and update them accordingly. Finally, we update the permission of
the assigned path.

More formally, an expression appearing in the right-hand side of an assignment
statement is a _moved expression_ when:

  * •

It is a deep type top-level expression (i.e. expressions that are not part of
other expressions).

  * •

It is the prefix of an Access attribute (equivalent to & “address-of” unary
operator in C) of a moved expression.666This prefix is necessarily a name per
Ada rules.

  * •

It is a deep type direct sub-expression of a moved expression.

When a moved expression is a name, then this yields directly a moved path. We
process each moved path sequentially by checking first its Read-Write
permission, and then deleting both read and write permission to any path that
gets aliased with the assigned path. Using our tree representation, one could
remark that when a path (ie. node) is aliased, then all the subtree rooted at
that node is also aliased. Hence we can directly consider aliases of trees.

(a) Example of a tree with its permissions updated after the path My_Var.all.y
has been moved with Access attribute. The aliased subtree is framed in green.

(b) Example of a tree with its permissions updated after the path My_Var.all.y
has been moved without Access attribute. The aliased subtree is framed in
green.

(c) The previous tree (Figure 3(b)) after assigning My_Var.all.y. A further
propagation will give RW permission to My_Var.all and My_Var.

If the path is yielded from the prefix of an Access attribute, then the whole
subtree is aliased. Hence, the whole subtree sees its permission changed to
NO, as well as any ancestor node (prefix) of this path that have the same
number of indirections. All other ancestors only lose their readability and
get their permission updated to W.777The exact wording as appearing in the
SPARK RM says: “After moving a path under ‘Access attribute, the permission
for the path, any of its extensions, and any strict prefix that contains the
same number of .all becomes NO permission. Any strict prefix that does not
contain the same number of .all becomes write-only.”

In the other case, any subtree that has more indirections than the moved path
is aliased. Hence those subtrees have their permission changed to NO, while
all other nodes of the moved tree only lose their readability. Similarly, all
ancestors have their permission set to W.888The exact wording as appearing in
the SPARK RM says: “After moving a path without an ‘Access attribute, the path
and any of its prefixes becomes write-only. Any shallow extension of the path
that has the same number of .all stays read-write. Any deep extension of the
path that has the same number of .all becomes write-only. Any extension of the
path that has not the same number of .all becomes NO permission.”

Finally, the assigned path is checked to have either W or RW permission. The
assigned path and any of its extensions get RW permission. We then propagate
this update to prefixes by increasing their permission with the greatest lower
bound of the permissions of their descendants. More details on this
propagation are given in Appendix E, which defines the PermRelease operator.

###  2.3 Borrowing

Borrowing consists in a temporary transfer of ownership of a path from a
caller to a callee. They happen only during subprogram call statements. A
parameter is said to be borrowed when it is a name of mode in-out or
out,999Only names can be sent to procedures with mode in-out or out. or of
mode in and of type access-to-variable.101010See Ada RM, section 3.10.(8) and
3.10.(10) [4].

The last condition allows sending pointers with mode in, and modifying their
referenced value while preventing any modification to the pointer. Ada
provides a modifier constant that forbids any modification to the referenced
value, and can be used in order send pointers with mode in without granting
the permission to write on those values.

Intuitively, borrows can be seen as moving the borrowed path (actual
parameter) with an Access attribute to the formal parameter, and then moving
back the formal parameter to the actual. However, given that mode in
parameters are not necessarily names, this complicates handling the borrows of
such parameters, the details being explained in section 3.2.

The formal definition of a borrowed expression is similar to move, except that
we do not require the top level expression to be deep for modes in-out or out
(which coincides well with enclosing the top-level expression in a Access
attribute). Hence, an expression in a procedure call is said to be borrowed
if:

  * •

It is an in actual parameter of a procedure and is of type access-to-variable.

  * •

It is an in-out or out actual parameter to a procedure.

  * •

It is the prefix of an Access attribute of a borrowed expression.

  * •

It is a deep type direct subexpression of a borrowed expression.

After gathering the borrowed paths, we check sequentially that they have RW
permission (or at least W for out parameters), and then set any prefix or
extension to NO for the whole duration of the call if it is of deep type, R if
shallow (so that its value can be used in other arguments without being passed
to the callee). At the end of the call, every borrowed path has its permission
updated to RW, and as for assigns, we propagate this update to the prefixes of
those paths.

In the callee, any borrowed formal parameter of a procedure with mode in or
in-out has RW permission, as well as any of its extensions. Any borrowed
formal parameter of a procedure with mode out has W permission, as well as any
of its extensions. We also require that at the end of the subprogram, every
borrowed parameter should have permission RW, so that they could be moved back
to the caller.

###  2.4 Observing

Observing is the mechanism that creates read-only aliases for parameters of
mode in to subprograms. Formally any deep actual parameter of mode in that is
not of type access-to-variable is observed, as well as any deep subexpression
of an observed expression.

After gathering the observed paths, we check sequentially that they have at
least R permission and then set any prefix or extension to R for the whole
duration of the call. At the end of the call, every observed path has its
permission reverted to the one it had before the call.

In the callee, any observed formal parameter of a procedure, as well as any of
its extensions, have R permission.

###  2.5 Control structures

The previously given rules describe the evolution of permissions at the level
of one block of statements. They should be completed with others rules that
describe the checks done at different control structures available in SPARK,
namely loops and conditions (gotos and exceptions are not available in SPARK).
We only include conditions in $\mu$SPARK and exclude loops.

For conditions, we apply our rules on each block independently, yielding to
different environments, and then merge those by taking, for each path, the
greatest lower bound of its permission in the different environments.

For loops, we require permissions to get only less restrictive at the end of
the loop, when compared to the entry. This rule forbids moving the same
variable to a different element of an array at each iteration.

##  3 Proofs of safety

The section that follows provides a proof of the previously given anti-
aliasing rules for the $\mu$SPARK language. For this purpose, we first provide
a formalization of the $\mu$SPARK language with a grammar and typing rules,
then with an operational semantics, and finally a formalization of the
previously given rules on which we provide a proof of non-aliasing.

###  3.1 Grammar and syntax

We remind that a $\mu$SPARK program consists of a single procedure file
containing declarations and body. A declaration can either be a procedure, a
record type definition or an uninitialized variable declaration. The body
consists of a sequence of instructions, that can be assignment statements of
existing or freshly allocated values, procedure calls or if statements from
which the condition has been abstracted (non-deterministic choice).

Only integer and user-defined record types are available, as well as accesses
to existing types. Note that there are no loops, nor expression operators,
which make the language non Turing-complete.

The full details of the grammar are given in Appendix B.

###  3.2 Operational semantics

####  3.2.1 Memory trees

The operational semantics is based on a memory model that keeps some
relational information about the path leading to the designated memory area.
To each path, we associate a memory cell with its value. This leads to the
concept of _memory trees_ that are quite similar to permission trees with the
exception that those trees are finite, given that the access nodes can point
to null value. Hence, the _memory environment_ $\Upsilon$ is a mapping from
variable declarations to memory trees.

We decide not to represent the implementation of aggregate structures inside
the memory, supposed to be compiler-dependent. Thus we keep in our memory
trees only a mapping of fields to children subtrees, as if one memory cell is
enough for a structure to point to all its children. Indeed, without loss of
generality, we can always chose in $\mu$SPARK a word size big enough, so that
each memory cell contains arbitrarily many pointers.

Each memory tree is defined in the following way:

$\begin{array}[]{lcl}M&::=&Integer(Cell,Value)\\\
&|&Record(Cell,Fields\rightarrow M)\\\ &|&Access(Cell,M)\\\
&|&Access(Cell,Null)\\\ &&\\\ \end{array}$

####  3.2.2 Fresh(tau)

Formally, memory cells are elements of an arbitrary infinite set. We use the
word fresh to designate an oracle that gives a new element of the infinite set
(seen as an allocation of a machine word). This construct can be easily
generalized to allocate a whole tree representing a given type $\tau$, which
we call $\textit{fresh}(\tau)$. It takes a type $\tau$ as an input and
allocates the required memory areas for the type $\tau$ using the fresh
oracle, and initializes them with default value.

  * •

$\textit{fresh}(\texttt{integer})$ is equivalent to $Integer(\textit{fresh})$.

  * •

$\textit{fresh}(\texttt{access}~{}\tau)$ is equivalent to
$Access(\textit{fresh},Null)$.

  * •

$\textit{fresh}(R)$ is equivalent to $Record(\textit{fresh},\forall x:\tau\in
R~{}x\mapsto\textit{fresh}(\tau))$.

####  3.2.3 Assign

(a) The tree of the left hand side My_Var. The assigned part (My_Var.all) is a
structure containing three fields, a of type integer with value 42, b of type
pointer to NULL, and c of type integer with value 45.

(b) The right-hand side My_Struct. It is a structure containing three fields,
a of type integer with value 21, b of type pointer to an integer with value
42, and c of type integer with value 14.

(c) The left-hand side after assignment. Note that the values of each node is
updated without changing their addresses except for the indirected integer
node (address 0xA) that is added to the tree.

Figure 4: Example of the semantic rule (E-assignName) applied to the
assignment My_Var.all := My_Struct; Pointers are in green, structures in gold,
and values in purple.

The assignment of one subtree to a node is peculiar. Indeed, as in real
Ada/SPARK, the left-hand side does not get its memory address changed, only
its value. In our representation of the memory this would look like a (deep)
replacement of every value in $Integer$ nodes, as well as a replacement of the
subtree pointed by every $Access$ node.

This leads to the following definition of the recursive
$\textit{Assign}_{\Upsilon}(Node,Node)$ operator (the two parameters are of
same type):

  * •

$\textit{Assign}(Integer(C,\\_),Integer(\\_,V))=Integer(C,V)$

  * •

$\textit{Assign}(Access(C,\\_),Access(\\_,P))=Access(C,P)$

  * •

$\textit{Assign}(Record(C,(F_{i})_{i}),Record(\\_,(F^{\prime}_{i})_{i}))=Record(C,(\textit{Assign}(F_{i},F^{\prime}_{i}))_{i})$

For assignments, we copy the value of the left-hand side to the right-hand
side. In terms of semantics, this is done by copying the value of each field,
except for pointers where we copy the whole subtree in the indirection, as
shown in Figure 4.

####  3.2.4 Procedure calls

Another peculiarity happens at procedure calls, where we have to copy the
actual parameter into a fresh tree representing the formal parameter
(GetFromExpr, see below), run the semantics on the procedure definition
(yielding $\Upsilon^{\prime\prime}$), and then, depending on mode, copy back
its content to the actual parameter. This semantics follows the compiled code,
which pushes the parameters in the stack before call, jumps to the callee, and
then pops them while moving them to the appropriate registers if those
parameters are of mode out or in-out. This can be summarized by the rule
(E-call), whose definition can be found in section 3.2.5.

The formal definition of $\textit{GetFromExpr}_{\Upsilon}(e)$ is:

  * •

$\textit{GetFromExpr}_{\Upsilon}(\texttt{null})=Access(fresh,Null)$

  * •

$\textit{GetFromExpr}_{\Upsilon}(literal)=Integer(fresh)$

  * •

$\textit{GetFromExpr}_{\Upsilon}(n\texttt{'Access})=Access(fresh,\Upsilon(n))$

  * •

$\textit{GetFromExpr}_{\Upsilon}(n)=\Upsilon(n)$

We also use $SetFromExpr_{\Upsilon}(e_{i},x_{i})$ for updating borrowed
parameters with mode in (access-to-variable, note that mode in actual
parameters are not solely names, hence the expression needs to be decomposed):

  * •

$SetFromExpr_{\Upsilon}(\texttt{null},x_{i})$: no update

  * •

$SetFromExpr_{\Upsilon}(literal,x_{i})$: impossible case

  * •

$SetFromExpr_{\Upsilon}(n,x_{i})=Assign(n,\Upsilon(x_{i}))$

  * •

$SetFromExpr_{\Upsilon}(n\texttt{'Access},x_{i})=Assign(n,\Upsilon(x_{i}.all))$
(valid since formal parameters of mode in cannot be set to null in callee).

####  3.2.5 Semantics for statements

Every rule is in the form $\Upsilon.c\xRightarrow{}\Upsilon^{\prime}$, where
$c$ designates any construct of the language. We annotate each semantics rule
with s (statements) or d (declarations) for readability purposes.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x\texttt{:=
null}\xRightarrow{}_{s}\Upsilon[x.all\mapsto\texttt{Null}]\end{array}}$
(E-assignNull)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}n~{}\textnormal{name}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x\texttt{:=}~{}n\xRightarrow{}_{s}\Upsilon[Assign(x,\Upsilon(n))]\end{array}}$
(E-assignName)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Upsilon.~{}i_{1}\xRightarrow{}_{s}\Upsilon^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>* then}~{}i_{1}~{}\texttt{else}~{}i_{2}~{}\texttt{end
if}\xRightarrow{}_{s}\Upsilon^{\prime}\end{array}}$ (E-ifConditionTrue)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\quad\quad
e~{}\textnormal{literal}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x\texttt{:=}~{}e\xRightarrow{}_{s}\Upsilon[x.value\mapsto
e]\end{array}}$ (E-assignLiteral)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}n~{}\textnormal{name}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon,\Phi.~{}x\texttt{:=}~{}n\texttt{'Access}\xRightarrow{}_{s}\Upsilon[x.all\mapsto\Upsilon(n)]\end{array}}$
(E-assignAccess)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x\texttt{:=}~{}\texttt{new}~{}\tau\xRightarrow{}_{s}\Upsilon[x.all\mapsto\textit{fresh}(\tau)]\end{array}}$
(E-assignNew)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall
j>0,~{}\Upsilon_{j}.~{}i_{j}\xRightarrow{}_{s}\Upsilon_{j+1}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(E-block)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Upsilon.~{}i_{2}\xRightarrow{}_{s}\Upsilon^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>* then}~{}i_{1}~{}\texttt{else}~{}i_{2}~{}\texttt{end
if}\xRightarrow{}_{s}\Upsilon^{\prime}\end{array}}$ (E-ifConditionFalse)

$\displaystyle\frac{\begin{array}[]{<EMAIL_ADDRESS>mode {in}},\\\ e_{a+1}...e_{b}~{}\textnormal{with mode {in-out}},\\\
~{}e_{b+1}...e_{n}~{}\textnormal{with mode {out}},\\\
\Upsilon^{\prime}=\\{\forall~{}0<i\leq
n,x_{i}\mapsto\textit{GetFromExpr}_{\Upsilon}(e_{i})\\}\\\
\Upsilon^{\prime}.~{}\texttt{procedure}~{}P(x_{1},~{}...~{},x_{n})\xRightarrow{}_{d}\Upsilon^{\prime\prime}\\\
\Upsilon^{\prime\prime\prime}=\Upsilon[\forall~{}0<i\leq
a,\textit{SetFromExpr}_{\Upsilon^{\prime\prime}}(e_{i},x_{i})\\\
\forall~{}a<i\leq b,Assign(e_{i},\Upsilon^{\prime\prime}(x_{i}))\\\
\forall~{}b<i\leq
n,Assign(e_{i},\Upsilon^{\prime\prime}(x_{i}))]\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}P(e_{1},~{}...~{},e_{n})\xRightarrow{}_{s}\Upsilon^{\prime\prime\prime}\end{array}}$
(E-call)

####  3.2.6 Semantics for declarations

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x:\tau\xRightarrow{}_{d}\Upsilon[x\mapsto\textit{fresh}(\tau)]\end{array}}$
(E-uninitDecl)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Upsilon_{1}=\Upsilon\quad\quad\forall
k,\Upsilon_{k}.~{}d_{k}\xRightarrow{}_{d}\Upsilon_{k+1}\quad\quad\Upsilon_{m+1}.~{}i\xRightarrow{}_{d}\Upsilon^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}\texttt{procedure}~{}P(x_{1},...,x_{n})~{}\texttt{is}~{}d_{1},...,d_{m}~{}\texttt{begin}~{}i~{}\texttt{end}\xRightarrow{}_{d}\Upsilon^{\prime}\end{array}}$
(E-procedureDecl)

###  3.3 Permission rules

Similarly, the rules defined in section 2.1 are mathematically formalized,
with semantic-like rules that show the evolution of permission trees (defined
in section 2.1.2) depending on lexical elements of the language and the
mechanism used (borrowed, observed, moved). As for the semantics, we define
some constructs to “allocate”111111Technically, the trees are not allocated,
but only constructed by the Pfresh operator. (Pfresh), normalize
(PermRelease), merge (Fusion) permission trees.

As an example, the same assignment shown in Figure 4 would give the following
sequence using the rule (P-assignDeepName) (all of them can be found in
Appendix E). The whole derivation tree is presented hereafter, for better
readability.

The rule (P-assignDeepName) applied to the assignment My_Var.all := My_Struct
checks first that My_Var.all is indeed a well defined deep variable, and that
My_Struct is a indeed a name. The permission corresponding to the node
My_Struct is checked to be Read-Write (using the notation
$\Phi(\texttt{My\\_Struct})$). Then, we apply the rule (P-M-ident) on the
moved name My_Struct that modifies its permission to write-only. The next part
of the (P-assignDeepName) rule changes the permission of every extension of
the moved name by putting its strict deep extensions with more indirections to
NO permission (My_Struct.b.all), strict deep extensions with same number of
indirections of write-only (My_Struct.b), and the strict shallow extensions to
read-write (My_Struct.a, My_Struct.c).121212The Readability lemma shows that
if a node has read permission, then all its children have also read
permission. This gives as a corollary that read-write permissions follow the
same rule outside procedure calls. Without this lemma, the changes of
permission in the semantics should be interpreted as taking the least upper
bound of the given permission and the actual permission. This method is the
one implemented in Ada, being more generic.

Only after those changes, we check for write permission to the assigned name
(My_Var.all). This order is very important so as to check the safety of
assignments of variables to themselves and prevent creating cycles in data-
structures (such as assigning Tree.left.all := Tree). Finally, we change the
permissions of the assigned path to read-write, as well as every extension,
and propagate this update to its prefixes with the PermRelease operator that
normalizes the permission tree.

$\inferrule*[Right=(P-assignDeepName)]{\texttt{My\\_Var.all}:\texttt{S}~{}\textnormal{deep}\in\Gamma\quad\quad\Phi(\texttt{My\\_Struct})=\texttt{RW}\quad\quad\inferrule*[Right=(P-M-
ident)]{}{\Phi.~{}\texttt{My\\_Struct}\xrightarrow{Move}_{n}\Phi[\texttt{My\\_Struct}\rightarrow\texttt{W}]}\\\
\Phi^{\prime\prime}=\Phi[\texttt{My\\_Struct}\rightarrow\texttt{W}][\texttt{My\\_Struct.b.all}\mapsto\texttt{NO}\quad\quad\texttt{My\\_Struct.b}\mapsto\texttt{W}\\\
\texttt{My\\_Struct.a}\mapsto\texttt{RW}\quad\quad\texttt{My\\_Struct.c}\mapsto\texttt{RW}]\quad\quad\Phi^{\prime\prime}(\texttt{My\\_Var.all})=\texttt{W,RW}\quad\quad}{\Phi.~{}\texttt{My\\_Var.all}\texttt{:=}~{}\texttt{My\\_Struct}\xrightarrow{}_{s}\textit{PermRelease}(\Phi^{\prime\prime}[\texttt{My\\_Var.all},\\\
\texttt{My\\_Var.all.a},\texttt{My\\_Var.all.b},\texttt{My\\_Var.all.b.all},\texttt{My\\_Var.all.c}\mapsto\texttt{RW}])}$

The Figure 5 shows the two permission trees associated with My_Var and
My_Struct before and after the assignment My_Var.all := My_Struct. Given that
the situation is symmetrical, the modification in permissions admits as an
inverse the reverse assignment My_Struct := My_Var.all.

(a) The tree of the left hand side My_Var before assignment. The assigned part
(My_Var.all) is shown in green.

(b) The tree of the right hand side My_Struct before assignment.

(c) The tree of the left hand side My_Var after assignment. The PermRelease
operator changed the permission of My_Var to RW.

(d) The tree of the right hand side My_Struct after assignment.

Figure 5: Example of the permission rule (P-assignDeepName) applied to the
assignment My_Var.all := My_Struct;.

As for the operational semantics, the rule for procedure calls is also
special. Depending on each argument mode, we apply a different rule (either
Observe, BorrowIntOut or BorrowOut; the last differs from the previous by
accepting write-only permission to the borrowed actual parameter). Then for
every out or in-out parameter, they are set to read-write as well as all their
extensions, as for assignment. Note that all the changes in permissions during
call last only for the duration of the call.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\texttt{procedure}~{}P(x_{1}:\tau_{1},~{}...~{},x_{n}:\tau_{n})~{}\textnormal{with}{}\\\
x_{1}...x_{a}~{}\textnormal{observed},\\\
~{}x_{a+1}...x_{b}~{}\textnormal{borrowed with mode {in}},\\\
~{}x_{b+1}...x_{c}~{}\textnormal{borrowed with mode {in-out}},\\\
~{}x_{c+1}...x_{n}~{}\textnormal{borrowed with mode {out}},\\\
\Phi_{1}=\Phi\\\ \forall~{}0<i\leq
a,\Phi_{i}.~{}e_{i}\xrightarrow{Observe}_{e}\Phi_{i+1}\\\ \forall~{}a<i\leq
b,\Phi_{i}.~{}e_{i}\xrightarrow{BorrowInOut}_{e}\Phi_{i+1}\\\
\forall~{}b<i\leq
c,\Phi_{i}.~{}e_{i}\xrightarrow{BorrowInOut}_{e}\Phi_{i+1}\\\
\forall~{}c<i\leq n,\Phi_{i}.~{}e_{i}\xrightarrow{BorrowOut}_{e}\Phi_{i+1}\\\
\Phi^{\prime}=\textit{PermRelease}(\Phi[\forall~{}b<i\leq
n:e_{i}\mapsto\textit{Pfresh}(\tau_{i},\texttt{RW})])\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}P(e_{1},~{}...~{},e_{n})\xrightarrow{}_{s}\Phi^{\prime}\end{array}}$
(P-call)

###  3.4 Correctness of permission rules with respect to the operational
semantics

The anti-aliasing requirement enforces CREW. This means that if an aliased
memory node can be written (by assigning its associated path, or any prefix
with the same number of indirections), then any other aliased node can be
neither written nor read using another path.

The way we built our memory representation adds to each memory cell the path
used to access it, thanks to the tree representation. This allows tracking
aliasing very precisely, which is by definition the fact of accessing the same
memory cell using two different paths. This gives a straightforward
formalization of the main theorem.

######  Theorem 1.

(No-aliasing). For every set of nodes $S$ in memory environment $\Upsilon$
such that their memory cells have the same address, consider their associated
paths. If there is one path that can be written using the permission
environment $\Phi$, then all other paths in $S$ can neither be written nor
read.

####  3.4.1 Lemmas

Some lemmas are required, so as to prove that an associated path to a memory
node always exists. The solution for this is to compare memory and permission
trees, and find out that memory trees are a subset of permission trees. This
is the _coherence_ lemma, whose formalization is given hereafter.

There are other lemmas, used in the proofs, such as the fact that each
permission rule leaves the environment normalized (_Normalization_ lemma),
that if a node has permission read, then all its children nodes also have read
permission (_Readability_ lemma), and that the memory cannot loop on itself
(_No-cycle_ lemma).

######  Lemma 1.

(Normalization). Permission environment is normalized.

###### Proof.

Straightforward. Every rule of the semantics calls the normalization operator
PermRelease. The rules that do not call it are (P-block) (trivial case), and
declaration rules (they create only new trees with one node). ∎

######  Lemma 2.

(Coherence). For every node $n$ in the memory environment, it is possible to
find an associated node $n^{\prime}$ in the permission environment, such that
$n$ and $n^{\prime}$ designate the same path.

###### Proof.

Every permission rule manipulates permission trees that have the same
constructs as memory trees, except for access types that cannot be null. Hence
every memory tree can be obtained from a permission tree by cutting nodes at
access nodes when the pointer has null value. ∎

######  Lemma 3.

(Readability). If a node has permission R (resp. RW), then all its children
have permission R (resp. RW) at each step of the semantics.

###### Proof.

By induction on the semantics:

  1. 1.

(E-assignNull), (E-assignLiteral): $\textit{Pfresh}(\tau,\texttt{RW})$
guarantees it for the assigned path.

  2. 2.

(E-assignName), (E-assignAccess), (E-assignNew): same thing for the assigned
path. For the moved path, every prefix gets its permission set to either W or
NO by the (P-M-ident), (P-M-field), (P-M-deref) or (P-SM-ident), (P-SM-field),
(P-SM-deref) rules. The extensions are handled by (P-assignDeepName),
(P-assignShallowName), (P-assignAccess), and (P-assignNew).

  3. 3.

(E-call): we create such nodes by observing their paths. The rules (P-O-
nullValue), (P-O-litteral), (P-O-takeAccess), (P-O-name) guarantee that if any
node is set to permission R, then any extension of it is also set to R. After
the callee returned, the proof is identical to assignments.

  4. 4.

(E-block), (E-ifConditionTrue), (E-ifConditionFalse), (E-uninitDecl),
(E-procedureDecl): trivial

∎

######  Lemma 4.

(No-cycle). A node cannot have the same memory cell as any of its descendants
(hence memory trees are finite).

###### Proof.

By induction on the semantics:

  1. 1.

(E-assignNull), (E-assignLiteral), (E-assignNew): given that those rules only
cut memory trees, there are no new indirections created.

  2. 2.

(E-assignName): such a cycle could only be created when applying $Assign$ on a
node $Access(C1,\\_)$ which is a descendant of the node being moved
$Access(\\_,P)$. In such a case, this would contradict hypothesis of the rule
(P-assignDeepName), given that we set descendants of the moved node (ie strict
extensions) to NO, before checking RW for the node to assign.

  3. 3.

(E-assignAccess): such a cycle could only be created if the assigned $Access$
node is a descendant of the subtree we are taking address of. In such a case,
this would contradict hypothesis of the rule (P-assignAccess), given that we
set descendants of the moved node (ie strict extensions) to NO, before
checking RW for the node to assign.

  4. 4.

(E-call): borrows and observes do not modify addresses before transferring to
callee. After returning, we assign every parameter. Hence identical as
(E-assign) on each in-out or out parameter. For every in parameter,
SetFromExpr is equivalent to either assigning $n.all$ or $n$.

  5. 5.

(E-block), (E-procedureDecl): trivial by applying the induction hypothesis
successively to each statement of the block.

  6. 6.

(E-ifConditionTrue), (E-ifConditionFalse): the $Fusion$ operator does not
change memory places and pointers, only permissions.

  7. 7.

(E-uninitDecl): every node is assigned to a new memory area (and pointers to
null). Hence it is impossible to point to an existing memory area.

∎

####  3.4.2 No-aliasing proof

######  Theorem 1.

(No-aliasing). For every set of nodes $S$ in memory environment $\Upsilon$
such that their memory cells have the same address, consider their associated
paths. If there is one path that can be written using the permission
environment $\Phi$, then all other paths in $S$ can neither be written nor
read.

The main theorem is proved by induction on the operational semantic. This
leads us to consider each semantic rule one by one and show that the invariant
holds. As an example, let us consider the proof for (E-assignName) and
(E-call). The full proof is given in Appendix F.

##### (E-assignName)

Let us take any set $S$ in the environments $\Upsilon^{\prime},\Phi^{\prime}$
after executing one step of the semantics. Nodes can only get aliased between
the first Access node descendant of assigned and moved node (because values
are recursively copied, up to the first Access node encountered in which the
pointer is copied, which creates an alias).

We can consider only the case when the moved or assigned path $y$ is the one
that can be written. Indeed, by Readability, $y$ cannot be R in $\Phi$. Hence
it can only be NO, which leads to a contradiction. If $y$ cannot be written
nor read, then its permission is NO before executing the semantics. By
normalization of $\Phi$, we can say that the glb of its children is also NO
(and recursively). Which contradicts RW permission for $x$.

Executing one step of the semantics creates an alias in $x$ (the assigned
path) for every node of any subtree rooted under an $Access$ node that is a
direct descendant of $n$. However, the rule (P-assignDeepName) says that when
encountering an $Access$ node, all the further descendants are set to NO,
hence their paths cannot be written. The rules (P-M-ident), (P-M-field), (P-M-
deref) guarantee also that any extension of $n$ cannot be read anymore. This
solves the case for elements of $S$ that are descendant of $x$ with different
number of .all.

For elements of $S$ that are descendant of $x$ with same number of .all, no
alias is created during assignment, hence induction hypothesis can be applied
directly.

Hence, the assigned path gets RW permission (as well as any extensions), but
any aliased subtree of this node cannot be written nor read in the moved tree,
hence only one aliased path be written, and all others can neither be written
nor read.

##### (E-call)

The case for procedure calls is particular: indeed we apply our inductive
hypothesis after modifying environments, hence we have to guarantee that the
invariants not only hold at the end of the rule, but also at the moment we
transfer the control flow to the callee (ie for $\Upsilon^{\prime}$ in
(P-call) and $\Phi^{\prime}$ in (P-procedureDecl)).

Let us consider such a set $S$ in $\Upsilon^{\prime}$ (at the moment
transferring to the callee). Suppose that one element of $S$ can be written.
Then the rule (P-procedureDecl) guarantee that this element is borrowed (it is
a borrow of a subtree $T$ of $\Upsilon$). Hence the rules (P-B-name), (P-B-
name-Out), (P-B-takeAccess), (P-B-nullValue), guarantee that the borrowed
subtree has permission set to NO if deep, and R if shallow. Note that the
borrowed subtree cannot have been observed, given that we borrow after
observing, hence we require RW permission on an argument that has been set to
R by observation. Thus, it is impossible for $T$ to be observed, hence
creating another element of $S$ that could be readable. For the same reason,
the hypothesis of the rules (P-B-entryPointInOut) and (P-B-entryPointOut)
guarantee that the argument cannot be borrowed twice. Hence if one path can be
written, all others cannot be neither written nor read.

##  4 Implementation and results

###  4.1 Laziness of permission trees

The implementation of the permission rules is done in Ada. They are
implemented as a separate module of the GNAT Pro compiler (more precisely in
the front-end) and the analysis procedure is invoked from SPARK analyzer when
called with the special flag -gnatdF.

The implementation is 6200 lines long. It involves dynamically allocated tree
data structures that are used to implement the permission trees. However,
given that those trees may be infinite, we decided to proceed with a lazy
implementation of permission trees, with a special dethunking method. Indeed,
the maximum depth at which those permission trees are used is the maximum
number of lexemes of a path, which is always finite, and in practice less than
7. Moreover, the AST does not allow easy iteration on extensions of paths,
hence those trees have to be built on the fly, leaving undefined many
parameters.

The definition of permission trees is hence modified to accept arrays, as well
as fields to records that may not be referenced by the original definition,
but may be added by object oriented programming (class-wide or incomplete
types). Note that the $Thunk$ node may represent both a leaf and an
unevaluated internal node.

$\begin{array}[]{lcl}P&::=&Thunk(Permission,Is\\_Node\\_Deep,Children\\_Permission)\\\
&|&Record(Permission,Is\\_Node\\_Deep,Fields\rightarrow P,P)\\\
&|&Access(Permission,Is\\_Node\\_Deep,P)\\\
&|&Array(Permission,Is\\_Node\\_Deep,P)\\\ &&\\\ \end{array}$

This creates some approximations in our implementation, specially when setting
the permissions to every extension in our permission rules, given that it is
not possible to iterate over extensions. The exact implementation dethunks the
tree depending on the type of the node, except for class-wide or incomplete
types, that are replaced by an over-approximation. Similarly, when the
permission changes for the whole subtree (such as assigning to a node), then
the subtree is deallocated and replaced by a $Thunk$ node.

###  4.2 Complete SPARK

Figure 6: The different deep types in full Ada. Access types can be added the
modifier constant that will prevent any modification to the pointed value. Any
other access type is called access-to-variable.

The rules presented in this report only address a subset of SPARK. However,
during the internship, the rules as well as the implementation target the
complete SPARK added with access types. Complete SPARK differs from $\mu$SPARK
on several points.

As evoked before, SPARK has arrays. We apply our permission rule to all
elements, without taking into account the exact index of that element. That
means when assigning to an element of an array, there are no effects in terms
of permissions, given that it is not known which element has been assigned. In
section 4.4, we present a method to have an iterator over an array of
pointers.

Besides procedures, SPARK has functions, that can return values and whose
calls are expressions (instead of statements for procedures). Note that
functions in SPARK can only have parameters of mode in and cannot have side
effects. To handle them safely, we add the rule that every formal parameter
has read-only permission (observing). Moreover, the expression returned is
considered to be moved. This constructs allows constructors (destructors being
procedures), but not accessors.131313However Ada has a mechanism called
_renaming_ that allows renaming a path to another, acting like an accessor to
one specific path.

Types for which passing to procedure as parameter can cause aliasing problems
are not the same as the ones that can cause aliasing problems when being
assigned. Actually deep types only designate the latter, the former being
already defined in Ada as _not-by copy_ types (see Figure 6). Indeed,
parameters to procedure are passed by-copy when they are shallow and can fit
in a standard machine register. Other parameters may be passed by reference if
shallow (compiler dependent) or are passed by reference if deep. Hence, the
rules for complete SPARK replace deep by _not by-copy_ in observes and
borrows, while deep is kept for moves.

Many features from OOP have been ignored in this report, such as class-wide
types. Some approximations are done to keep the safety of the analysis. We
consider all class-wide types to be deep, by just ignoring their content, and
considering them as always aliasing types.

Loops in Ada can be either finite or infinite. Exit statements allow exiting
any enclosing loop. Thus, we require that the permission of each path at the
exit point of a loop (exit statement or end of finite loop), has to be less
restrictive than at entry. This is enforced by an hashtable that associates
each loop id to two permission environments, the one at entry and an
accumulator that merges every environment at each exit point of the loop.

Global variables are considered as implicit parameters to the most enclosing
procedure, all the more since SPARK requires specifying the mode of each used
global in a procedure. Thus, they obey to the same rules as formal parameters
and actual parameters. When calling a procedure, the caller has to ensure that
every global variable used in the procedure has adequate permissions with
respect to specified mode.

Packages in Ada can have elaboration code that is executed when being loaded
from outside. Any initialized global declaration in Ada is implicitly
rewritten as initialization code. This feature is very useful for interacting
with hardware that needs to be initialized before any call to the library. In
our analysis, we treat this code as a procedure that has as out parameter
every stateful global variable of the package.

###  4.3 Test suites

The analysis has first been tested on two test suites. The first, called
_fixedbugs_ , contains 17041 tests for all bugs fixed and features added in
GNAT Pro compiler. The second is called _acats-4_ (Ada Conformity Assessment
Test Suite),141414They can be downloaded from http://www.ada-auth.org/acats-
files/4.1/ACATS41.ZIP and has 3905 standardized tests that every Ada compiler
must pass. Those test suites must be passed in order to show that the new
features implemented in the front-end do not break the existing compiler
architecture. However, given that they do not contain any SPARK code, they do
not allow assessing the efficiency of our rules on existing code base.

The most interesting test suite is _spark2014_ , specific to SPARK. This suite
has 2087 tests with valid SPARK code, and our analysis has only 30
regressions, almost all of them being caused by class-wide global variables
that are manipulated with finer graining than the analysis is able to handle.

Finally, a small test suite written by the author has been used to check that
the different constructs act accordingly to the anti-aliasing rules. These
tests are inspired by the examples given in Rust borrow-checker README
file.151515https://github.com/rust-
lang/rust/blob/master/src/librustc_borrowck/borrowck/README.md

###  4.4 Some use cases

####  4.4.1 Swap

The first example is the swap procedure, whose naive implementation gets
accepted by our rules. Note that there is no way of implementing a swap
function in Rust. In Ada, we take advantage of in-out mode, that guarantees
that after the procedure call, the in-out actual parameter to be assigned is
exactly at the same address than the one being sent to the callee.

⬇

procedure Swap (X, Y:in out T) is

Temp :T :=Y; \-- Move Y. X:RW, Y:W, Temp:RW

begin

Y:=X; \-- Move X. X:W, Y:RW, Temp:RW

X:=Temp; \-- Move Temp. X:RW, Y:RW, Temp:W

end Swap; \-- Both borrowed arguments X and Y have RW permission.

####  4.4.2 Iterator

The second example shows how to have a mutable iterator over an array of
pointers using the previously defined swap procedure. The procedure guarantees
RW permission for both its arguments. Note that it is also possible to use
renaming declarations for this case, but only the swap method could iterate
pairwise over an array (bubble sorting, …).

⬇

Iterator:=Null; \-- Iterator:RW

for i in a..b loop

Swap(Iterator, My_Array(i)); \-- Iterator:RW and My_Array(...):RW = Null

DoStuff(Iterator); \-- Iterator:RW and My_Array(...):RW = Null

Swap(Iterator, My_Array(i)); \-- Iterator:RW = Null and My_Array(...):RW

end loop; \-- My_Array:RW

####  4.4.3 Dynamic data structures

The last example shows some pieces of a code that manipulates trees with their
child-sibling representation[7]. The code has a procedure Free_Node that
deallocates recursively a whole tree, and some statements that allocate a tree
shown by Figure 7. Then some procedure is called with two nodes passed as
borrowed parameters with mode in-out, before the whole tree is freed.

Figure 7: The tree in example 4.4.3.

⬇

procedure Free_Node (N : in out Node) is

if N.Child /= null

Free_Node (N.Child);

end if;

if N.Sibling /= null

Free_Node (N.Sibling);

end if;

Free (N); \-- N set to null by Free;

end Free_Node;

Node := new Node; \-- allocate node

Node.Child := new Node; \-- allocate child

Node.Child.Child := new Node; \-- allocate child

Node.Child.Sibling := new Node; \-- allocate sibling

Some_Procedure (Node.Child, Node.Sibling);

Free_Node (Node);

###  4.5 Comparison with Rust

The following section compares Rust and SPARK on some constructs that seem
relevant to the author. We study what features the anti-aliasing allows and
what constructs can be done using these rules. The main difference comes from
the fact that SPARK uses provers to handle a lot of safety features, that are
handled directly by Rust’s borrow-checker.

Features | SPARK | Rust
---|---|---
No-aliasing | ✓ | ✓
Lifetime check | Specific checks | ✓
Automatic reclamation | Pools | ✓
Initialization checking | Flow | ✓
Nullity checking | By proof | ✓
Simple semantics | ✓ | [14]
No user annotation | ✓ |
Figure 8: Comparison of the features available from the anti-aliasing analysis
of SPARK and Rust.

First comparison is on the features done by the analysis of both languages (as
shown in Figure 8). Even if both of them prevent non-benign aliasing in the
source code, comparison shows that our rules do not handle as much features as
Rust’s borrow-checker, but allows more constructs than Rust (such as swap
present in 4.4.1).

Indeed, Rust’s borrow-checker checks lifetimes (so that a local deep variable
cannot be assigned to a global one), whereas this check is implemented as a
separate analysis of GNAT compiler, with some more restrictive rules than
Rust.

Automatic reclamation is handled by Rust’s borrow-checker (using a static
garbage collector), whereas Ada has a separate feature, called _pools_ ,
acting like virtual stacks with a scope. Every variable allocated in this pool
gets freed when the pool is destroyed (and lifetime checks prevent aliasing
between two pools of different scopes).

Initialization checks are similarly done by Rust’s borrow-checker in a safe
way, whereas our rules only catch some uninitialized variable usage, with
SPARK flow analysis doing the safe and very fine-grained analysis.

Nullity-checking is also a built-in feature of Rust (there a no safe null
pointers in Rust), whereas we allow them, considering dereferencing a null
pointer should be considered as a runtime error (like division by 0), and
should be checked by SPARK static analysis tool-suite at silver level (AoRTE
proof) [3].161616The joint Thales-AdaCore guideline defines fives levels of
software assurance for SPARK software. The first is stone, that consists of
valid SPARK code. The second is bronze, SPARK code that passed the
initialization check and has a correctly specified data-flow. The third is
silver, that adds the proof of AoRTE. The fourth is gold, in which key
integrity properties are proven, such as pre and post conditions, type
predicates, loop invariants. The fifth requires full functional proof of
requirements, with a program fully specified. More details can be found on the
following blog post http://www.spark-2014.org/entries/detail/verifythis-
challenge-in-spark

Finally, we should note that our analysis does not require any additional user
annotation to the source code (whereas Rust needs sometimes explicit lifetimes
to be specified), and the rules are unambiguously defined whereas for Rust no
official document specifies the borrow-checker (the README provided is quite
incomplete).

Features | SPARK | Rust
---|---|---
Move semantics | ✓ | ✓
Read only grant | Only to callee | ✓
Move to callee | ✓ | ✓
Move back to caller | ✓ | Only 1 path
Primitives (swap) | ✓ |
Fine graining (R/RW) | ✓ |
Figure 9: Comparison of the constructs accepted by the anti-aliasing analysis
of SPARK and Rust.

Second comparison is on what could be defined as expressiveness of the
analysis, that means which constructs can be implemented on this analysis.
Although we did not formalize this concept (and did not prove for Rust that
some constructs could not be implemented), we consider that a little review of
some constructs can be useful.

We previously showed that cycling constructs could not be implemented in SPARK
(No-cycle lemma). Rust has a similar limitation and requires some work-around
to implement structures like graphs (like manually handling
indexes).171717https://github.com/nrc/r4cppp/blob/master/graphs/README.md We
also saw that swap primitive is available in SPARK whereas it requires unsafe
code in Rust, and the in-out mode allows assigning the exact same path as the
one borrowed. In Rust, this feature is available for only one path by moving
the argument to the callee, and moving back from the callee the argument as
return value of the function.

Similarly, our intra-procedural analysis has the best approximation possible
on aliasing (except for object oriented programming), using the lattice of
permissions previously defined that allows tracking the exact path that gets
aliased. Rust has a mechanism of restrictions against assignment, mutable
borrow, or read-only borrow, which would correspond respectively to R/NO,
R/W/NO, or W/NO. For instance, in Rust, when moving a variable, every prefix
and extension gets restricted indiscriminately, whereas in SPARK, only paths
that access to the aliased data are restricted on their reading or writing
permission accordingly.

Another interesting design choice we made, is to ban borrows or observes
inside a block, whereas Rust allows it. Indeed, we do not see use cases for
which we need to create several read-only copies of a same deep variable in
the body of a subprogram, all the more since this feature would require some
new lexical constructs (like keywords or symbols), that cannot be added easily
in Ada. Moreover, Ada has a mechanism, called _renaming_ , that is used to
shorten long paths, hence also rendering useless read-write borrows of a path.

##  5 Conclusion

In this report, we have presented anti-aliasing rules that allow adding
pointers to SPARK, a subset of Ada used for static analysis with deductive
verification. We showed a systematic analysis that allows a wide range use
cases of pointers and dynamic allocation, as showed by the experiments. To the
best of our knowledge, this is a novel approach for controlling aliasing
introduced by arbitrary pointers in a programming language supported by proof.
Our approach does not require user annotations or proof of verification
conditions, which makes it much simpler to adopt. Moreover, we provided a
mathematical proof of the safety of our analysis, and compared our method to
another language providing such analysis, Rust.

Yet, still some work needs to be done to start using this analysis in
commercial applications. Indeed, some constructs of SPARK (specially object
orientation) are still not handled efficiently by the rules, and the back-end
still does not implement proofs with pointers, which hopefully will be solved
during year 2018. Similarly, some Ada libraries have to be changed in order to
get them accepted by SPARK (drivers and containers), even though those fixes
can be done without major refactoring. We could hopefully expect that future
contributors to these anti-aliasing rules will tackle those problems.

Another long term goal would be extending the analysis so that it could handle
different features (like Rust), such as automatic reclamation, parallelism,
initialization and lifetime checks, which will simplify the existing
mechanisms in the GNAT compiler.

## Appendix

##  Appendix A References

## References

  * [1] AdaCore and Altran UK Ltd.  SPARK 2014 Reference Manual.  http://docs.adacore.com/spark2014-docs/html/lrm/.
  * [2] AdaCore and Altran UK Ltd.  SPARK 2014 User’s Guide.  http://docs.adacore.com/spark2014-docs/html/ug/.
  * [3] AdaCore, Thales.  Implementation Guidance for the Adoption of SPARK.  http://www.adacore.com/uploads/technical-papers/ePDF-ImplementationGuidanceSPARK.pdf.
  * [4] AXE Consultants.  Ada Reference Manual, ISO/IEC 8652:2012(E).  http://www.ada-auth.org/standards/12rm/RM-Final.pdf.
  * [5] A. Burns.  The Ravenscar Profile.  Ada Lett., XIX(4):49–52, Dec. 1999.
  * [6] Filliâtre, Jean-Christophe and Paskevich, Andrei.  Why3 – Where Programs Meet Provers.  In ESOP’13 22nd European Symposium on Programming, volume 7792, Rome, Italy, Mar. 2013. Springer.
  * [7] M. L. Fredman, R. Sedgewick, D. D. Sleator, and R. E. Tarjan.  The pairing heap: A new form of self-adjusting heap.  Algorithmica, 1(1):111–129, Nov 1986.
  * [8] J.-Y. Girard.  Linear logic.  Theoretical Computer Science, 50(1):1 – 101, 1987.
  * [9] K. N. Gregertsen.  An Extended Ravenscar Profile for Execution Time Control.  Ada Lett., 33(2):109–114, Nov. 2013.
  * [10] B. Liskov.  Keynote Address - Data Abstraction and Hierarchy.  In Addendum to the Proceedings on Object-oriented Programming Systems, Languages and Applications (Addendum), OOPSLA ’87, pages 17–34, New York, NY, USA, 1987. ACM.
  * [11] N. D. Matsakis and F. S. Klock, II.  The Rust Language.  Ada Lett., 34(3):103–104, Oct. 2014.
  * [12] J. W. McCormick and P. C. Chapin.  Building High Integrity Applications with SPARK.  Cambridge University Press, 2015.
  * [13] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, Virgile Prevosto.  ACSL: ANSI/ISO C Specification Language Version 1.12.  https://frama-c.com/download/acsl.pdf.
  * [14] Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.  RustBelt: Securing the Foundations of the Rust Programming Language.  2017\.
  * [15] E. Reed.  Patina: A Formalization of the Rust Programming Language.  Technical report, University of Washington, 2015.
  * [16] J. C. Reynolds.  Separation Logic: A Logic for Shared Mutable Data Structures.  In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS ’02, pages 55–74, Washington, DC, USA, 2002. IEEE Computer Society.
  * [17] J. A. Tov and R. Pucella.  Practical Affine Types.  In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’11, pages 447–458, New York, NY, USA, 2011. ACM.

##  Appendix B Grammar for $\mu$SPARK

### Basic lexemes

$\begin{array}[]{lcl}\langle digit\rangle&::=&0-9\\\ &&\\\ \langle
alpha\rangle&::=&a-z|A-Z\\\ &&\\\ \langle ident\rangle&::=&\langle
alpha\rangle(\langle alpha\rangle|\langle digit\rangle|\\_)^{*}\\\ &&\\\
\langle integer\rangle&::=&\langle digit\rangle^{+}\\\ &&\\\ \langle
name\rangle&::=&\langle ident\rangle\\\ &|&\langle
name\rangle\texttt{.}\langle ident\rangle\\\ &|&\langle
name\rangle\texttt{.}\texttt{all}\\\ \end{array}$

### Expressions grammar

$\begin{array}[]{lcl}\langle expr\rangle&::=&\texttt{null}\\\ &|&\langle
integer\rangle\\\ &|&\langle name\rangle\texttt{'Access}\\\ &|&\langle
name\rangle\\\ \end{array}$

### Statements grammar

$\begin{array}[]{lcl}\langle instr\rangle&::=&\langle
name\rangle\texttt{:=}\langle expr\rangle\texttt{;}\\\ &|&\langle
name\rangle\texttt{:=}~{}\texttt{new}~{}\langle ident\rangle\texttt{;}\\\
&|&\langle ident\rangle\texttt{(}~{}{\langle
expr\rangle}^{+}\texttt{,}~{}\texttt{);}\\\ &|&\texttt{if * then}~{}\langle
instr\rangle~{}\texttt{else}~{}\langle instr\rangle~{}\texttt{end if;}\\\
&|&\texttt{begin}~{}\langle instr\rangle^{+}~{}\texttt{end;}\\\ \end{array}$

### Declarations grammar

$\begin{array}[]{lcl}&&\\\ \langle
file\rangle&::=&\texttt{procedure}~{}\langle
ident\rangle~{}\texttt{is}~{}\langle
decl\rangle^{*}~{}\texttt{begin}~{}\langle instr\rangle~{}\texttt{end;}\\\
&&\\\ \langle decl\rangle&::=&\texttt{type}~{}\langle
ident\rangle~{}\texttt{is record}~{}\langle field\rangle^{+}~{}\texttt{end
record ;}\\\ &|&\texttt{procedure}~{}\langle
ident\rangle~{}\texttt{(}~{}\langle
param\rangle^{+}_{\texttt{;}}~{}\texttt{)}~{}\texttt{is}~{}\langle
decl\rangle^{*}~{}\texttt{begin}~{}\langle instr\rangle~{}\texttt{end;}\\\
&|&\langle ident\rangle:\langle type\rangle\texttt{;}\\\ &&\\\ \langle
field\rangle&::=&\langle ident\rangle~{}\texttt{:}~{}\langle
type\rangle~{}\texttt{;}\\\ &&\\\ \langle type\rangle&::=&\langle
ident\rangle\\\ &|&\texttt{access}~{}\langle ident\rangle\\\ &&\\\ \langle
param\rangle&::=&\langle ident\rangle~{}\texttt{:}~{}\langle
mode\rangle~{}\langle type\rangle\\\ &&\\\ \langle
mode\rangle&::=&\texttt{in}~{}|~{}\texttt{in-out}~{}|~{}\texttt{out}\\\
\end{array}$

##  Appendix C Additional conditions on $\mu$SPARK

Some additional conditions are required in order to have valid $\mu$SPARK:

  * •

In a procedure call with parameters in-out or out, the parameter should be a
$\langle name\rangle$.

  * •

It is not possible to write to a formal parameter or any of its fields if it
is of mode in.

  * •

A declaration cannot shadow another one.

  * •

Two fields of a record cannot have the same name.

  * •

We consider that all parameters of mode in to procedures are passed by copy.
Hence, aliasing between in bound parameters can only occur between formal
parameters of deep type.

  * •

In record declaration, the record being declared can only be used under access
type.

##  Appendix D Typing $\mu$SPARK

The types for $\mu$SPARK are defined as the following:

$\begin{array}[]{lcl}\tau&::=&\texttt{integer}~{}|~{}R~{}|~{}\texttt{access}~{}\tau~{}|~{}\texttt{nulltype}\\\
\end{array}$

where $R$ is a record type. We also write $x:\tau\in R$ if the record type $R$
has a field $x$ of type $\tau$. We call $\equiv$ the smallest reflexive and
symmetric relationship so that
$\forall\tau,\texttt{nulltype}\equiv\texttt{access}~{}\tau$. We use $\Gamma$
to denote a set of variable, type, and procedure declarations. We write
$a\in\Gamma$ if the environment $\Gamma$ contains the declared object $a$. We
also use syntactic sugar $\Gamma+d$ to add the object declared by the
declaration $d$ to the environment $\Gamma$.

We define deep types by induction. Any $\texttt{access}~{}\tau$ type is deep,
and any record type $R$ in which there is at least one field of deep type is
also deep. Any type that is not deep is called shallow.

### Well-formed typing environments

We call well-formed any typing environment $\Gamma$ that is built
constructively from a well-typed program, starting with the empty environment.
We assume that in the following typing rules, the environments are well-
formed.

### Typing rules for names

We write $\Gamma\vdash_{\textnormal{\small n}}n:\tau$ if “in the environment
$\Gamma$, the name $n$ is well-typed and has type $\tau$”.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}{x:\tau}\end{array}}$ (T-readIdent)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}n:R\quad\quad a:\tau\in
R\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}{n.a:\tau}\end{array}}$ (T-readField)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}n:\texttt{access}~{}\tau\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}{n.\texttt{all}:\tau}\end{array}}$ (T-readDeref)

### Typing rules for expressions

We write $\Gamma\vdash_{\textnormal{\small e}}e:\tau$ if “in the environment
$\Gamma$, the expression $e$ is well-typed and has type $\tau$”.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
e}}\texttt{null}:\texttt{nulltype}\end{array}}$ (T-nullValue)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}e~{}\textnormal{integer
literal}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
e}}{e:\texttt{integer}}\end{array}}$ (T-literal)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}n:\tau\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
e}}{n\texttt{'Access}:\texttt{access}~{}\tau}\end{array}}$ (T-takeAccess)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}n:\tau\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
e}}{n:\tau}\end{array}}$ (T-name)

### Typing rules for statements

We write $\Gamma\vdash_{\textnormal{\small s}}s$ if “in the environment
$\Gamma$, the statement $s$ is well-typed”.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}{x:\tau^{\prime}}\quad\quad\Gamma\vdash_{\textnormal{\small
e}}e:\tau\quad\quad\tau\equiv\tau^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
s}}{x\texttt{:=}~{}e}\end{array}}$ (T-assignExpr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
n}}{x:\tau^{\prime}}\quad\quad\tau\in\Gamma\quad\quad\texttt{access}~{}\tau\equiv\tau^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
s}}{x\texttt{:=}~{}\texttt{new}~{}\tau}\end{array}}$ (T-assignNew)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\texttt{procedure}~{}P(x_{1}:m_{1}~{}\tau_{1}^{\prime},~{}...~{},x_{n}:m_{n}~{}\tau_{n}^{\prime})\in\Gamma\\\
\forall i\in\\{1..k\\},m_{i}=\texttt{in}\\\ \forall i\leq
k,~{}(\Gamma\vdash_{\textnormal{\small
e}}e_{i}:\tau_{i})\wedge(\tau_{i}\equiv\tau_{i}^{\prime})\quad\quad\forall
i>k,~{}(\Gamma\vdash_{\textnormal{\small
n}}n_{i}:\tau_{i})\wedge(\tau_{i}\equiv\tau_{i}^{\prime})\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
s}}{P(e_{1},~{}...~{},e_{k},n_{k+1}~{}...~{},n_{n})}\end{array}}$
(T-procedureCall)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall
j,~{}\Gamma\vdash_{\textnormal{\small
s}}i_{j}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
s}}{\texttt{begin}~{}i_{1}~{}...~{}i_{n}~{}\texttt{end}}\end{array}}$
(T-block)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall
j,~{}\Gamma\vdash_{\textnormal{\small
s}}i_{j}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
s}}{\texttt{if * then}~{}i_{1}~{}\texttt{else}~{}i_{2}~{}\texttt{end
if}}\end{array}}$ (T-ifCondition)

### Typing rules for declarations

We write $\Gamma\vdash_{\textnormal{\small t}}\tau$ if “in the environment
$\Gamma$, the type $\tau$ is well formed”.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
t}}{\texttt{integer}}\end{array}}$ (T-baseType)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
t}}\tau\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
t}}{\texttt{access}~{}\tau}\end{array}}$ (T-accessType)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}R\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
t}}{R}\end{array}}$ (T-recordType)

We write $\Gamma\vdash_{\textnormal{\small d}}d$ if “in the environment
$\Gamma$, the declaration $d$ is well formed”. Note that usage of global
variables is forbidden inside procedures.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
t}}\tau\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
d}}x:\tau\end{array}}$ (T-uninitDecl)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall
j,\Gamma\vdash_{\textnormal{\small
t}}\tau_{i}^{\prime}\quad\quad\Gamma^{\prime}:=\\{\tau\in\Gamma,\texttt{procedure}~{}P^{\prime}\in\Gamma\\}+P+x_{1}:\tau_{1}^{\prime}+...+x_{n}:\tau_{n}^{\prime}\\\
\forall k,\Gamma^{\prime}+d_{1}+...+d_{k-1}\vdash_{\textnormal{\small
d}}d_{k}\quad\quad\Gamma^{\prime}+d_{1}+...+d_{m}\vdash_{\textnormal{\small
s}}i\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
d}}\texttt{procedure}~{}P(x_{1}:\tau_{1}^{\prime},...,x_{n}:\tau_{n}^{\prime})~{}\texttt{is}~{}d_{1},...,d_{m}~{}\texttt{begin}~{}i~{}\texttt{end}\end{array}}$
(T-procedureDecl)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall
i,\Gamma+R\vdash_{\textnormal{\small
t}}\tau_{i}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\textnormal{\small
d}}{\texttt{type}~{}R~{}\texttt{is
record}~{}x_{1}:\tau_{1},...,x_{n}:\tau_{n}}~{}\texttt{end
record;}\end{array}}$ (T-recordDecl)

##  Appendix E Permission rules for µSPARk

### Definitions

#### Permission environments

Permission environment $\Phi$ are mappings from variable declarations to
permissions trees. As shown by the permission rules, permission environments
evolve through the execution of the program. Note that in case of a recursive
record type, the permission tree is infinite.

$\begin{array}[]{lcl}P&::=&Integer(Permission)\\\
&|&Record(Permission,Fields\rightarrow P)\\\ &|&Access(Permission,P)\\\ &&\\\
\end{array}$

#### Normalized permission environment

We say that a permission environment is normalized when each node of each tree
has a permission that is more permissive than the most restrictive permission
of its children.

#### PermRelease operator

We define a normalization operator called PermRelease that takes a permission
environment as input, and produces another one with permissions of each node
changed using the following definition:

$\begin{array}[]{lcl}\textit{PermRelease}~{}(Integer(\kappa))&=&Integer(\kappa)\\\
\textit{PermRelease}~{}(Record(\kappa,f_{i}\rightarrow
F_{i}))&=&Record(\kappa\vee(\bigwedge_{i}\textit{PermRelease}~{}(F_{i}).Permission),\\\
&&f_{i}\rightarrow\textit{PermRelease}~{}(F_{i}))\\\
\textit{PermRelease}~{}(Access(\kappa,D))&=&Access(\kappa\vee\textit{PermRelease}~{}(D).Permission,\textit{PermRelease}~{}(D))\\\
&&\\\ \end{array}$

This produced environment is trivially normalized.

#### Fusion operator

We define an operator called Fusion that takes two (or more) permission
environments as input, and outputs another one where for each node, the
permission is updated by taking the glb of every identical node from the
merged environments.

#### Pfresh(tau,kappa)

We also define the function $\textit{Pfresh}(\tau,\kappa)$ that takes a type
$\tau$ and a permission $\kappa$ as input and produces an adequate permission
tree.

More specifically,

  * •

$\textit{Pfresh}(\texttt{integer},\kappa)$ is equivalent to $Integer(\kappa)$.

  * •

$\textit{Pfresh}(\texttt{access}~{}\tau,\kappa)$ is equivalent to
$Access(\kappa,\textit{Pfresh}(\tau,\kappa))$.

  * •

$\textit{Pfresh}(R,\kappa)$ is equivalent to $Record(\kappa,\lambda x:\tau\in
R.\textit{Pfresh}(\tau,\kappa))$.

#### Syntactic sugar

We allow modifying or accessing permission and memory trees at a given paths
in the environments. For instance, $x.a.all.y\mapsto\textit{Pfresh}(\tau)$
will modify the node $x.a.all.y$ in the tree of x, by replacing its subtree
with a new (fresh) tree.

### Permission rules for names

We annotate each permission rule with n, e, s or d for readability purposes.

#### Move

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-M-ident)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{Move}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-M-field)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{Move}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-M-deref)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-SM-ident)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{Access}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-SM-field)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{Move}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-SM-deref)

#### Borrow

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n:\tau\quad\quad\tau~{}\textnormal{deep}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-identDeep)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n.a:\tau\quad\quad\tau~{}\textnormal{deep}\quad\quad\Phi.n\xrightarrow{Borrow}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-fieldDeep)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n.all:\tau\quad\quad\tau~{}\textnormal{deep}\quad\quad\Phi.~{}n\xrightarrow{Borrow}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-derefDeep)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n:\tau\quad\quad\tau~{}\textnormal{shallow}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-identShallow)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n.a:\tau\quad\quad\tau~{}\textnormal{shallow}\quad\quad\Phi.~{}n\xrightarrow{Borrow}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-fieldShallow)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n.all:\tau\quad\quad\tau~{}\textnormal{shallow}\quad\quad\Phi.~{}n\xrightarrow{Borrow}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-derefShallow)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi(n)=\texttt{RW}\quad\quad\Phi.~{}n\xrightarrow{Borrow}_{n}\Phi^{\prime}\\\
\Phi^{\prime\prime}=\Phi^{\prime}[\forall n^{\prime}~{}\textnormal{strict deep
extension of}~{}n,n^{\prime}\mapsto\texttt{NO},\\\ \forall
n^{\prime}~{}\textnormal{strict shallow extension
of}~{}n,n^{\prime}\mapsto\texttt{R}]\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-entryPointInOut)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi(n)=\texttt{W,RW}\quad\quad\Phi.~{}n\xrightarrow{Borrow}_{n}\Phi^{\prime}\\\
\Phi^{\prime\prime}=\Phi^{\prime}[\forall n^{\prime}~{}\textnormal{strict deep
extension of}~{}n,n^{\prime}\mapsto\texttt{NO},\\\ \forall
n^{\prime}~{}\textnormal{strict shallow extension
of}~{}n,n^{\prime}\mapsto\texttt{R}]\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-entryPointOut)

#### Observing

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n:\tau\quad\quad\tau~{}\textnormal{deep}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-O-ident)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n.a:\tau\quad\quad\tau~{}\textnormal{deep}\quad\quad\Phi.~{}n\xrightarrow{ObserveName}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-O-field)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{n}n.all:\tau\quad\quad\tau~{}\textnormal{deep}\quad\quad\Phi.~{}n\xrightarrow{ObserveName}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-O-deref)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi(n)=\texttt{R,RW}\quad\quad\Phi.~{}n\xrightarrow{ObserveName}_{n}\Phi^{\prime}\\\
\Phi^{\prime\prime}=\Phi^{\prime}[\forall n^{\prime}~{}\textnormal{strict
extension
of}~{}n,n^{\prime}\mapsto\texttt{R}]\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-O-entryPoint)

### Permission rules for expressions

#### Borrow (in or in-out mode)

Note that it is not possible to borrow an integer literal.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-nullValue)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{BorrowInOut}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-takeAccess)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{BorrowInOut}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-name)

#### Borrow (out mode)

Only names can be borrowed with mode out.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{BorrowOut}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-B-name-Out)

#### Observing

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-O-nullValue)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}e~{}\textnormal{integer
literal}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-O-literal)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{ObserveName}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-O-takeAccess)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}n\xrightarrow{ObserveName}_{n}\Phi^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-O-name)

### Permission rules for statements

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\quad\quad\Phi(x)=\texttt{W,RW}\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}x\texttt{:=
null}\xrightarrow{}_{s}\textit{PermRelease}(\Phi[x\mapsto\textit{Pfresh}(\tau,\texttt{RW})])\end{array}}$
(P-assignNull)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\quad\quad
e~{}\textnormal{literal}\quad\quad\Phi(x)=\texttt{W,RW}\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}x\texttt{:=}~{}e\xrightarrow{}_{s}\textit{PermRelease}(\Phi[x\mapsto\textit{Pfresh}(\tau,\texttt{RW})])\end{array}}$
(P-assignLiteral)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\quad\quad
n~{}\textnormal{name}\quad\quad\Phi(n)=\texttt{RW}\quad\quad\Phi.~{}n\xrightarrow{Move}_{n}\Phi^{\prime}\\\
\tau~{}\textnormal{deep}\quad\quad\Phi^{\prime\prime}=\Phi^{\prime}[\forall
n^{\prime}~{}\textnormal{strict extension of}~{}n~{}\textnormal{with more
{.all}},n^{\prime}\mapsto\texttt{NO}\\\ \forall
n^{\prime}~{}\textnormal{strict deep extension of}~{}n~{}\textnormal{with same
number of {.all}},n^{\prime}\mapsto\texttt{W}\\\ \forall
n^{\prime}~{}\textnormal{strict shallow extension of}~{}n~{}\textnormal{with
same number of {.all}},n^{\prime}\mapsto\texttt{RW}]\\\
\Phi^{\prime\prime}(x)=\texttt{W,RW}\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}x\texttt{:=}~{}n\xrightarrow{}_{s}\textit{PermRelease}(\Phi^{\prime\prime}[x\mapsto\textit{Pfresh}(\tau,\texttt{RW}))])\end{array}}$
(P-assignDeepName)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\quad\quad
n~{}\textnormal{name}\\\
\Phi(n)=\texttt{R}\quad\quad\Phi(x)=\texttt{W,RW}\quad\quad\tau~{}\textnormal{shallow}\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}x\texttt{:=}~{}n\xrightarrow{}_{s}\textit{PermRelease}(\Phi[x\mapsto\textit{Pfresh}(\tau,\texttt{RW}))])\end{array}}$
(P-assignShallowName)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\quad\quad
n~{}\textnormal{name}\quad\quad\Phi(n)=\texttt{RW}\quad\quad\Phi.~{}n\xrightarrow{Access}_{n}\Phi^{\prime}\\\
\Phi^{\prime\prime}=\Phi^{\prime}[\forall n^{\prime}~{}\textnormal{strict
extension of}~{}n,n^{\prime}\mapsto\texttt{NO}]\\\
\Phi^{\prime\prime}(x)=\texttt{W,RW}\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}x\texttt{:=}~{}n\texttt{'Access}\xrightarrow{}_{s}\textit{PermRelease}(\Phi^{\prime\prime}[x\mapsto\textit{Pfresh}(\tau,\texttt{RW})])\end{array}}$
(P-assignAccess)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi(x)=\texttt{W,RW}\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}x\texttt{:=}~{}\texttt{new}~{}\tau\xrightarrow{}_{s}\textit{PermRelease}(\Phi[x\mapsto\textit{Pfresh}(\tau,\texttt{RW})])\end{array}}$
(P-assignNew)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\texttt{procedure}~{}P(x_{1}:\tau_{1},~{}...~{},x_{n}:\tau_{n})~{}\textnormal{with}{}\\\
x_{1}...x_{a}~{}\textnormal{observed},\\\
~{}x_{a+1}...x_{b}~{}\textnormal{borrowed with mode {in}},\\\
~{}x_{b+1}...x_{c}~{}\textnormal{borrowed with mode {in-out}},\\\
~{}x_{c+1}...x_{n}~{}\textnormal{borrowed with mode {out}},\\\
\Phi_{1}=\Phi\\\ \forall~{}0<i\leq
a,\Phi_{i}.~{}e_{i}\xrightarrow{Observe}_{e}\Phi_{i+1}\\\ \forall~{}a<i\leq
b,\Phi_{i}.~{}e_{i}\xrightarrow{BorrowInOut}_{e}\Phi_{i+1}\\\
\forall~{}b<i\leq
c,\Phi_{i}.~{}e_{i}\xrightarrow{BorrowInOut}_{e}\Phi_{i+1}\\\
\forall~{}c<i\leq n,\Phi_{i}.~{}e_{i}\xrightarrow{BorrowOut}_{e}\Phi_{i+1}\\\
\Phi^{\prime}=\textit{PermRelease}(\Phi[\forall~{}b<i\leq
n:e_{i}\mapsto\textit{Pfresh}(\tau_{i},\texttt{RW})])\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}P(e_{1},~{}...~{},e_{n})\xrightarrow{}_{s}\Phi^{\prime}\end{array}}$
(P-call)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall
j>0,~{}\Phi_{j}.~{}i_{j}\xrightarrow{}_{s}\Phi_{j+1}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(P-block)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Phi.~{}i_{1}\xrightarrow{}_{s}\Phi^{\prime}\quad\quad\Phi.~{}i_{2}\xrightarrow{}_{s}\Phi^{\prime\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>* then}~{}i_{1}~{}\texttt{else}~{}i_{2}~{}\texttt{end
if}\xrightarrow{}_{s}\textit{PermRelease}(\textit{Fusion}(\Phi^{\prime},\Phi^{\prime\prime}))\end{array}}$
(P-ifCondition)

### Permission rules for declarations

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}x:\tau\texttt{;}\xrightarrow{}_{d}\Phi[x\mapsto\textit{Pfresh}(\tau,\texttt{W})]\end{array}}$
(P-uninitDecl)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\texttt{procedure}~{}P(x_{1},~{}...~{},x_{n})~{}\textnormal{with}{}\\\
x_{1}...x_{a}~{}\textnormal{observed},\\\
~{}x_{a+1}...x_{b}~{}\textnormal{borrowed with mode {in} or {in-out}},\\\
~{}x_{b+1}...x_{n}~{}\textnormal{borrowed with mode {out}},\\\
\Phi^{\prime}=\\{\forall~{}0<i\leq
a,x_{i}\mapsto\textit{Pfresh}(\tau_{i},\texttt{R}),\\\ \forall~{}a<i\leq
b,x_{i}\mapsto\textit{Pfresh}(\tau_{i},\texttt{RW}),\\\ \forall~{}b<i\leq
n,x_{i}\mapsto\textit{Pfresh}(\tau_{i},\texttt{W})\\}\\\
\Phi_{1}=\Phi^{\prime}\\\ \forall
k,\Phi_{k}.~{}d_{k}\xrightarrow{}_{d}\Phi_{k+1}\\\
\Phi_{m+1}.~{}i\xrightarrow{}_{d}\Phi^{\prime\prime}\\\ \forall
i\in\\{a+1..n\\},\Phi^{\prime\prime}(x_{i})=\texttt{RW}\end{array}}{\begin{array}[]{@{}c@{}}\Phi.~{}\texttt{procedure}~{}P(x_{1},...,x_{n})~{}\texttt{is}~{}d_{1},...,d_{m}~{}\texttt{begin}~{}i~{}\texttt{end}\xrightarrow{}_{d}\Phi^{\prime\prime}\end{array}}$
(P-procedureDecl)

##  Appendix F Theorems and proofs

We want to show that at each point of the program, the following lemmas and
theorem hold.

### Lemmas

######  Lemma 1.

(Normalization). Permission environment is normalized.

###### Proof.

Straightforward. Every rule of the semantics calls the normalization operator
PermRelease. The rules that do not call it are (P-block) (trivial case), and
declaration rules (they create only new trees with one node). ∎

######  Lemma 2.

(Coherence). For every node $n$ in the memory environment, it is possible to
find an associated node $n^{\prime}$ in the permission environment, such that
$n$ and $n^{\prime}$ designate the same path.

###### Proof.

Every permission rule manipulates permission trees that have the same
constructs as memory trees, except for access types that cannot be null. Hence
every memory tree can be obtained from a permission tree by cutting nodes at
access nodes when the pointer has null value. ∎

######  Lemma 3.

(Readability). If a node has permission R (resp. RW), then all its children
have permission R (resp. RW) at each step of the semantics.

###### Proof.

By induction on the semantics:

  1. 1.

(E-assignNull), (E-assignLiteral): $\textit{Pfresh}(\tau,\texttt{RW})$
guarantees it for the assigned path.

  2. 2.

(E-assignName), (E-assignAccess), (E-assignNew): same thing for the assigned
path. For the moved path, every prefix gets its permission set to either W or
NO by the (P-M-ident), (P-M-field), (P-M-deref) or (P-SM-ident), (P-SM-field),
(P-SM-deref) rules. The extensions are handled by (P-assignDeepName),
(P-assignShallowName), (P-assignAccess), and (P-assignNew).

  3. 3.

(E-call): we create such nodes by observing their paths. The rules (P-O-
nullValue), (P-O-litteral), (P-O-takeAccess), (P-O-name) guarantee that if any
node is set to permission R, then any extension of it is also set to R. After
the callee returned, the proof is identical to assignments.

  4. 4.

(E-block), (E-ifConditionTrue), (E-ifConditionFalse), (E-uninitDecl),
(E-procedureDecl): trivial

∎

######  Lemma 4.

(No-cycle). A node cannot have the same memory cell as any of its descendants
(hence memory trees are finite).

###### Proof.

By induction on the semantics:

  1. 1.

(E-assignNull), (E-assignLiteral), (E-assignNew): given that those rules only
cut memory trees, there are no new indirections created.

  2. 2.

(E-assignName): such a cycle could only be created when applying $Assign$ on a
node $Access(C1,\\_)$ which is a descendant of the node being moved
$Access(\\_,P)$. In such a case, this would contradict hypothesis of the rule
(P-assignDeepName), given that we set descendants of the moved node (ie strict
extensions) to NO, before checking RW for the node to assign.

  3. 3.

(E-assignAccess): such a cycle could only be created if the assigned $Access$
node is a descendant of the subtree we are taking address of. In such a case,
this would contradict hypothesis of the rule (P-assignAccess), given that we
set descendants of the moved node (ie strict extensions) to NO, before
checking RW for the node to assign.

  4. 4.

(E-call): borrows and observes do not modify addresses before transferring to
callee. After returning, we assign every parameter. Hence identical as
(E-assign) on each in-out or out parameter. For every in parameter,
SetFromExpr is equivalent to either assigning $n.all$ or $n$.

  5. 5.

(E-block), (E-procedureDecl): trivial by applying the induction hypothesis
successively to each statement of the block.

  6. 6.

(E-ifConditionTrue), (E-ifConditionFalse): the $Fusion$ operator does not
change memory places and pointers, only permissions.

  7. 7.

(E-uninitDecl): every node is assigned to a new memory area (and pointers to
null). Hence it is impossible to point to an existing memory area.

∎

### Non aliasing

######  Theorem 1.

(No-aliasing). For every set of nodes $S$ in memory environment such that
their memory cell is identical, consider their associated paths. Then, if
there is one path that can be written, then all other paths in $S$ can neither
be written nor read.

######  Proof of theorem 1.

To show that each theorem holds at each point of the program, we reason by
induction on the semantics:

  1. 1.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x\texttt{:=
null}\xRightarrow{}_{s}\Upsilon[x.all\mapsto\texttt{Null}]\end{array}}$
(E-assignNull)

Let us take any set $S$ in the environments $\Phi^{\prime},\Upsilon^{\prime}$
after executing one step of the semantics. Given that we do not modify
addresses during assignment, this set $S$ also verifies, by induction
hypothesis, non-aliasing before executing that step, in the environments
$\Phi,\Upsilon$. There is in $S$ at most one ancestor of $x$ (No-cycle on
$\Phi$). If there are none, there is nothing to prove. If there is one (that
we name $y$), let us consider the two cases of non-aliasing in
$\Phi,\Upsilon$, before executing that step.

     * •

If $y$ is the path that can be written (there is only one by induction
hypothesis), then using the fact paths not related to $x$ do not get their
permissions changed, we show that all others paths cannot be written or read
after executing one step of the semantics.

     * •

By (Readability), $y$ cannot be R in $\Phi$. Hence it can only be NO, which
leads to a contradiction. This means that if $y$ can be read, then it can also
be written.

     * •

If $y$ cannot be written nor read, then its permission is NO before executing
the semantics. By normalization of $\Phi$, we can say that the glb of its
children is also NO (and recursively). Which contradicts RW permission for
$x$.

  2. 2.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\quad\quad
e~{}\textnormal{literal}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x\texttt{:=}~{}e\xRightarrow{}_{s}\Upsilon[x.value\mapsto
e]\end{array}}$ (E-assignLiteral)

Exactly the same as (E-assignNull).

  3. 3.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}n~{}\textnormal{name}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x\texttt{:=}~{}n\xRightarrow{}_{s}\Upsilon[Assign(x,\Upsilon(n))]\end{array}}$
(E-assignName)

Let us take any set $S$ in the environments $\Upsilon^{\prime},\Phi^{\prime}$
after executing one step of the semantics. Nodes can only get aliased between
the first Access node descendant of assigned and moved node (because values
are recursively copied, up to the first Access node encountered in which the
pointer is copied, which creates an alias). Like (E-assignNull), we can
consider only the case when the moved or assigned path is the one that can be
written.

Executing one step of the semantics creates an alias in $x$ (the assigned
path) for every node of any subtree rooted under an $Access$ node that is a
direct descendant of $n$. However, the rule (P-assignDeepName) says that when
encountering an $Access$ node, all the further descendants are set to NO,
hence their paths cannot be written. The rules (P-M-ident), (P-M-field), (P-M-
deref) guarantee also that any extension of $n$ cannot be read anymore. This
solves the case for elements of $S$ that are descendant of $x$ with different
number of .all.

For elements of $S$ that are descendant of $x$ with same number of .all, no
alias is created during assignment, hence induction hypothesis can be applied
directly.

Hence, the assigned path gets RW permission (as well as any extensions), but
any aliased subtree of this node cannot be written nor read in the moved tree,
hence only one aliased path be written, and all others can neither be written
nor read.

  4. 4.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}n~{}\textnormal{name}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon,\Phi.~{}x\texttt{:=}~{}n\texttt{'Access}\xRightarrow{}_{s}\Upsilon[x.all\mapsto\Upsilon(n)]\end{array}}$
(E-assignAccess)

Let us take any set $S$ in the environments $\Phi^{\prime},\Upsilon^{\prime}$
after executing one step of the semantics. Nodes can only get aliased from the
subtree we take address and the one that is assigned using ’Access. Like
(E-assignNull), we can only consider exclusive write aliasing, as well as
consider the case when the moved or assigned path is the one that can be
written.

Executing one step of the semantics creates an alias of $x.all$ (the assigned
path) with the subtree rooted at $n$. However, the rules (P-assignAccess),
(P-SM-ident), (P-SM-field), (P-SM-deref) ensure that all the subtree as well
as its parents up to the first Access node encountered are set to NO, hence
any of the aliased path (extensions of $n$) cannot be written. The rules (P-M-
ident), (P-M-field), (P-M-deref) that get applied when applying (P-SM-deref)
also guarantee that those aliased paths cannot be read.

Hence, the assigned path gets RW permission (as well as any extension), but
any aliased subtree of this node cannot be written or read in the moved tree,
hence only one aliased path can be written, and all others can neither be
written nor read.

  5. 5.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x\texttt{:=}~{}\texttt{new}~{}\tau\xRightarrow{}_{s}\Upsilon[x.all\mapsto\textit{fresh}(\tau)]\end{array}}$
(E-assignNew)

Exactly the same as (E-assignNull), given that we allocate fresh memory area
not aliased with anything existing before.

  6. 6.

$\displaystyle\frac{\begin{array}[]{<EMAIL_ADDRESS>mode {in}},\\\ e_{a+1}...e_{b}~{}\textnormal{with mode {in-out}},\\\
~{}e_{b+1}...e_{n}~{}\textnormal{with mode {out}},\\\
\Upsilon^{\prime}=\\{\forall~{}0<i\leq
n,x_{i}\mapsto\textit{GetFromExpr}_{\Upsilon}(e_{i})\\}\\\
\Upsilon^{\prime}.~{}\texttt{procedure}~{}P(x_{1},~{}...~{},x_{n})\xRightarrow{}_{d}\Upsilon^{\prime\prime}\\\
\Upsilon^{\prime\prime\prime}=\Upsilon[\forall~{}0<i\leq
a,\textit{SetFromExpr}_{\Upsilon^{\prime\prime}}(e_{i},x_{i})\\\
\forall~{}a<i\leq b,Assign(e_{i},\Upsilon^{\prime\prime}(x_{i}))\\\
\forall~{}b<i\leq
n,Assign(e_{i},\Upsilon^{\prime\prime}(x_{i}))]\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}P(e_{1},~{}...~{},e_{n})\xRightarrow{}_{s}\Upsilon^{\prime\prime\prime}\end{array}}$
(E-call)

The case for procedure calls is particular: indeed we apply our inductive
hypothesis after modifying environments, hence we have to guarantee that the
invariants not only hold at the end of the rule, but also at the moment we
transfer the control flow to the callee (ie for $\Upsilon^{\prime}$ in
(P-call) and $\Phi^{\prime}$ in (P-procedureDecl)).

Let us consider such a set $S$ in $\Upsilon^{\prime}$ (at the moment
transferring to the callee). Suppose that one element of $S$ can be written.
Then the rule (P-procedureDecl) guarantee that this element is borrowed (it is
a borrow of a subtree $T$ of $\Upsilon$). Hence the rules (P-B-name), (P-B-
name-Out), (P-B-takeAccess), (P-B-nullValue), guarantee that the borrowed
subtree has permission set to NO if deep, and R if shallow. Note that the
borrowed subtree cannot have been observed, given that we borrow after
observing, hence we require RW permission on an argument that has been set to
R by observation. Thus, it is impossible for $T$ to be observed, hence
creating another element of $S$ that could be readable. For the same reason,
the hypothesis of the rules (P-B-entryPointInOut) and (P-B-entryPointOut)
guarantee that the argument cannot be borrowed twice. Hence if one path can be
written, all others cannot be neither written nor read.

  7. 7.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall
j>0,~{}\Upsilon_{j}.~{}i_{j}\xRightarrow{}_{s}\Upsilon_{j+1}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>(E-block)

Trivial by applying the induction hypothesis successively to each statement of
the block.

  8. 8.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Upsilon.~{}i_{1}\xRightarrow{}_{s}\Upsilon^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>* then}~{}i_{1}~{}\texttt{else}~{}i_{2}~{}\texttt{end
if}\xRightarrow{}_{s}\Upsilon^{\prime}\end{array}}$ (E-ifConditionTrue)

Let us consider such a set $S$. At the end of executing the first block, they
are non-aliased, at the end of the second block, they are also non-aliased.
Hence applying Fusion that only takes the $glb$ cannot give more permissions
to a path than it has before. Hence aliasing cannot occur.

  9. 9.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Upsilon.~{}i_{2}\xRightarrow{}_{s}\Upsilon^{\prime}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>* then}~{}i_{1}~{}\texttt{else}~{}i_{2}~{}\texttt{end
if}\xRightarrow{}_{s}\Upsilon^{\prime}\end{array}}$ (E-ifConditionFalse)

Exactly the same as (E-ifConditionTrue).

  10. 10.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x:\tau\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}x:\tau\xRightarrow{}_{d}\Upsilon[x\mapsto\textit{fresh}(\tau)]\end{array}}$
(E-uninitDecl)

It cannot point to existing memory area, hence cannot alias.

  11. 11.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Upsilon_{1}=\Upsilon\quad\quad\forall
k,\Upsilon_{k}.~{}d_{k}\xRightarrow{}_{d}\Upsilon_{k+1}\quad\quad\Upsilon_{m+1}.~{}i\xRightarrow{}_{d}\Upsilon^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon.~{}\texttt{procedure}~{}P(x_{1},...,x_{n})~{}\texttt{is}~{}d_{1},...,d_{m}~{}\texttt{begin}~{}i~{}\texttt{end}\xRightarrow{}_{d}\Upsilon^{\prime}\end{array}}$
(E-procedureDecl)

Like (E-block), we use inductive hypothesis to each declaration and then each
instruction of the body.

∎