]Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations

Extended Version
Extended version of “Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations,” <cit.>.

Chaitanya<EMAIL_ADDRESS>Mike<EMAIL_ADDRESS>Michael<EMAIL_ADDRESS>Milind<EMAIL_ADDRESS>Ryan R<EMAIL_ADDRESS>
Recent work showed that compiling functional programs to use dense, serialized
memory representations for recursive algebraic datatypes can yield significant
constant-factor speedups for sequential programs.

But serializing data in a
maximally dense format consequently serializes the processing of that
data, yielding a tension between density and parallelism.

This paper shows that a disciplined, practical compromise is possible.

We present , a
compiler that obtains the benefits of dense data formats and parallelism.

We formalize the semantics of the parallel location calculus
underpinning this novel implementation strategy,
and show that it is type-safe.

exceeds the parallel performance of existing compilers for purely
functional programs that use recursive algebraic datatypes,
including, notably, abstract-syntax-tree traversals as in compilers.

<concept_desc>Software and its engineering Formal language definitions</concept_desc>
<concept_desc>Software and its engineering Compilers</concept_desc>
<concept_id>10011007.10011006.10011008.10011009.10010175 </concept_id>
<concept_desc>Software and its engineering Parallel programming languages</concept_desc>

[500]Software and its engineering Formal language definitions
[500]Software and its engineering Parallel programming languages
[500]Software and its engineering Compilers

§ INTRODUCTION

Representing tree-like data as pointer-free, serialized byte arrays can
be extremely efficient for tree traversals, as it minimizes pointer-chasing and
maximizes locality <cit.>.

Moreover, by using an in-memory representation also suitable for external
transfer and storage <cit.>, programs can rapidly process
data without the overhead of deserialization.

Traditionally, any such tree-layout optimizations would be implemented manually by
the programmer—for example, in a scientific application with balanced

Recent work, however, has shown the benefits of automatically compiling tree
traversals to use denser representations, even for source programs written in a
general-purpose language.

The Gibbon compiler for a subset of Haskell
exemplifies this approach <cit.>.

While the dense data representation strategy works well for sequential
programs, there is an intrinsic tension if we want to parallelize
these tree traversals.  As the name implies, efficiently serialized
data must often be read serially.  To change that, first, enough indexing data
must be left in the representation so parallel tasks can
“skip ahead” and process multiple subtrees in parallel.  Second, the
allocation areas must be bifurcated to allow allocation of outputs in

In this paper, we offer a solution to these challenges.
We propose a strategy where form follows function: where data
representation is random-access only insofar as parallelism is needed,
and both data representation and control flow “bottom out” to
sequential pieces of work.  That is, granularity-control in the data
mirrors traditional granularity-control in parallel task
scheduling. We demonstrate our solution by extending the Gibbon
compiler with support for parallel computation, introducing .

We also extend LoCal, Gibbon's typed intermediate language,
adding parallelism and give an updated formal
semantics (sec:region-parallel-local).

In addition to tree traversals, we show that  can efficiently
compile other parallel programs, such as sort and search algorithms
(sec:evaluation) to match or exceed the performance of the best
existing parallel functional compilers.  We choose a functional focus
for three primary reasons:

* Many tree traversals have different input and output types—as in
a compiler pass that converts between intermediate languages—which necessitates
out-of-place traversals even in an imperative language.

* Even pure programs can use mutable data, via linear
types. (Gibbon uses these and eschews the IO monad.)

* The purely-functional parallel Gibbon programs considered in this work are intrinsically
data-race free.

The last point is worth emphasizing: every time a language adds both parallel
constructs and mutable data, it enables data-races and must define a memory
model to give them meaning.  In this work, we extend Gibbon with linearly-typed primitives for mutable data[Leveraging the Linear Haskell <cit.>
extensions now available in GHC 9]
while keeping the language race-free.

We claim that linearly-typed mutable data, efficient data representation, and
compiler-supported parallelism are a synergistic combination.

In Parallel Gibbon programs, as in other
purely functional parallel programs, parallelism annotations not only don't
introduce races but also do not affect program semantics,

meaning that these programs are deterministic as well as data-race free.

Ultimately, we believe that this work shows one path forward for
high-performance, purely-functional programs.  Parallelism in functional
programming has long been regarded as theoretically promising, but has a
spottier track record in practice, due to problems in runtime systems, data
representation, and memory management.

directly addresses these sore spots, showing how a
purely-functional program operating on fine-grained, irregular data can also run
fast (sequentially) and parallelize efficiently.

This complements more well-trodden areas of compiler research on parallelism, such
as dense and sparse collective operations on arrays <cit.>.

That is, the approach described in this paper—for general-purpose, recursive
functional programs, including tree traversals—could be combined with targeted EDSLs or libraries implementing additional parallel programming idioms,
such as Haskell's Accelerate <cit.>.  Both determinism and
data-race-freedom would be compositional within the functional-parallelism

Indeed, we have taken the first steps in this direction, adding a small set of parallel array primitives to Gibbon (subsec:parallel-arrays).

In this paper, we make the following contributions:

* We introduce the first compiler that combines parallelism with automatic dense data
representations for trees. While dense data <cit.> and
efficient parallelism <cit.> have been shown to independently yield large
speedups on tree-traversing programs, our system is the first to combine
these sources of speedup, yielding the fastest known performance generated by
a compiler for this class of programs.

* We formalize the semantics of a parallel location calculus
(sec:region-parallel-local) that underpins the compiler,
including a proof of its type-safety (subsec:type-safety).
To do so, we extend prior work on location calculi <cit.>,
which in turn builds on work in region calculi <cit.>.

* We evaluate our implementation (sec:implementation)
on several benchmarks
from the literature (sec:evaluation).
On a single thread, our implementation is
$1.93\times$, $2.53\times$, and $2.14\times$
faster than  <cit.> (an extension of MLton),
OCaml, and GHC, respectively.
When utilizing 48 threads, our geomean speedup is
$1.92\times$, $3.73\times$ and $4.01\times$,

meaning that the use of dense
representations to improve sequential processing performance
coexists with scalable parallelism.

Most notably, the speedup on a five-pass compiler drawn from a university
compiler course was $1.02\times$, $2.2\times$ and $10.7\times$ over those alternative

§ OVERVIEW

We give a high-level overview of the ideas presented in this paper
using a program given in fig:example1-haskell

(with a larger sample program given in Appendix <ref>).

(with a larger sample program given in the Appendix of the extended version <cit.>).

Because the techniques we present for compiling tree-traversals are
directly applicable to compilers themselves, we use
a miniature compiler pass as our example.

The example defines a datatype Exp which represents the abstract syntax of a language that supports
integer arithmetic, and a function constFold that implements
constant folding for this language.

Constant folding is a common compiler optimization in which expressions with
constant operands are evaluated at compile time, thus improving the run-time performance.

But here we are trying to optimize the performance of the constant folding pass itself
rather than the performance of the program produced by constant folding.

constFold walks over the abstract-syntax-tree, and substitutes all
expressions of the form (Plus (Lit i) (Lit j)) with (Lit (i+j)).

We only show a simplified constFold —
for example it doesn't recur on the children of Plus before checking if they're literals —
to keep it simple enough to serve as a running example.

The program in fig:example1-haskell is written using the
front-end language for Gibbon, a polymorphic, higher-order subset of Haskell,
with strict rather than lazy evaluation.

The ($\partup$) operator used on line <ref> denotes a parallel tuple — it marks its operands to evaluate in parallel with each other.

But with a purely functional source language, it is semantically equivalent to a sequential
tuple, i.e., replacing all “$\partup$” occurences with “,” yields a valid program.

We will return to this topic in sec:implementation.

Gibbon uses LoCal (short for location calculus) as an intermediate
representation (IR) with explicit byte-addressed, mostly-serialized data layout.

To go from the vanilla Haskell front-end language to ,
it performs location inference,
a variant of region inference <cit.>,
on the input programs.

The LoCal IR code generated by Gibbon for the constFold function
is shown in fig:example1.

In the following, we use it to sketch out how LoCal works.

§.§ A Primer on Location-Calculus

LoCal is a type-safe IR that represents programs operating on
densely encoded (serialized) data.  All serialized values live in regions,
which are unbounded memory buffers that never overlap and that store the raw data.
All programs make explicit not only the region to which a value belongs to, but
also a location at which that value is written.

In our notation, a location $\locreg{l}{r}$ resides in region $r$.

Locations are fine-grained indices into a region, but unlike pointers in
languages like C, arbitrary arithmetic on locations is not allowed.
Locations are only introduced relative to other locations,
and they can be written to only once.

Once allocated at a particular location, a value cannot be shared with another location
(within the same region or across regions), and it has to be copied
to allocate it at a different location.

(In practice, the Gibbon compiler supports sharing using pointers, which
we discuss in subsec:indirection-pointers.)

A new location is either: at the start of a region, one unit past
an existing location, or after all elements of a value rooted at an
existing location.

In the program given in fig:example1,

the location $\locreg{\loc_3}{\reg_2}$ is one past the
location $\locreg{\loc_2}{\reg_2}$ (line <ref>)
and $\locreg{\loc_4}{\reg_2}$ is after
every element of the value rooted at location $\locreg{\loc_3}{\reg_2}$
(line <ref>).

Any expression that allocates takes an extra argument:
a location-region pair that specifies where the allocation should happen.

The types of such expressions are decorated with these location-region pairs.

For example, the (Lit $\;\locreg{\loc_2}{\reg_2}\;$ i) data constructor
(line <ref>)
allocates a tag at location $\loc_2$ in region $\reg_2$, and has type (Exp$\tyatlocreg{}{\loc_2}{\reg_2}\;$).

Any scalar arguments passed to a data constructor, such as the
unpacked integer i in this case, are allocated immediately after

the tag.

Functions may be polymorphic over any of their input or output locations,
and these locations are provided at call-sites.

In the example, the function constFold is polymorphic over an
input location $\locreg{\loc_1}{\reg_1}$ and an output location $\locreg{\loc_2}{\reg_2}$,
and values for these are given at all call-sites.

In spite of the forall quantifier in its type signature,
the input and output regions given at its call-site must be distinct ($\reg_1 \neq \reg_2$) to prevent overwrites.

This property is checked by LoCal's type-system (described in subsec:type-system),
which makes multiple writes to any location illegal—with the use of a nursery environment—
ensuring that function calls like
(constFold [$\locreg{\loc_x}{\reg_x}$ $\locreg{\loc_x}{\reg_x}$] x)
don't type check.

§.§.§ Sequential Execution Model

LoCal has a dynamic semantics which can run programs sequentially <cit.>.
In this model, regions are represented as serialized heaps, where each heap
is an array of cells that can store primitive values
(data constructor tags, numbers, etc).

A write operation, such as the application of a data constructor, allocates to a fresh cell
on the heap, and a read operation reads the contents of a cell.
Performing multiple reads on a single cell is safe, and the type-system ensures
that each cell (location) is written to only once.

At run time, locations in the source language translate to heap indices,
which are the concrete addresses of the cells where reads/writes happen.

Computing addresses of locations which are at the start of a region,
or one past another location is straightforward
— the addresses get initialized to 0 and (prev + 1) respectively.

But evaluating an $\gramwd{after}$ expression,
to get an address one past the end of another, variable-sized value,
requires more work.

A naive computational interpretation of this $\gramwd{after}$ is to simply scan over
a value to compute its end.

In LoCal's formal model, this is referred to as the end-witness judgment.

Locations computed via $\gramwd{after}$ are used during both read and write operations.

For example,
when a LoCal case expression pattern matches on (Plus e1 e2),
it has to scan past e1 in order to know the starting address of e2,
which adds $O(n)$ amount of extra work in a fully serialized representation!

In practice, if values are read in the same order in which they were serialized,
a linear scan can be avoided by tracking end-witnesses that are
naturally computed in the evaluation of the program,
for example, by having every read return the address of the cell after it.

Intuitively, we can imagine there being a single read pointer that
is used to perform all reads in the program.

It always points to the next cell to be read on heap, and each read
advances it by one.

When the program starts executing, the read pointer starts at the
beginning of the heap and it chugs along in a continuous fashion.

Allocating a serialized value can  be thought of in a similar way —
that there is a single allocation pointer that starts at the
beginning of the heap, and moves along its length performing writes,
as illustrated in fig:step-by-step-dynamics-sequential-right.

To avoid changing the asymptotic complexity of programs which read values out-of-order,
the Gibbon compiler by default inserts some offset information —
such as pointers to some fields of a data constructor —  back into the representation.

But it doesn't allow out-of-order allocations,
which will be needed as we add parallelism to LoCal (subsec:parallelism-in-local).

§.§.§ Sequential Execution Model, Example

(a) Sequential, step-by-step execution of the program from
and (b) the heap operations corresponding to the output region $\reg_2$.

Each step is named after its line number in the program and only
shows the changes relative to the previous step.
AP is the allocation pointer.

P is short for Plus, and L is short for Lit.

To make this execution model concrete, let us go over
a step-by-step trace of the semantics executing constFold on
(Plus (Lit 20) (Plus (Lit 10) (Lit 12))).

The execution trace is given in fig:step-by-step-dynamics-sequential.

The store $\STOR$ maps regions to their corresponding heaps, and
the location map $\MENV$ maps symbolic locations to their corresponding
heap indices.

The evaluation starts at
(constFold [$\locreg{l_1}{r_1}\;\locreg{l_2}{r_2}$] e),
and is given a store containing a fully allocated input region $r_1$
and an empty region $r_2$ to allocate the output,
along with a location map
containing the locations $\locreg{l_1}{r_1}$ and $\locreg{l_2}{r_2}$
initialized to the starting addresses of these regions.

Since the input region has a Plus at the top,

execution continues at line 5.

The pattern match binds the locations $l_{a}^0$ and $l_{b}^0$ to
the addresses of the sub-expressions (Lit 20) and (Plus (Lit 10) (Lit 12))
respectively .

Since both the sub-expressions are not constants, execution continues at line 10.

Then, the output location of the first sub-expression, $\locreg{l_3}{r_2}$, is defined to
be one past $\locreg{l_2}{r_2}$, and constFold is invoked recursively
on this sub-expression.

Step 4 copies[This value is copied because line <ref> in fig:example1 has a data constructor (Lit $\;\locreg{l_2}{r_2}\;$ i) on the right hand side of the case alternative. If we update the program to return the input expression exp directly, Gibbon would allocate a pointer and the value (Lit 20) would be shared between the input and the output regions. We discuss how sharing works in subsec:indirection-pointers.]
the first sub-expression by writing a tag $L$ (short for Lit),
followed by the integer 20 on the heap.

Then, the output location of the second sub-expression, $\locreg{l_4}{r_2}$, is defined to be one past
every element of the first sub-expression, which occupies two cells after the 0$^{th}$ cell.

Thus, $\locreg{l_4}{r_2}$ gets initialized with the address of the 3$^{rd}$ cell.

constFold is now invoked recursively

for the second sub-expression.

Following similar steps, the second sub-expression is allocated at $\locreg{l_4}{r_2}$.

Since the second sub-expression is a Plus with constant operands,
it is transformed to (Lit 22).

Finally, Step 16 writes the tag $P$ (short for Plus) which
completes the construction of the full expression,
(Plus (Lit 20) (Lit 22)).

§.§ Parallelism in Location-Calculus

In this section, we outline various latent opportunities for parallelism
that exist in  programs (irrespective of annotation with “$\partup$”).

The first kind of parallelism is available when programs access
the store in a read-only fashion,

such as in an interpreter, for example.

interp : forall @lr@ . @Explr@ -> Int
interp [@lr@] t = case t of
Lit (i : @Intl_ir@) -> i
Plus (e1 : @Expl_ar@) (e2 : @Expl_br@) ->
(interp [@l_ar@] a) + (interp [@l_br@] b)

Even though the recursive calls in the Plus case can
safely evaluate in parallel, there is a subtlety: parallel evaluation
is efficient only if the Plus constructor stores offset
information for its right child node.

If it does, then the address of e2 can be calculated in constant
time, thereby allowing the calls to proceed immediately in parallel.

If there is no offset information, then the overall tree traversal is
necessarily sequential, because the starting address of e2 can be
obtained only after a full traversal of e1.

As such, there is a tradeoff between space and time, that is, the cost
of the space to store the offsets,
versus the time of the sequential traversal
forced by the absence of offsets.

Programs that write to the store also provide opportunities for

The most immediate such opportunity exists when the program performs
writes that affect different regions.

Such writes can happen in parallel because different regions cannot overlap
in memory.

There is another kind of parallelism that is more challenging
to exploit, but is at least as important as the others:

intra-region parallelism that can be realized by allowing different fields
of the same constructor to be filled in parallel.

This is crucial in  programs, where large, serialized data
(large trees or DAGs) frequently occupy only a small number of regions, and yet there are
opportunities to exploit parallelism in their construction.

Consider the case in fig:example1 which recursively calls
constFold on the sub-expressions of Plus.

If we want to access the parallelism between the recursive calls,
we need to break the data dependency that the right branch has on
the left.

The starting address of the right branch, namely $\locreg{l_4}{r_2}$, is
assigned to be end witness of the left branch by the after

But the end witness of the left branch is, in general, known only
after the left branch is completely filled, which would effectively
sequentialize the computation.

One non-starter would be to ask the programmer to specify the
size of the left branch up front, which would make it possible to
calculate the starting address of the right branch.

Unfortunately, this approach would introduce safety issues, such as
incorrect size information, of exactly the kind that
is designed to prevent.

Instead, we explore an approach that is safe-by-construction and
efficient, as we explain next.

§ REGION-PARALLEL LOCAL

To address the challenges of parallel evaluation—in concert with dense,
mostly-serialized data representations—we start by
presenting an execution model, ,
which can utilize all potential parallelism in  programs.

Parallelism in this formal model is generated implicitly,
by allowing every let-bound expression to potentially evaluate in parallel with the body.
Accordingly, the language omits explicit parallelism “hints” ($\partup$).

That is, you'll see in the next sections that implicitly parallel let has both a sequential and parallel evaluation rule.

By modeling every possible parallelization, the formal model is general —
it formalizes all possible valid parallel schedules, and all valid heap layouts.

We return to the pragmatic issue of selecting efficient parallelizations, i.e. granularity control, in subsec:granularity.

§.§ Region Memory and Parallel Tasks

(a) Parallel, step-by-step execution of the program from fig:example1 such that
parallel allocations happen only in separate regions,
and (b) the heap operations corresponding to the output region $\reg_2$.

Each step is named after its line number in the program and only
shows the changes relative to the previous step.

P is short for Plus, and L is short for Lit.

In the formal model, while parallelism is implicit, there is
still a restriction that at
most one task allocates in a given region at a time.

To realize intra-region parallelism, the model introduces fresh,
intermediate regions as needed, that is, when

the schedule takes a parallel evaluation step for a given let-bound expression,
and the body tries to allocate in the same region.

To demonstrate this, let us consider a trace of the
region-parallel evaluation of the program from fig:example1,

corresponding to the schedule
shown in fig:step-by-step-dynamics-region-parallel,
where the recursive calls to constFold on lines 12 and 14 run in parallel
with each other.

The parallel fork point for the first recursive call

occurs on the $11^{th}$ step of the trace.

At this point, the evaluation of the let-bound expression results in
the creation of a new child task, and the
continuation of the body of the let expression in the parent task.

Each task has its own private view of memory, which is realized by
giving the child and parent task copies of the store $\STOR$ and
location map $\MENV$.

These copies differ in one way, however: each sees a different mapping
for the starting location of e3, namely $\locreg{l_3}{r_2}$.

The child task sees the mapping
$\locreg{l_3}{r_2} \mapsto \concreteloc{r_2}{1}{}$, which
is the ultimate starting address of e3 in the heap.

The parent task sees a different mapping for $\locreg{l_3}{r_2}$,
namely $\concreteloc{r_2}{\indivar{e3}}{}$.

This address is an ivar: it behaves exactly like an I-Var <cit.>,
and, in our example, stands in for the completion of the memory being
filled for e3, by the child task.

Any expression in the body of the let expression that tries to read
from this location blocks on the completion of the child task.

The only exception to this blocking-rule is a letloc $\gramwd{after}$ expression, which is handled differently.

Such an expression occurs at line <ref>,
just after the parent continues after the fork point.

At this step, the parent task uses an after expression to
assign an appropriate location for the starting address of e4,
one past every byte occupied by e3.

If we synchronize with the child task here, the computation will effectively be

In order to avoid that,
the starting address of e4 is assigned to be
$\locreg{l_4}{r_2} \mapsto \concreteloc{r_2}{\indirection{r_3}{0}}{}$.

This address is an indirection pointing to the start of fresh region $r_3$, and
causes the parent task to allocate e4 in the region $r_3$ instead of $r_2$,
which is being allocated to by the child task,
thus maintaining the single-threaded-per-region allocation invariant.

The parent and child tasks have, in effect, two different
allocation pointers for

what will functionally be the same region (after joining).

The use of e3 on line <ref> forces the parent task
to join with its child task.

In particular,
$\concreteloc{r_2}{\indivar{e3}}{}$ is
substituted by $\concreteloc{r_2}{1}{}$, the starting address of
e3, in the expression and the location map $\MENV$.

Also, all the new entries in the location map $\MENV$ and store
$\STOR$ of the child are merged into the corresponding environments in
the parent.

Finally, the regions $r_2$ and $r_3$ are linked with a pointer,
corresponding to the indirection pointer that was added for the starting address of e4.

§.§ Syntax and Operational Semantics

∈  ,   ∈  ,

, ,∈  ,
, lr ∈  ,

∈  ,   ,  ∈  ,

;   ;

: ;  =

(: )

r + 1

_1 ↦_1 ,   …  , _n ↦_n

_1 ↦_1 ,   …  , _n ↦_n

_1_1 ↦_1 ,   …  , _n_n ↦_n

; ;

(, , )

_1, …, _n

Grammar of .

In this section, we present the formal semantics of our parallel
location calculus, . This semantics has also been mechanically tested in PLT
Redex <cit.>.

The grammar for the language is given in fig:opergram.

Again, all parallelism in this model language is introduced implicitly, by
evaluating let expressions.

There is no explicit syntax for introducing parallelism in our
language, and consequently the language is,
from the perspective of a client, exactly same as the
sequential language <cit.>.

The parallel operational semantics does, however, differ from the
sequential semantics, most notably from the introduction of a richer
form of indexing in regions.

Whereas in sequential  a region index consists simply of a non-negative integer,
it is enriched to an extended region index $\indbef{\ind}$ in .

It consists of either a concrete index
$\concreteind{\ind}$, an $\indivar{\ivarid}$, or an indirection pointer

A concrete index is a non-negative integer that specifies the
final position of a value in a region.

An ivar is a synchronization variable that is used to coordinate between parallel tasks.

For example, the $\indivar{e3}$ in the sample
trace in fig:step-by-step-dynamics-region-parallel, is used
to synchronize with the child task that is allocating e3.

An indirection $\indirection{\reg}{\concreteind{\ind}}$ points
to the address $\concreteind{\ind}$ in the region $\reg$,
and is used to link together different chunks of the same logical region,
which may have been introduced to enable intra-region parallel allocation.

For example, in the sample
trace in fig:step-by-step-dynamics-region-parallel, a pointer
$\indirection{\reg_3}{0}$ written at the end of the value e3
links it with the value e4, which is allocated to a separate region $\reg_3$.

And a concrete location $\concretelocvar$ is enriched to a pair
of a region $\reg$,
and an extended region index $\indbef{\ind}$.

The state configurations of  appear at the bottom of

Just like in sequential , a sequential state of
, $\SEQSTATE$, contains a store $\STOR$, location map $\MENV$, and an
expression $\EXPR$.

But by using enriched concrete locations,
the location map also has the ability to contain indirection pointers.

A value that can be written to a heap, $\heapval$, is
similarly enriched to allow indirection pointers.

§.§.§ Sequential Transitions

Selected dynamic semantics rules (sequential transitions).

A subset of the sequential transition rules are given in

The rules are close to the original sequential rules,
except for some minor differences.

For the rule , we need to handle the case
where an indirection is assigned to the source symbolic location

For this purpose, we use a metafunction $\hat{\MENV}$
(formally defined in Appendix <ref>)

(formally defined in the Appendix of the extended version <cit.>)

that can dereference indirection pointers when looking up its address in the location map $\MENV$.

With respect to the rule , we now
allow the concrete location assigned to the source location
$\locreg{\loc_0}{\reg}$ to hold an ivar.

The purpose of this relaxation is to allow an expression downstream
from a parallelized let binding to continue evaluating in
parallel with the task that is evaluating the let-bound expression.

The task evaluating the after expression continues by using an
indirection pointing to the start of a fresh region $\reg'$.

The effect is to make $\concreteloc{\reg'}{0}{}$ the setting for the allocation
pointer for the task.

If the source location $\locreg{\loc_0}{\reg}$ is assigned to hold a concrete index
$\concreteind{\ind}$, the rule  yields an address by using the
the end-witness judgment.

The remaining rules are similar to sequential ,
and are available in Appendix <ref>.

and are available in the Appendix of the extended version <cit.>.

§.§.§ Parallel Transitions

Dynamic semantics rules (parallel transitions).

We generalize a sequential state to a parallel task $\TASKVAR$ by
adding two more fields: a located type and a concrete location, which
together describe the type and location of the final result allocated
by the task.

A parallel transition in  takes the form of the following
rule, where any number of tasks
in a task set $\TASKSET$ may step together.

In each step, a given task may make a sequential transition, it may
fork a new parallel task, it may join with another parallel task,
or it may remain unchanged.

The parallel transition rules are given in

In these rules, we model parallelism by an interleaving semantics.

Any of the tasks that are ready to take a sequential step may make a
transition in rule .

A parallel task can be spawned by the  rule, from which an
in-flight let expression breaks into two tasks.

The child task handles the evaluation of the let-bound expression
$\EXPR_1$, and the parent task handles the body $\EXPR_2$.

To represent the future location of the let-bound expression,
and to create a data dependency on it,
the rule creates a fresh ivar, which is
passed to the body of the let expression.

This same ivar is also the target concrete location of the
child task, thereby indicating that it produces this value.

A task can satisfy a data dependency in a rule such as
, where a case expression is blocked

on the value
located at $\indivar{\ivarid_c}$, by joining with the task producing the value.

Because each task has a private copy of the store and location map,
the process of joining two tasks involves merging environments.

The merging of the task memories is performed by the metafunctions $\merges$ and $\mergem$,
defined formally in Appendix <ref>.

defined formally in the Appendix of the extended version <cit.>.

We merge two stores by merging the heaps of all the regions that are
shared in common by the two stores, and then by combining with all
regions that are not shared.

We merge two heaps by taking the set of all the heap values at
indices that are equal, and all the heap values at
indices in only the first and only the second heap.

The merging of location maps follows a similar pattern, but is slightly
complicated by its handling of locations that map to ivars.

In particular, for any location where one of the two location maps
holds an ivar and the other one holds a concrete index, we assign
to the resulting location map the concrete index, because the concrete
index contains the more recent information.

After merging the environments, all occurrences of
$\indivar{\ivarid}_c$ are eliminated in the continuation,
and are replaced by the index $\ind_p$,
that represents the starting index of the value produced by the task $\TASKVAR_p$.

Join points in  are, in general, deterministic, because they only
increase the information held by the parent task.

The rule  handles the case where a data constructor
is blocked on the value of its $j^{th}$ field, and it joins with the task
producing that value.

It is similar to , and also requires merging environments.

But depending on the schedule of execution,
if the $(j+1)^{th}$ field of this constructor was computed in parallel
with the $j^{th}$ field, they will both be allocated to separate regions,
due to the way the rule  works.

These fields have to be reconciled to simulate a single region.

For this purpose, we use a metafunction $\linkfields$
— defined formally in Appendix <ref> —

— defined formally in the Appendix of the extended version <cit.> —

which stitches together these fields
by writing an indirection pointing to the start of region containing the $(j+1)^{th}$ field
at an address one past the end of the $j^{th}$ field.

Thus, when all fields of a data constructor are synchronized with, all fields allocated
to different regions are linked together by indirection pointers,
forming a linked-list.

§.§ Type System

Typing rules for a parallel task $\TASKVAR$, and a set of parallel tasks $\TASKSET$.

Our type system for  requires some substantial extensions
to the original type system given by <cit.>.

These extensions address the need to handle multi-task configurations,
which require a number of new typing environments and rules.

Before we present these extensions, we recall the typing rule
for the configuration of a single task, which is mostly unchanged from
the original.

\[ \TENV;\SENV;\CENV;\AENV;\NENV \vdash \AENV'; \NENV'; \EXPR : \hTYP \]

The context for this judgment includes five different environments.
First, $\TENV$ is a standard typing environment.
Second, $\SENV$ is a store-typing environment, mapping
materialized symbolic locations to their types. That is, every location in $\SENV$ has been written and contains a value of type $\SENV(l^r)$.
Third, $\CENV$ is a constraint environment, keeping
track of how symbolic locations relate to each other.
Fourth, $\AENV$ maps each region in scope to a location, and is used to symbolically
track the allocation and incremental construction of data structures;

Finally, $\NENV$ is a nursery of all symbolic locations that have been allocated,
but not yet written to.

Locations are removed from $\NENV$ upon being written to,
as the purpose is to prevent multiple writes to a location.

Both $\AENV$ and $\NENV$ are threaded through the typing
rules, also occurring in the output of the judgment, to the right of the

To generalize our typing rules to handle multi-task configurations,
we introduce new environments for variables $\TENVMAP$, store
typing $\SENVMAP$, allocation constraints $\CENVMAP$, allocation
pointers $\AENVMAP$, and nurseries $\NENVMAP$.

These environments extend their counterparts in the sequential
type system, and are needed to track state on a per-task

fig:static-semantics-parallel gives
the precise typing rules to type check a parallel task $\TASKVAR$, and
a set of parallel tasks $\TASKSET$.

A parallel task $\TASKVAR$ is well-typed if its target expression
$\EXPR$ is well-typed, using the original  typing rules, and
a task set $\TASKSET$ is well-typed if all tasks in it are

's complete typing rules are given in Appendix <ref>.

's complete typing rules are given in the Appendix
of the extended version <cit.>.

§.§ Type Safety

Compared to the original type-safety result proved for single-task
, ours generalizes to parallel evaluation by requiring that,
for any given multi-task configuration, either the program has fully
evaluated or at least one task can take a step.

As usual, we prove this theorem by showing progress and preservation.

The main complication relates to the property that parts of the
overall store are now spread across the individual stores of the
tasks, whereas in the original proof there is only one store.

In particular, our proof must establish that the store of each task
remains well formed, even while that task waits on a data dependency,
and moreover after the task joins with another task and their stores
are merged.

The complete proof is available
in Appendix <ref>.

in the Appendix of the extended version <cit.>.

Here we summarize key invariants.

Many such invariants are specified by our well-formedness rule, which
applies to a set of tasks executing in the parallel machine.

We give the full rule in Appendix <ref>.

The full rule is given in the Appendix of the extended version<cit.>.

This judgment specifies two new invariants that must hold for all
tasks $\TASKVAR \in \TASKSET$.

The first enforces that all ivars get filled with an appropriate value.

In particular, if an expression being evaluated by a task references an ivar,

then there must be exactly one other task in the task set which supplies a
well-typed value for it.

The second invariant consists of the well-formedness judgment that
verifies certain properties hold for each store of a given task.

This judgment generalizes a similar rule used in the original proof
by its use of the overall task set $\TASKSET$.

We discuss in detail the necessary extensions in the sequel.

With these new typing judgments in hand, we can now state the type-safety
theorem, shown below.

This theorem states that, if a given task set $\TASKSET$ is well typed
and its overall store is well formed, and if $\TASKSET$

makes a transition to some task set $\TASKSET'$ in $n$ steps,
then either all tasks in
$\TASKSET'$ are fully evaluated or $\TASKSET'$ can take
a step to some task set $\TASKSET''$.

If        ∅;;;;⊢_taskset ' ; ' ;   ∧  ;;;

and        ^n '

then, either        ∀∈'.

or        ∃  ”.   ' ”.

§.§.§ Well formedness of the store

Our store well-formedness judgment extends the judgment of the
sequential  typing system to establish a global criterion
for well-formedness, checking in particular that parts of regions
that are distributed across each task-private store, given by
$\MENV; \STOR$, are well-formed:

This judgment, defined formally in Appendix <ref>,

This judgment, defined formally in the Appendix of
the extended version <cit.>,

is one of the most challenging parts of our extension, because it must be
strong enough to ensure safe merging of stores when tasks meet at join points.

Like in sequential LoCal, it specifies three categories of invariants.

The first category enforces that allocations occurring across the
task-private stores are accounted for.

In particular, for each symbolic location in the store-typing environment,
$(\locreg{\loc}{\reg} \mapsto \TYP) \in \SENV$,
a value must be allocated to the appropriate store.

There are two possible ways in which this allocation may occur:
(1) sequentially, in the current task, or (2) in parallel, in a different task.

In the sequential case, $\locreg{\loc}{\reg}$'s address in the location map $\MENV$ must be a
concrete index, and it must have an end-witness.

This technical point ensures that the store never contains partially allocated values.

In the parallel case, $\locreg{\loc}{\reg}$'s address in $\MENV$ must be an ivar,
and there must be exactly one other task, $\TASKVAR_{oth} \in \TASKSET$,
that supplies a well-typed value for it.

Moreover, $\locreg{\loc}{\reg}$'s address in $\TASKVAR_{oth}$'s location map must be a concrete index,
and if $\TASKVAR_{oth}$ has finished evaluating, this value must have an end-witness.

This property ensures that when these tasks merge, the resulting store has complete values
allocated at the expected addresses and the expected types.

The second category enforces that allocations occur in the sequence specified by the constraint
environment $\CENV$.

In particular, if there is some location $\locreg{\loc}{}$ in the domain of $\CENV$,
then the location map and store must have the expected allocations at the expected types.

The most interesting rule here is that for the after constraint,
since it involves potential parallel allocations.

For instance, if $(\loc \mapsto (\afterl{\tyatlocreg{\TYP}{\loc'}{}})) \in \CENV$,
then the values at locations $\loc$ and $\loc'$ may be allocated sequentially,
in the same task, or in parallel, in different tasks.

The sequential case is straightforward.

For the parallel case, there are two possibilities — (1) the task allocating the value at
location $\loc'$ may be still in-flight,
or (2) it may have already synchronized with the current (parent) task.

In the first case, we ensure the presence of an appropriate indirection in the location map
($\loc \mapsto \concreteloc{\reg}{\indirection{\reg_{\text{fresh}}}{0}}{}$)
and of a fresh region in the store ($\reg_{\text{fresh}} \in \STOR$).

Otherwise, we ensure that a link between the values at locations $\loc'$ and $\loc$ exists,
which is accomplished by the metafunction $\linkfields$.

The final category enforces that each location is written to only once.

This is done by checking that the domain of the store-typing environment and the nursery
are disjoint: $dom(\SENV) \cap \NENV = \emptyset$.

§.§ Controlling Fragmentation

A consequence of  introducing fresh regions
is that the schedule of evaluation dictates the way a value is laid out on the heap,
as shown in fig:datacon-layouts.

Every choice to parallelize an intra-region allocation implies the creation
of a new region and a new indirection, thereby introducing fragmentation.

Thus, in addition to the usual task-scheduling overheads,
in our system, a schedule that parallelizes too many allocations also leads
to fragmentation.

Conversely, effort at amortizing the overhead of parallelism
simultaneously amortizes the overhead of indirections and region

We return to this topic and address fragmentation along with parallelism granularity management in subsec:granularity.

The heap layout for a data constructor if:

(a) all fields are allocated sequentially,

(b) only the second and third fields are allocated in parallel with each other, and

(c) all fields are allocated in parallel.

§ IMPLEMENTATION

Gibbon is a whole-program[Gibbon’s automatic selection of data representation works best if it can see the whole program, much like the data-representation optimizations in MLton. One way to get around this issue would be to make the programmer responsible for choosing the representation, by using appropriate annotations in datatype definitions. Another option is to conservatively insert random-access information in all datatypes that flow into code within other compilation units. Our current implementation does not offer these options, and only supports whole program compilation.] micropass compiler that compiles a
polymorphic, higher-order subset of (strict) Haskell[Note
that we are not the first to propose a strict variant of Haskell, not only do many of its cousins like Idris take a strict approach, but GHC itself supports a module-level strict mode.].

The Gibbon front-end uses standard whole-program compilation and monomorphization
techniques <cit.> to lower input programs into a
first-order, monomorphic representation.

On this representation, Gibbon performs location inference
to convert it into a LoCal program, which has region and location annotations.

Then a big middle section of the compiler is a series of LoCal->LoCal compiler passes
that perform various transformations.

Finally, it generates C code.

Our parallelism extension operates in the middle end,
with minor additions to the backend code generator and the runtime system.

We add a collection of LoCal->LoCal compiler passes that transform the program
so that reads and allocations can run in parallel.

At run time, we make use of the Intel Cilk Plus language extension <cit.>
(and its work-stealing scheduler) to realize parallel execution.
Our implementation closely follows the formal model described in subsec:region-parallel-semantics,
but with explicit parallelism annotations.

§.§ Granularity Control

Before going further into the details of what we implemented, we first
explain our choices in what we do and do not implement.

As we saw in fig:example1-haskell, we use manual annotations
for the programmer to mark parallelism opportunities.  This is the
norm in both current and past parallel programming practice: from
MultiLisp <cit.> to OpenMP <cit.>, Cilk <cit.>,
Java fork-join <cit.>, etc.

Recall also that with a purely functional source language,
parallel-tuple annotations change performance only, not program
semantics, so a programmer need not worry about safety when inserting
annotations[This same property holds for inserting parallel
annotations in pure GHC Haskell code, which has been used to modest
benefit in past experimental work <cit.>, but
is not commonplace practice.].

Task granularity thresholds can be fine-tuned by using the same reasoning
as in other parallel systems — switch to sequential for small
problem sizes.

But there's also the issue of fragmentation
(subsec:fragmentation), i.e. amortizing the overhead of
pointers in the representation as well as parallel tasks in the
control flow. One might wonder how these interact.

§.§.§ How to optimize granularity in Gibbon?

Relatively small chunks of sequential data can effectively amortize the
cost of creating regions and indirections.

For instance, serializing just the bottom two levels in our binary tree examples eliminates 75% of pointers and ensures pointers use only 11% of memory.

The task size to amortize parallel scheduling overheads, on the other
hand, is usually much larger.  Therefore, it's best the Parallel
Gibbon programmer thinks about parallelism granularity exclusively,
and the data representation can comfortably follow from that.

In other words, a manual (or automatic) solution to task granularity, also gives “for free”, an efficient, mostly-serialized data representation with amortized indirections.

§.§.§ Why not automatic granularity?

Automatic task-parallel granularity control is an active research area

Combining Parallel Gibbon's automatic
control over data representation, together with automatic
granularity control, is a promising avenue for future work.  This goes
doubly so if approaches like Heartbeat scheduling
<cit.> mature to the point of offering robust backends
and runtime systems that compilers like Parallel Gibbon may target,
and very recent work offers a step in that direction <cit.>.

For this paper, however, it would be confounding to address automating
granularity simultaneously with compacting data representation and
assigning regions.

In our experiments (sec:evaluation), we hold task granularity
constant across different implementations of the same benchmarks,
focusing only on the impact of each compiler's code generation and
data representation choices.

Parallel Gibbon, as well as all of its competitors, use explicit
parallelism annotations, and schedule the same set of tasks at runtime
for the same program inputs, unless mentioned otherwise.

§.§ Desugaring Parallel Tuples

As shown in fig:example1-haskell,
in the front-end language, we use the standard parallel tuples to express parallelism,
like other eager, parallel functional languages <cit.>.

A parallel tuple (e1 $\;\partup\;$ e2)
marks the expressions e1 and e2 to evaluate in parallel with each other.

To more closely match Cilk, we desugar these parallel tuples into a spawn/sync representation in the compiler IR:

let x = spawn e1 in
let y = e2 in
let _ = sync in

Using this representation simplifies the subsequent conversion to LoCal,
in which additional steps like allocating regions or binding locations
may be required before getting to e1 or e2.

Generating the corresponding letregion/letloc bindings, such that they have
the correct scope, is easier with a spawn/sync representation.

Also, we preserve these parallelism annotations in the LoCal code we
generate.  In contrast with the formal model (with implicit
parallelism, sec:region-parallel-local), let y = e2
is always sequential, whereas let y = spawn e2 essentially
corresponds to a potentially parallel let binding, though the decision
is ultimately dynamic.

We do not support first-class futures, or tasks that communicate through channels
or other mutable data structures, and thus the task-parallelism opportunities available in
Parallel Gibbon remain effectively series-parallel.

But this is sufficiently expressive for writing a large number of parallel algorithms.

Note that the formal model can express some local, non-escaping futures that are not strictly series-parallel by using parallel lets that are
forced out of order. This pattern of parallelism does not provide much additional expressive power over that provided by parallel tuples, so we do not give up much by not exposing this capability in the front-end language.

§.§ Indirection Pointers

In the implementation, we need a runtime representation of optional
pointers to include in the data that corresponds to the indirections in the
semantics (sec:indirection-semantics-intro).

Fortunately, in the Gibbon compiler there is already a
pointer mechanism that is sufficient for our purposes.

This exists because of how Gibbon's regions grow—rather than copying
data into a larger buffer, Gibbon accumulates a linked list of contiguous
chunks, doubling the size on each extension. The last filled cell in a
chunk is an indirection into the next chunk.

Indirections also enable Gibbon to allocate a value that is shared
between multiple locations (within the same region or across regions)
without requiring a full copy,
which is crucial for ensuring asymptotic complexity conservation of programs.

Variable aliases indicate this sharing to the compiler.

For example, the aliased variable x in the expression
(let x = mkBigExpr in Plus x x) indicates that a single, shared value
must be allocated for the left and right subtrees of Plus.

Gibbon rewrites this expression to (let x = mkBigExpr in Plus x (IndPtr x)),
where the right subtree is an indirection pointing to the data allocated for
the left.

Similarly, the identity function (id x = x) becomes (id x = IndPtr x).

However, shared scalar values such as numbers and booleans are always copied,
because it is more efficient to do so.

In , we reuse this indirection pointer mechanism to implement
intra-region parallel allocations.

§.§ Parallel Reads

Using static analysis, Gibbon can infer if a dataype requires offsets,
and it can transform the program to add offsets to datatypes that need them.

In sequential programs, these are used to preserve asymptotic complexity of
certain functions.

In , we use these offsets to enable parallel reads.

We update that static analysis, and add offsets if a program
performs parallel reads, i.e. via a clause in a case expression that accesses a
data-constructor's fields in parallel.

§.§ Parallel Allocations

The implementation of intra-region parallel allocations closely follows the
design described in sec:region-parallel-local.

A program transformation pass generates code that allocates fresh regions and writes
indirection pointers at appropriate places.

But the metafunctions $\merges$ and $\mergem$ which merge task memories at join points have
a different run time behavior compared to their formal definition.

The implementation does not have a direct notion of a store.

At run time, a region variable $\reg$ is only a structure containing a
pointer to the start of a memory buffer
and some metadata necessary for garbage collection.

Two memory buffers are merged (linked) simply by writing a single indirection pointer
in one of them.

This operation is relatively cheap compared to the set union used
in the formal definition.

Similarly, the implementation does not have a direct notion of a location map,
and therefore there is no run time operation equivalent to $\mergem$.

At run time, all location variables become absolute pointers into the heap.

But there still exists an issue with fragmentation.

With granularity control — in the form of judicious use of parallel tuples —
we can restrict excessive creation of fresh regions, but the number of regions created will still
always be equal to the number of parallel tasks spawned by the program.

This can still cause fragmentation because all spawned tasks
might not actually run in parallel.

The key insight

is to make the number of fresh region allocations equal to the number of
steals, not spawns.

That is, because our implementation uses a work-stealing scheduler,
but the general idea applies to other schedulers as well: fragmentation
should be proportional to parallelism in the dynamic schedule, not the static
potential for parallelism.

Our implementation creates fresh regions for intra-region parallel allocations
only if they really run in parallel.

We accomplish this by using the Cilk Plus API to implement a hook to detect when steals occur.

Before reaching a parallel fork point (spawn), the runtime system stores the ID of the worker
executing the current code.

Next, the corresponding ID is immediately fetched in the continuation of the fork point.

If the IDs match, it indicates that a steal did not occur.

This optimization enables parallel allocations with minimal fragmentation.

§.§ Parallel Arrays

Programs need arrays as well as trees.
We extend Gibbon with array primitives such as
alloc, length, nth, slice, and inplaceUpdate,
and use them to build a small library of parallel array operations with
good work and span bounds.

The ability to safely mutate an array in-place allows us to implement optimizations
that go beyond what is commonly allowed in a purely functional language.

This is enforced using the new Linear Haskell extensions <cit.>, for example, the signature of an $O(1)$ array mutation is:

inplaceUpdate :: Int $\rightarrow$ a $\rightarrow$ Array a $\multimap$ Array a

Using these primitive operations, collective operations on arrays are implemented as recursive
divide-and-conquer functions in Parallel Gibbon that use parallelism annotations[These combinators offer variants to explicitly control sequential chunk size, or to use the common heuristic of splitting into a number of tasks that is a multiple of the number of cores (provided as a global constant).].

For example, our parallel map first allocates an array to store the output,
and then updates it in parallel with inplaceUpdate.

But all such potentially-racy operations are hidden behind a pure interface.

Also, an Array in  can only store primitive values such as
numbers, booleans, and n-ary tuples of such values.

In the future, we plan to explore ways to support data-parallel operations
on serialized algebraic data.

§.§ Memory Management

In the formalism,
regions are modeled as unbounded memory buffers that offer a byte-indexed storage
for primitive values (data constructor tags, numbers, etc.).

Practically, we start by allocating a single contiguous chunk of memory of bounded size.

When this chunk is exhausted, a new one which is double in size is allocated
and linked with the previous one using a pointer.

This policy is used up to an upper bound (1GB)
after which constant sized (1GB) new chunks are allocated.

Thus, a single region is really a linked-list of chunks:
a small initial chunk, with subsequent ones doubling in size.

The small initial chunk is beneficial when a region contains a small value,
and the doubling policy reduces the overall malloc overhead when
allocating large values.

Our garbage collection strategy is based on regions and lifetimes, and also reference counting.

In classic region calculi, regions can be immediately deallocated at the end of their lexical scope.

However, we allow indirection pointers to point across different regions (chunks),
which is crucial to support parallelism, (and also to maintain the asymptotic complexity
of certain sequential programs).

Thus, a region can stay alive beyond its lexical scope, for example if a pointer to
it is captured by another region which is still in scope.

We use reference counting to deallocate such regions.

When a region is initialized—with a letregion—its reference count is set to 1,
and it is decremented when the region goes out of scope.

At this stage, if its reference count hits zero, it is deallocated by freeing
all of its chunks.

When a chunk is freed, the reference counts of the regions it points to are also decremented,
which may cause some of these regions to be freed as well.

But these reference counts are per-region, rather than per-chunk.
Hence, even if a single chunk in a region is truly alive, all of its other chunks are also
considered alive, and cannot be freed.

Also, there isn't a supplemental garbage-collector for long-lived regions at this time,
as in later versions of MLKit <cit.>.

In the future, we plan to make improvements in this area.

Note, however, that it is impossible to create heap cycles in Gibbon, because it's a pure strict language. (In-place modification through linear types doesn't change this, and besides, Parallel Gibbon's arrays do not contain pointers or sum types.)

§ EVALUATION

In this section, we evaluate our implementation using a variety of
benchmarks from the existing literature, as well as a new compiler benchmark.

To measure the latent overheads of adding parallelism,
we compare our single-thread performance
against the original, sequential LoCal, as implemented by the Gibbon compiler.

Sequential Gibbon is also a good baseline for performing speedup calculations
since its programs operate on serialized heaps, and
as shown in prior work, are significantly faster than their pointer-based counterparts.

Note that prior work <cit.> compared sequential constant factor performance
against a range of compilers including GCC and Java.  Since Sequential Gibbon
outperformed those compilers in sequential tree-traversal workloads, we focus
here on comparing against Sequential Gibbon for sequential performance.

We also compare the performance of our implementation
to other languages and systems
that support efficient parallelism for recursive, functional programs
—  <cit.>,

Multicore OCaml <cit.>, and GHC.

(an extension of MLton)
is a whole-program, optimizing compiler for Standard ML <cit.>;

it supports nested fork/join parallelism, and generates extremely efficient code.

The experiments in this section are performed on a 48 core machine
(96 hyper-threads) made up of
2 $\times$ 2.9 GHz 24 core Intel Xeon Platinum 8268 processors, with 1.5TB of memory,
and running Ubuntu 18.04.

The shared memory on this machine is divided into two NUMA nodes
such that CPUs 0-23 and 48-71 use node-0 as their local memory node,
and 24-47 and 72-95 use node-1.

In our experiments we only use 48 threads (no SMT), evenly distributed across
both NUMA nodes (numactl $\;--$physcpubind=48-95).

All experiments are performed using the default memory allocation policy
which always allocates memory on the current NUMA node.

We observed that using a round-robin memory allocation policy
(option $--$interleave=0,1) did not affect performance,
and therefore we do not report those results.

Each benchmark sample is the median of 9 runs.

To compile the C programs generated by our implementation we use
GCC 7.4.0 with all optimizations enabled (option -O3), and
the Intel Cilk Plus language extension <cit.>
(option -fcilkplus) to realize parallelism.

To compile sequential LoCal programs we use the open-source Sequential Gibbon compiler, but we modify it to include arrays with in-place mutation using linear types, just like Parallel Gibbon.

For , we use version 20200220.150446-g16af66d05 compiled from its source code.

For OCaml, we use the Multicore OCaml compiler <cit.>
(version 4.10 with options -O3),
along with the domainslib [https://github.com/ocaml-multicore/domainslib]
library for parallelism.

We use GHC 8.6.5, with options -threaded -O2, along with
the monad-par <cit.> library for parallelism.

§.§ Benchmarks

We use the following set of 10 benchmarks.

For GHC, we use strict datatypes in benchmarks, which generally offers the
same or better performance, and avoids problematic interactions between
laziness and parallelism.

All programs use the same algorithms and datatypes
(including mutable arrays, which are provably race-free in Gibbon and GHC),
have identical granularity control thresholds, and are run with the same inputs.

This way, each pairing of program and input creates a deterministic task graph —
which does not change when varying the number of threads —
and the evaluation focuses on data representation and code generation,
rather than on decomposing and scheduling parallel tasks.

* fib:

Compute the 48th fibonacci number with a sequential cutoff after depth=18: a simple baseline for scaling.

* :

This is an artificial benchmark that is included here to
measure parallel allocation under ideal conditions.

It constructs a balanced binary tree of height 18, and computes
the 20th fibonacci number at each leaf, with sequential cutoff after depth=12.

* buildKdTree and countCorrelation and allNearest:
buildKDTree constructs a kd-tree <cit.>
containing 1M 3-d points

in the Plummer distribution.

The sequential cutoff is at a node containing less than 32K points.

countCorrelation takes as input a kd-tree and a list of 100 3-d points,
and counts the number of points which are correlated to each one.

The chunk-size for the parallel-map is 4, and the sequential cutoff
for countCorrelation is at a node containing less than 8K points.

allNearest computes the nearest neighbor of all 1M 3-d points.

The chunk-size for the parallel-map is 1024.

* barnesHut:

Use a quad tree to run an nbody simulation over
1M 2-d point-masses distributed uniformly within a square.

The chunk-size for the parallel-map is 4096.

* coins
This benchmark is taken from GHC's NoFib [https://gitlab.haskell.org/ghc/nofib]
benchmark suite. It is a combinatorial search problem that computes
the number of ways in which a certain amount of money can be paid by
using the given set of coins.

The input set of coins and their quantities are
and the amount to be paid is 999.

The sequential cutoff is after depth=3.

* countNodes: This operates on ASTs gathered from the Racket compiler when processing
large, real programs. The benchmark simply counts the number of
nodes in a tree.

For our implementation, we store the ASTs on disk in a serialized format
which is read using a single mmap call.

All others parse the text files before operating on them.

To ensure an apples-to-apples comparison, we do not measure the time required
to parse the text files.

The size of the text file is 1.2G, and that same file
when serialized for our implementation is 356M.

The AST has around 100M nodes in it.

The sequential cutoff is after depth=9.

* constFold:
Run the constFold function shown in
fig:example1-both on an artificially generated syntax-tree,
which is a balanced binary tree of Plus expressions,
with a Lit as a leaf.

The height of the syntax-tree is 26, the sequential cutoff is after depth=8.

* mergeSort:

An in-place parallel merge sort,
which bottoms out to a sequential quick sort
when the array contains less than 8192 elements.

For our implementation, we use the qsort function from the C standard library to
sort small arrays.

The Haskell implementation is taken from Kuper et al's artifact
accompanying their paper <cit.>,
and it makes an FFI call to a sequential quick sort written in C.

and OCaml bottom out to a sequential quick sort implemented in their source language.

The input array contains 8M randomly generated floating point numbers.

§.§ Results: Parallel versus Sequential Gibbon

Gibbon          4cOurs

Benchmark     $T_s$        $T_1$     O     $T_{48}$     S

fib     12.8        12.8     0     0.31     41.3

4.69        4.69     0     0.11     42.6

buildKdTree     2.33        2.67     14.6     0.22     10.6

countCorr     1.46         1.47     0.68     0.044     33.2

allNearest     1.0        1.01     1     0.023     43.5

barnesHut     3.21        3.21     0     0.074     43.4

coins     3.04        3.13     3     0.096     31.7

countnodes     0.21        0.21     0     0.006     35.0

constFold     1.78        1.78     0     0.16     11.1

x86-compiler     1.08        1.08     0     0.041     26.3

mergeSort     1.58        1.60     1.27     0.039     40.5

average     -        -     1.28     -     29.5

$T_s$ is the run time of Sequential Gibbon.

$T_1$ and $T_{48}$ are the run times of Parallel Gibbon
on 1 thread and on 48 threads respectively.

$O$ is the single-thread percentage overhead: $O = (T_1 - T_s) / T_s * 100$.

$S$ is the 48-thread speedup: $S = T_s / T_{48}$.

Speedups relative to Sequential Gibbon.

Figures <ref> and <ref> show the results
of comparing performance of benchmarks compiled using our

implementation, labeled “Ours”, relative to Sequential Gibbon.

The quantities in the table can be interpreted as follows.

Column $T_s$ shows the run time of a sequential program.
which serves the purpose of a sequential baseline.

$T_1$ is the run time of a parallel program on a single thread, and
$O$ the percentage overhead relative to $T_s$, calculated as
$((T_1 - T_s) / T_s) * 100$.

$T_{48}$ is the run time of a parallel program on 48 threads and
$S$ is the speedup relative to $T_s$, calculated as $T_s / T_{48}$.
$R$ is the number of additional regions created to enable
parallel allocations, calculated as $R_{48} - R_{s}$.

For a majority of benchmarks, the overhead is under 3%,
and the speedups range between 31.7$\times$ and 43.5$\times$.

These speedups match, or in cases such as barnesHut and allNearest,
exceed those of optimized implementations that have been analyzed on
similar machines <cit.>.

With respect to the difference in speedups between different benchmarks,
we see the expected relationship among them which reflects their memory access patterns.

Compute-bound benchmarks such as fib scale very well,
whereas benchmarks such as constFold and buildKdTree
can become memory bound, and do not scale over a certain number of cores[For example, a simple parallel dot-product computation (in Cilk) has a similar linear access pattern and low arithmetic intensity to constFold, and it achieves only a 6X speedup on this same machine.].

With respect to buildKdTree, a significant portion of its total running time is
spent in sorting the points at each node.

We observed that our mergeSort doesn't scale well on small inputs,
and since buildKdTree performs a series of smaller and smaller sorts,
it eventually runs into this, leading to lower scalability.

But its high overhead (14.6%) and low speedup (10.6$\times$)
are in the same ballpark as an optimized C implementation
which <cit.> analysed on a 32-core machine.

Figures <ref>
and <ref> (given in the Appendix)

and 15 (given in the Appendix of the extended version <cit.>)

show that , GHC and OCaml also scale similarly.

Overall, these results show that our technique is able to handle
parallelism in a mostly-serialized data representation effectively.

§.§.§ Fragmentation:

Traversals on a serialized heap are efficient because serialization minimizes
pointer-chasing and maximizes data locality.

But the heap produced by running intra-region allocations in parallel is
fragmented, which can affect the performance of subsequent traversals that
consume this heap, due to additional pointer dereferences and worse locality.

To measure this downstream effect,
we compare the run time of a single-threaded traversal operating
on a sequentially allocated value to that traversal
operating on a value allocated in parallel, which will be fragmented.

Thus, the thing whose run time is being compared—the traversal—stays the same
but it is given inputs that have different levels of fragmentation.

We also measure the amount of fragmentation introduced for parallelism by counting
the number of regions created solely to enable parallel allocations.

fig:fragmentation-results shows the results.

We use a subset of the benchmarks from subsec:benchmarks
whose output is a serialized value (the other benchmarks do not measure
the construction of new values),
and measure the time required to traverse the output.

For example, the benchmark trav(constFold)
constructs an input expression, runs constant folding over it,
and then sequentially traverses the resulting expression
(counts the number of leaves in it),
but the number reported is only the run time of the traversal
and it does not include the time taken to run constFold itself.

Each benchmark sample is the median of 9 runs,
such that each run allocates a value and then traverses it $N$ times,
where $N$ is set high enough to get the total run time over one second,
and the run time of a single traversal is reported.

$T_s$ is the time required to sequentially traverse a sequentially allocated
value, which is the baseline.

We compare against this baseline the performance of traversing
a value allocated in parallel with two levels of fragmentation:
optimum and maximum.

In the optimum setting, the allocators are identical to
those used for measurements reported in fig:gibbon-table.

That is, they control fragmentation by
controlling the granularity of parallelism
(using the thresholds given in subsec:benchmarks)
and are compiled using the region-upon-steal allocation
policy (subsec:parallel-allocations).

$R_{\mathit{opt}}$ is the number of additional regions created to allocate a value in parallel using 48 threads.

For example, the sequential constFold uses a single region
and its parallel version requires 132 additional regions (133 regions total).

$T_{\mathit{opt}}$ is the time required to sequentially traverse the allocated value,
and $O_{\mathit{opt}}$ is the percentage overhead relative to $T_s$, calculated as
$O_{\mathit{opt}} = (T_{\mathit{opt}} - T_s) / T_s * 100$.

In the maximum setting,
the allocators do not control fragmentation at all (no granularity control),
and they are compiled
using the region-upon-spawn allocation policy, which creates a fresh
region for every intra-region allocation task that is spawned.

This setting thus represents the upper bound on the amount of fragmentation that can be
introduced due to parallelism, where the heap essentially degenerates
to a full pointer-based representation.

$R_{\mathit{max}}$, $T_{\mathit{max}}$ and $O_{\mathit{max}}$ are the corresponding
numbers for this fragmentation setting when using 48 threads.

$O_{\mathit{max}}$ is the percentage overhead relative to $T_s$, calculated as
$O_{\mathit{max}} = (T_{\mathit{max}} - T_s) / T_s * 100$.

Seq Alloc.          3cOptimum Fragmentation          3cMaximum Fragmentation

Benchmark     $T_s$        $\;\;\;$ $R_{\mathit{opt}}$     $T_{\mathit{opt}}$     $O_{\mathit{opt}}$        $\;\;\;$ $R_{\mathit{max}}$     $T_{\mathit{max}}$     $O_{\mathit{max}}$

trav()     0.99ms        $\;\;\;$ 341     1.02ms     3.03        $\;\;\;$ 262K     11.45ms     1056.6

trav(buildKdTree)     6.22ms        $\;\;\;$ 31     6.64ms     6.75        $\;\;\;$ 262K     55ms     784.2

trav(coins)     0.35s        $\;\;\;$ 9K     0.37s     5.71        $\;\;\;$ 75M     5.21s     1388.6

trav(constFold)     0.30s        $\;\;\;$ 132     0.32s     6.67        $\;\;\;$ 67M     2.70s     800

trav(x86-compiler)     366.2$\mu s$        $\;\;\;$ 1K     377.5$\mu s$     3.09        $\;\;\;$ 14K     464.3$\mu s$     26.8

geomean     -        $\;\;\;$ -     -     4.74        $\;\;\;$ -     -     476.9

$T_s$ is the time required to sequentially traverse a sequentially allocated value.

$R_{\mathit{opt}}$ is the number of additional regions created to allocate a value in parallel using 48 threads,

$T_{\mathit{opt}}$ is the time required to sequentially traverse it,
and $O_{\mathit{opt}}$ is the percentage overhead of the traversal: $O_{\mathit{opt}} = (T_{\mathit{opt}} - T_s) / T_s * 100$.

$R_{\mathit{max}}$, $T_{\mathit{max}}$ and $O_{\mathit{max}}$ are the corresponding
numbers for a value allocated in parallel using 48 threads with maximum fragmentation.

$O_{\mathit{max}}$ is the percentage overhead relative to $T_s$ calculated as
$O_{\mathit{max}} = (T_{\mathit{max}} - T_s) / T_s * 100$.

Comparing $R_{\mathit{opt}}$ and $R_{\mathit{max}}$,
we see that in the optimum setting most of the allocated heap is still serialized
and uses only a small number of additional regions—less than 0.13% of the maximum— in most cases.

For x86-compiler, this percentage is higher (7.14%) compared to the other benchmarks
because even in the optimum setting this benchmark
does not control the granularity of parallelism,
which is controlled only by the structure of the input
as we discuss in subsec:compiler-case-study.

In this case, the region-upon-steal allocation policy is responsible
for trimming the number of regions from 14K to 1K.

With respect to the run time of the traversal,
the overhead with optimum fragmentation is between 3.03% to 6.75%,
with a geomean of 4.74%.

In addition to fragmentation,
the NUMA memory policy [As described in the experimental setup, the shared memory on this machine is divided into two NUMA nodes and we use 48 threads evenly distributed across both nodes with the default local memory allocation policy.] has a significant impact on the overall overhead
because in the parallel version potentially
of memory accesses are at a non-local NUMA memory node.

If we run the experiment using a single NUMA node (numactl $\;--$membind=0 $\;$ $\;--$physcpubind=1-24,49-71),
the geomean overhead drops to 1.44%,
with a significant reduction in the overheads for buildKdTree (0.96%) and
constFold (2.95%).

In the presence of maximum fragmentation, we see the expected result:
since heap degenerates to a full pointer-based representation,
the traversals are several times slower
and the benefits of using a serialized representation are lost.

This slowdown in traversing a pointer-based representation compared to a serialized one
is consistent with the results given in previous work <cit.>.

Overall, these results show that using the granularity of parallelism to
guide the data representation works well in practice,
and gives us an efficient, mostly-serialized representation.

§.§ Results: Gibbon versus Other Compilers

fig:ours_versus_others shows the results of comparing performance of

our implementation to , OCaml, and GHC.

For each compiler, Column $T_s$ is the run time of a sequential program,
Column $T_{48}$ is the run time of a parallel program on 48 threads,
and an adjacent column to each shows the corresponding speedup (or slowdown) of our implementation
relative to this compiler.

For example, on 48 threads, allNearest is $3.95\times$ faster with our
implementation compared to OCaml.

fig:scaling-subset shows how a subset of benchmarks scale on 48 threads.

The scaling results for the remaining benchmarks
are available in Appendix <ref>.

are available in the Appendix of the extended version <cit.>.

With respect to self-relative comparisons,
on average, we scale similarly to , and better than OCaml or GHC.

Across all benchmarks,
on a single thread our  offers a $1.93\times$, $2.53\times$, and $2.14\times$ geomean speedup compared to , OCaml, and GHC, respectively.

When utilizing 48 cores, our geomean speedup is $1.92\times$, $3.73\times$ and $4.01\times$.

these results show that we start with a faster baseline in the sequential world,
and we're able to preserve the speedups in the parallel as well,
meaning that the use of dense representations
to improve sequential processing performance coexists with scalable parallelism.

The only benchmark for which our implementation is slower compared to others is coins.

This benchmark makes heavy use of linked-list operations
such as cons, head, and tail,
and our implementation uses malloc to allocate memory
for every cons, which is inefficient.

Also, our dense representation currently offers no benefit when building
linked-lists by cons'ing onto existing lists.

All others, , OCaml and GHC, use a copying garbage collector <cit.> allowing them to use a bump-allocator,
making them more efficient than our implementation.

fig:others-benchmark-results in Appendix

Figure 15 in the Appendix of the extended version <cit.>

gives the self-relative performance
results for , OCaml and GHC.

4c          4cOCaml          4cGHC

Benchmark                 $T_s$     s     $T_{48}$     48        $T_s$     s     $T_{48}$     48        $T_s$     s     $T_{48}$     48

fib                 37.4     2.92     1.06     2.93        21.1     1.65     0.50     1.61        31.9      2.5     0.76      2.45

14.5     3.09     0.35     3.18        8.60     1.83     0.25     2.27         12.4     2.64     0.34      3.09

buildKdTree                 7.26     3.11     0.41     1.86        10.9     4.68     1.84     8.36        13.4     5.75     2.21     10.0

countCorr                 10.5     7.19     0.27     6.14        13.9     9.52     0.37     8.41        3.54     2.42     0.15     3.41

allNearest                 2.38     2.38     0.06     2.60        3.01     3.01     0.091     3.95        2.07     2.07     0.068     2.96

barnesHut                 5.05      1.57     0.12     1.62        10.9     3.40     0.44     5.94        4.97     1.55     0.33     4.46

coins                 1.71     0.56     0.05     0.52        1.05     0.34     0.036     0.37        0.82      0.27     0.085      0.88

countnodes                 0.37      1.76     0.019     3.16        0.46      2.19     0.034     5.67         1.45      6.90      0.049     8.16

constFold                 2.36     1.32     0.23     1.44        17.7     9.94     2.23     13.9        3.71     2.08     0.64     4.00

x86-compiler                 1.34     1.24     0.042      1.02        1.20     1.11     0.09     2.20        2.34     2.16     0.44     10.7

mergeSort                 1.74     1.10     0.047     1.20        3.83     2.42     0.19     4.87         2.74      1.73     0.16      4.10

geomean                 -     $1.93\times$     -     $1.92\times$         -     $2.53\times$     -     $3.73\times$        -     $2.14\times$      -      $4.01\times$

Comparison of Ours with , OCaml, and GHC —

execution time in seconds,
and ratios to Ours.

$T_s$ is the run time of a sequential program, and
$T_{48}$ is the run time of a parallel program on 48 threads.

Speedups on 1-48 threads relative to the fastest sequential baseline,
which is Sequential Gibbon for these three benchmarks.

§.§ Results: x86-Compiler Case Study

As an example of a complex benchmark which performs multiple traversals over
different datatypes, we implement a subset of
a compiler drawn from a university course <cit.>.

Our version compiles to x86, from a source language that supports
integers and arithmetic and comparison operations on them,
booleans and operations such as and and or,
and a conditional expression, if.

To compile this high level language, we first translate it to an
intermediate language similar to C,
in which the order of evaluation is explicit in its syntax.

The compiler is written in a nanopass style <cit.>,
and is made up of five passes:

* typecheck type checks the source program,

* uniqify freshens all bound variables to handle shadowing,

* explicateControl translates to an
intermediate language similar to C,

* selectInstructions generates x86 code which has variables in it,

* and assignHomes maps each variable to a location on the stack.

The input to this benchmark is a synthetically generated, balanced syntax-tree
with conditional expressions at the top, followed by a sequence of let bindings.

The structure of the input program is used to control the granularity of parallelism.

The first three passes process the branches of conditionals in parallel,
and subsequent ones process every block of instructions in parallel.

On this compiler benchmark, Parallel Gibbon offers a
$1.24\times$, $1.11\times$, and $2.16\times$ speedup on a single thread, and
$1.02\times$, $2.20\times$ and $10.7\times$ speedup when utilizing 48 threads,
compared to , OCaml, and GHC, respectively.

Note that most of the run time and
also the self-relative parallel speedup of this benchmark is due to assignHomes.

The first four passes of the compiler have a linear memory access pattern
and low arithmetic intensity, much like constFold.

The passes inspect the input expression,
perform inserts or lookups on shallow environments
(which only contain entries for variables that are in scope at a point),
and then allocate the output.

But assignHomes works in a different way.

Since it needs to assign a unique stack location to every variable occurring in an expression,
it constructs an environment containing all variables in
the expression (as opposed to just those in scope at a point),
and then performs repeated lookups on it to
rewrite variable occurrences with stack location references.

This environment is significantly larger than those used by other passes,
making assignHomes much more work-intensive and suitable for parallel execution.

Here we have only taken the first step towards developing an efficient parallel compiler,
and there is ample opportunity for further investigation in this area.

In the future, we plan to expand the compiler's source language to include
constructs such as top-level function definitions and modules which
are a source of parallelism in many real compilers.

§ RELATED WORK

The most closely related work to this paper is, of course, Vollmer et al.'s LoCal <cit.>, which was summarized in Section <ref>. As discussed there,

Vollmer et al.'s treatment only provided sequential semantics, while this paper
extends those semantics to incorporate parallelism.

This work, and LoCal, are related to several HPC approaches to serializing recursive trees into flat buffers for efficient traversal <cit.>. Notably, these approaches must maintain the ability to access the serialized trees in parallel, despite the elimination of pointers internal to the data structure, or risk sacrificing their performance goals. The key distinction that makes enabling parallelism in the HPC setting “easier” than in our setting is that these approaches are application-specific. The serialized layouts are tuned for trees whose structure and size are known prior to serialization, and the applications that consume these trees are specially-written to deal with the application-specific serialization strategies. Hence, offsets are either manually included in the necessary locations, or are not necessary as tree sizes can be inferred from application-specific information.

Work on more general approaches for packing recursive structures into buffers includes Cap'N Proto <cit.>, which attempts to unify on-disk and in-memory representations of data structures, and Compact Normal Form (CNF) <cit.>. Neither of these approaches have the same design goals as  and :

both Cap'N Proto and CNF preserve internal pointers in their representations, eliding the problem of parallel access by invariably paying the cost (in memory consumption and lost spatial locality) of maintaining those pointers. We note that Vollmer et al. showed that 's representations enable faster sequential traversal than either of those two approaches <cit.>, and Section <ref> shows that our approach is comparable in sequential performance to  despite also supporting parallelism.

There is a long line of work on flattening and nested data parallelism, where parallel computations over irregular structures are flattened to operate over dense structures <cit.>. However, these works do not have the same goals as ours. They focus on array
data, generating parallel code, and data layouts that promote data parallel access to the elements of the structure, rather than selectively trading off between parallel access to structures and efficient sequential access.

Efficient automatic memory management is a longstanding challenge for parallel functional

Recent work has addressed scalable garbage collection by structuring
the heap in a hierarchy of heaps, enabling task-private collections
<cit.>. There is work proposing a
split-heap collector that can handle a parallel lazy
language <cit.> and a strict
one <cit.>, and there is work on a
scalable, concurrent collector <cit.>.

A promising new line of work explores hierarchical heaps for parallel
functional programs <cit.>.

All of these designs focus on a conventional object model for algebraic datatypes that, unlike ,
assume a uniform, boxed representation.

In the future, we plan to investigate how results in these collectors relate to our model,
where objects may be laid out in a variety of ways.

§ CONCLUSIONS AND FUTURE WORK

We have shown how a practical form of task parallelism can be reconciled with
dense data representations.  We demonstrated this result inside a compiler
designed to implicitly transform programs to operate on such dense
representations.  For a set of tree-manipulating programs we considered in
sec:evaluation, this experimental system yielded better performance
than existing best-in-class compilers.

To build on what we have presented in this paper, we plan to explore automatic
granularity control <cit.>; this would remove the
last major source of manual tuning in Gibbon programs,
which already automate data layout optimizations.
Parallel Gibbon with
automatic granularity control would represent the dream of implicitly parallel
functional programming with good absolute wall-clock performance.

While our current approach supports limited examples of data parallelism–friendly data structures beyond trees, such as dense arrays (subsec:parallel-arrays), we plan to further generalize our system by adding additional data structures that capture mutable sparse and dense multi-dimensional data.

We plan to support limited in-place mutation of densely-encoded algebraic data, by adding primitives based on linear types, which we expect to mesh well with the implicitly parallel functional paradigm.

While  already out-performs competing parallel, functional approaches, we expect these additional features will both improve programmability (by relieving the programmer of the burden of granularity control) and performance (by supporting more efficient parallel structures and strategies).

This work was supported in part by nsfNational Science Foundation
awards spx-milindCCF-1725672, spx-ryanCCF-1725679
and spx-milind-twoCCF-1919197, as well as
by the EPSRCEngineering and Physical Sciences Research Council
award epsrc-granuleEP/T013516/1.

We would like to thank our shepherd, Cyrus Omar, as well as the anonymous
reviewers for their suggestions and comments.

§ APPENDIX: SAMPLE GIBBON PROGRAMS

type Point3d = (Float, Float, Float)
– In Gibbon, the Kdtree type will be represented in a dense, mostly-serialized format.
data KdTree = KdLeaf  x :: Float, y :: Float, z :: Float
| KdNode  x :: Float, y :: Float, z :: Float
, total_elems   :: Int   – Number of elements in this node
, split_axis    :: Int   – (0: x, 1: y, 2: z)
, split_value   :: Float
, min :: Point3d, max :: Point3d
, left :: KdTree, right :: KdTree

| KdEmpty

– | Given an array of points, build a KdTree.
mkKdTree :: Array Point3d -> KdTree
mkKdTree axis pts = ...

– | Return query's nearest-neighbor.
nearest :: KdTree -> Point3d -> Point3d
nearest tr query =
case tr of
KdEmpty -> (0.0,0.0,0.0)
KdLeaf x y z -> (x,y,z)
KdNode x y z _total_elems split_axis _split_value _min _max left right ->
let pivot = (x,y,z)
tst_query = get_coord split_xis query
tst_pivot = get_coord split_xis pivot
in if tst_query < tst_pivot
then find_nearest pivot query tst_pivot tst_query left right
else find_nearest pivot query tst_pivot tst_query right left

find_nearest :: Point3d -> Point3d -> Float -> Float -> KdTree -> KdTree -> Point3d
find_nearest pivot query tst_pivot tst_query good_side other_side =
let best0 = nearest good_side query
candidate1 = least_dist query best0 pivot
– Whether the difference between the splitting coordinate of the query point and current node
– is less than the distance (overall coordinates) from the search point to the current best.
nearest_other_side = tst_query - tst_pivot
in if (nearest_other_side * nearest_other_side) <= (dist query candidate1)
then let candidate2 = nearest other_side query
in least_dist query candidate1 candidate2
else candidate1

– | Return the point that is closest to a.
least_dist :: Point3d -> Point3d -> Point3d -> Point3d
least_dist a b c =
let d1 = dist a b
d2 = dist a c
in if d1 < d2 then b else c

– | Maps an array of points to an array of their nearest neighbor.
allNearest :: KdTree -> Array Point3d -> Array Point3d
allNearest tr ls = map (-> nearest tr p) ls

A program to compute nearest-neighbors written in Gibbon's front-end language (Haskell).

– | Compute the nth fibonacci number, in parallel.
parfib :: Int -> Int -> Int
parfib cutoff n = if n <= 1
then n
else if n <= cutoff
then seqfib n
else let (x,y) = (parfib cutoff (n-1)) @@
(parfib cutoff (n-2))
in x + y

– | Parallel 'buildTreeHvyLf'.
buildTreeHvyLf :: Int -> Int -> Tree
buildTreeHvyLf cutoff i = if i <= 0
then Leaf (seqfib 20)
else if i <= cutoff
then buildTreeHvyLf_seq i
else let (x,y) = (buildTreeHvyLf cutoff (i-1)) @@
(buildTreeHvyLf cutoff (i-1))
in Node i x y

– ————————————–

type Point3d = (Float, Float, Float)

– In Gibbon, the Kdtree type will be represented in a dense, mostly-serialized format:
data KdTree = KdLeaf  x :: Float, y :: Float, z :: Float
| KdNode  x :: Float, y :: Float, z :: Float
, total_elems   :: Int   – Number of elements in this node
, split_axis    :: Int   – (0: x, 1: y, 2: z)
, split_value   :: Float
, min :: Point3d, max :: Point3d
, left :: KdTree, right :: KdTree

| KdEmpty

– | Maps an array of points to an array of their nearest neighbor.
allNearest :: KdTree -> Array Point3d -> Array Point3d
allNearest tr ls =
– parallel map with a chunk-size of 1024.
par_map 1024 (-> nearest tr p) ls
nearest :: KdTree -> Point3d -> Point3d
nearest = ...

Programs for fib,  and
allNearest in Gibbon's front-end language (Haskell).

§ APPENDIX: FULL EVALUATION DETAILS

Speedups relative to the fastest sequential baseline, which is Sequential Gibbon
for all benchmarks except coins, in which case sequential GHC is fastest.

In sec:evaluation, we presented the results for , OCaml, and GHC
by showing speedups/slowdowns of our implementation relative to them.

In this section, we give the full evaluation results.

To make this section somewhat self-contained, we also include a copy of
Figure <ref>, which compares the performance of sequential
and parallel Gibbon.

fig:others-benchmark-results shows the self-relative comparisions
for , OCaml and GHC.

The quantities in the table can be interpreted as follows.

Column $T_s$ shows the run-time of a sequential program,
which serves the purpose of a sequential baseline.

$T_1$ is the run-time of a parallel program on a single thread, and
$O$ the percentage overhead relative to $T_s$,
calculated as $((T_1 - T_s) / T_s) * 100$.

$T_{48}$ is the run-time of a parallel program on 48 threads and
$S$ is the speedup relative to $T_s$, calculated as $T_s / T_{48}$.

These comparisions are self-relative, meaning that they compare sequential  to
parallel , sequential OCaml to parallel OCaml, and sequential GHC to parallel GHC.

With respect to self-relative comparisons,
on average, we scale similarly to , and better than OCaml or GHC,
and the single-thread overhead across all four compilers is comparable to each other.

fig:scaling-all shows speedups on 1-48 threads
relative to the fastest sequential baseline, which is Sequential Gibbon
for all benchmarks except coins, for which GHC is fastest.

A copy of fig:gibbon-table which compares performance of
sequential and parallel Gibbon.

Execution time in seconds,
self-relative overheads on a single thread (Columns 3, 8 and 13)
and self-relative speedups on 48 threads (Columns 5, 10 and 15).

$T_s$ is the run-time of a sequential program.

$T_1$ and $T_{48}$ are the run-times of a parallel program
on 1 thread and on 48 threads respectively.

$O$ is the single-thread percentage overhead: $O = (T_1 - T_s) / T_s * 100$.

$S$ is the 48-thread speedup: $S = T_s / T_{48}$.

§ APPENDIX: FORMALISM

This section contains:

* typing rules for  (subsec:appendix-typing-rules),

* a complete version of the dynamic semantics (subsec:appendix-dynamic-semantics),

* definitions of all metafunctions used in the formalism (subsec:appendix-metafunctions),

* well-formedness judgments for various elements of the formal model (subsec:well-formedness-judgments),

* and the complete proof of type-safety for

§.§ Typing rules for

Our type system for  requires some substantial extensions
to the original type system given by <cit.>.

These extensions address the need to handle multi-task configurations,
which require a number of new typing environments and rules.

Before we present these extensions, we recall the typing rule
for the configuration of a single task, which is mostly unchanged from
the original.

\[ \TENV;\SENV;\CENV;\AENV;\NENV \vdash \AENV'; \NENV'; \EXPR : \hTYP \]

The context for this judgement includes five different environments.
First, $\TENV$ is a standard typing environment.
Second, $\SENV$ is a store-typing environment, mapping
materialized symbolic locations to their types. That is, every location in $\SENV$ has been written and contains a value of type $\SENV(l^r)$.
Third, $\CENV$ is a constraint environment, keeping
track of how symbolic locations relate to each other.
Fourth, $\AENV$ maps each region in scope to a location, and is used to symbolically
track the allocation and incremental construction of data structures;

Finally, $\NENV$ is a nursery of all symbolic locations that have been allocated,
but not yet written to.

Both $\AENV$ and $\NENV$ are threaded through the typing
rules, also occuring in the output of the judgement, to the right of the

An additional typing rule for type checking an in-flight data constructor.

Let us first consider the rule  given in fig:static-semantics.

It starts by ensuring that the tag being written, and all the fields have the
correct type.

Along with that, the locations of all the fields of the constructor must
also match the expected constraints.

That is, the location of the first field
should be immediately after the constructor tag, and there should be
appropriate $\mathit{after}$ constraints for other fields in the
location constraint environment.

To indicate that the tag has been written, the allocation environment is extended,
and the location $\loc$ is removed from the nursery,
to prevent multiple writes to a location.

However, if any fields of the constructor have evaluated to an ivar,
the tag is not written to the store ().

The rule  handles this case.

It does not extend the allocation environment, and also keeps the location $\loc$
in the nursery, so that a constructor tag may be written at this location
in the future, once this task has synchronized with those
allocating the fields.

This additional typing rule is necessary to satisfy a requirement of
the Top Level Preservation lemma (<ref>).

To generalize our typing rules to handle multi-task configurations, we
introduce new environments for variables $\TENVMAP$, store
typing $\SENVMAP$, allocation constraints $\CENVMAP$, allocation
pointers $\AENVMAP$, and nurseries $\NENVMAP$.

These environments extend their counterparts in the sequential
type system, and are needed to track state on a per-task

The precise typing rules to type check a parallel task $\TASKVAR$, and
a set of parallel tasks $\TASKSET$ are given in
the fig:appendix-static-semantics-parallel.

A parallel task $\TASKVAR$ is well-typed if its target expression
$\EXPR$ is well-typed, using the original  typing rules, and
a task set $\TASKSET$ is well-typed if all tasks in in it are

_1 ↦_1,   …  , _n ↦_n

_1 ↦_1,   …  , _n ↦_n

_1 ↦_1,   …  , _n ↦_n

_1 ↦_1,   …  , _n ↦_n

_1 ↦_1,   …  , _n ↦_n

Extended grammar of  for static semantics.

A copy of the typing rules given in fig:static-semantics-parallel.

A copy of the typing rules for  given in <cit.>

A copy of remaining typing rules for  given in <cit.>

§.§ Dynamic semantics rules for

Figures <ref> and <ref> show
the complete dynamic semantics of .

These rules also appear in the main body of the paper,
but we include their copies here to make the appendix somewhat self-contained.

The driver which runs a  program initially loads all data
types, functions, type checks them, and if successful, then seeds the
$Function$, $\typeofcon$, and $\typeoffield$ environments.

Let $\EXPR_0$ be the main expression.

If $\EXPR_0$ type checks with respect to the  rule, then
the main program is safe to run.

The initial configuration for the machine is a single task,
$\taskconfig{\hTYP}{\concreteloc{\reg}{0}{}}{\emptyset;\set{\loc \mapsto \concreteloc{\reg}{0}{}};\EXPR_0}$,

and the program can start taking evaluation steps from this initial configuration.

This configuration can be constructed automatically in a
straightforward way.

A complete version of dynamic semantics rules (sequential transitions).

Copy of dynamic semantics rules (parallel transitions), given in fig:dynamic-parallel.

§.§ Definitions of metafunctions

In the following, we define various metafunctions used in our formal model.

§.§.§ Merging task memories

We merge two stores by merging the heaps of all the regions that are
shared in common by the two stores, and then by combining with all
regions that are not shared.

We merge two heaps by taking the set of the all the heap values at
indices that are equal, and all the heap values at
indices in only the first and only the second heap.

The merging of location maps follows a similar pattern, but is slightly
complicated by its handling of locations that map to ivars.

In particular, for any location where one of the two location maps
holds an ivar and the other one holds a concrete index, we assign
to the resulting location map the concrete index, because the concrete
index contains the more recent information.

Metafunctions for merging task memories.

§.§.§ End-Witness judgement

The end-witness provides a naive computational interpretation
of the process for finding the index one past the end of a
given concrete location, with its given type.

This rule is mostly the same as the one given for the original, sequential ,
but includes an additional case for handling indirection pointers.

To compute the end-witness of an indirection pointer,
the judgement first reads the address $\concreteloc{\reg'}{\ind'_s}{}$ which is written
at $\concreteloc{\reg}{\ind_s}{}$,
and returns the end-witness of the value allocated at $\concreteloc{\reg'}{\ind'_s}{}$.

Case (A) $\ewitness{\TYPC}{\concreteloc{\reg}{\concreteind{\ind_{s}}}{}}{\STOR}{\concreteloc{\reg}{\concreteind{\ind_{e}}}{}}$:

*  $\STOR(\reg)(\ind_s) = \DC'$   such that

$\; \DATA\;\TYPC = \overharpoon{\DC_1 \; \overharpoon{\sTYP}_1\;} \; | \; \ldots \; | \; \DC' \; \overharpoon{\sTYP}' \; | \; \ldots \; | \; \overharpoon{\DC_m \; \overharpoon{\sTYP}_m\;}$

*  $\overharpoon{\concreteind{w_0}} = \concreteind{\ind_s}+1$

$\ewitness{\overharpoon{\TYP'_1}}{\concreteloc{\reg}{\overharpoon{\concreteind{w_0}}}{}}{\STOR}{\concreteloc{\reg}{\overharpoon{\concreteind{w_1}}}{}} \wedge$

where $\concreteind{\indj} \in \set{1,\ldots,n-1} ; n = | \overharpoon{\TYP'} |$

$\ind_e = \overharpoon{\concreteind{w_n}}$

Case (B) $\ewitness{\TYPC}{\concreteloc{\reg}{\concreteind{\ind_{s}}}{}}{\STOR}{\concreteloc{\reg'}{\concreteind{\ind'_{e}}}{}}$:

* $\STOR(\reg)(\ind_s) = \indirection{\reg'}{\concreteind{\ind_s'}}$

* $\ewitness{\TYPC}{\concreteloc{\reg'}{\concreteind{\ind_{s}'}}{}}{\STOR}{\concreteloc{\reg'}{\concreteind{\ind_{e}'}}{}}$

The end-witness rule.

§.§.§ Linking fields of a data constructor

Given a store $\STOR$, a location map $\MENV$, and the addresses of the
$n^{th}$ and $(n+1)^{th}$ fields of a data constructor $\DC$,

this metafunction conditionally establishes a link between these fields.

If the location map $\MENV$ maps the symbolic location of the $(n+1)^{th}$ field,
$\locreg{\loc_2}{\reg_1}$, to an indirection pointer $\indirection{\reg_2}{\ind_2}$,
it means that these fields were computed in parallel with each other,
and thus would have been allocated into separate regions.

To link such fields, we use the end-witness judgement to compute an address
$\concreteloc{\reg_1}{\ind_e}{}$ which is one past the end of the $n^{th}$ field,
and we then write an indirection pointer pointing to the starting address of the $(n+1)^{th}$
field at $\concreteloc{\reg_1}{\ind_e}{}$.

This establishes the desired link.

If the fields have been allocated into the same region, we do not have to link them,
and the store $\STOR$ is returned unchanged in this case.

A precondition for using this metafunction is that the $n^{th}$ field must be fully

\[
\begin{array}{lcl}
\tie(\STOR,\MENV,\TYP_1,\concreteloc{\reg_1}{\concreteind{\ind_1}}{\loc_1}, \concretelocvar^{\loc_2}) = \STOR \cup \set{\reg_1 \mapsto (\concreteind{\ind_e} \mapsto \indirection{\reg_2}{\concreteind{\ind_2}})} \\
\text{where} \;\; (\locreg{\loc_2}{\reg_1} \mapsto \concreteloc{\reg_1}{\indirection{\reg_2}{\concreteind{\ind_2}}}{}) \in \MENV
\; \text{and} \; \ewitness{\TYP_1}{\concreteloc{\reg_1}{\concreteind{\ind_1}}{}}{\STOR}{\concreteloc{\reg_1}{\concreteind{\ind_{e}}}{}}\\\\
\tie(\STOR,\MENV,\TYP_1,\concreteloc{\reg_1}{\ind_1}{\loc_1}, \concretelocvar^{\loc_2}) = \STOR \\
\text{where} \;\; (\locreg{\loc_2}{\reg_1} \mapsto \concreteloc{\reg_1}{\indirection{\reg_2}{\concreteind{\ind_2}}}{}) \notin \MENV
\end{array}
\]

Metafunction for linking fields of a data constructor.

§.§.§ Derefrencing indirections in $\MENV$

If a location $\loc$ maps to an indirection pointer $\indirection{\reg'}{\ind}$ in $\MENV$,
it is derefrenced by returning the address $\concreteloc{\reg'}{\ind}{}$.

Otherwise, the mapping contained in $\MENV$ is returned unchanged.

\[
\begin{array}{l}
\maplookupone{\MENV}{\loc} = \concreteloc{\reg}{\indbef{\indj}}{} \;\; \text{where}
\begin{array}{l}
(\loc \mapsto \concretelocvar) \in \MENV(\loc) \\
\concreteloc{\reg}{\indbef{\indj}}{} = \followinm(\MENV, \concretelocvar)
\end{array} \\\\
\followinm(\MENV,\concreteloc{\reg}{\indirection{\reg'}{\concreteind{\ind}}}{}) = \concreteloc{\reg'}{\concreteind{\ind}}{} \\
%% \followinm(\MENV,\concreteloc{\reg}{\indbef{\ind}}{}) = \concreteloc{\reg}{\indbef{\ind}}{}
\followinm(\MENV,\concreteloc{\reg}{\concreteind{\ind}}{}) = \concreteloc{\reg}{\concreteind{\ind}}{} \\
\followinm(\MENV,\concreteloc{\reg}{\indivar{\ivarid}}{}) = \concreteloc{\reg}{\indivar{\ivarid}}{}
\end{array}
\]

§.§.§ Other global environments and metafunctions

* $Function(f)$: An environment that maps a function $f$ to its definition $\FD$.

* $Freshen(\FD)$: A metafunction that freshens all bound variables in function definition
$\FD$ and returns the resulting function definition.

* $TypeOfCon(\DC):$ An environment that maps a data constructor to its type.

* $TypeOfField(\DC,i)$: A metafunction that returns the type of the i'th field
of data constructor $\DC$.

* $ArgTysOfConstructor(\DC)$: An environment that maps a data constructor to its field types.

* $\allocptr{\reg}{\STOR}$ = $\max(\set{-1} \cup \set{ \indj \; | \; {(\reg \mapsto (\indj \mapsto \DC)) \in \STOR}})$: A metafunction that returns the highest allocated address in the store,
or -1 if nothing has been allocated yet.

* $\isval{\EXPR}$: A metafunction that checks if an expression is a value or not.

* $Ivars(\EXPR)$: A metafunction that yields the set of ivars that occur in the term $\EXPR$.

* $ \singlewriter{\TASKSET}{\hTYP}{\indivar{\ivarid}} =
|\set{\taskconfig{\hTYP}{\concreteloc{\reg}{\indivar{\ivarid}}{\loc}}{\STOR;\MENV;\EXPR} \; | \; \exists_{\STOR,\MENV,\EXPR} . \taskconfig{\hTYP}{\concreteloc{\reg}{\indivar{\ivarid}}{\loc}}{\STOR;\MENV;\EXPR} \in \TASKSET}| = 1

A metafunction that checks if there is exactly one task $\TASKVAR \in \TASKSET$
which can supply a value of type $\hTYP$ for $\indivar{\ivarid}$.

* :
A metafunction that returns a unique task $\TASKVAR \in \TASKSET$
which can supply a value of type $\hTYP$ for $\indivar{\ivarid}$
if it exists, or returns -1 otherwise.

* $\taskcomplete{\taskconfig{\hTYP}{\concretelocvar}{\STOR;\MENV;\EXPR}} = \isval{\EXPR}$:
A metafunction that checks whether a task has evaluated to a value.

* $deepSupersetEqS(\SENVMAP_1, \SENVMAP_2) = \SENVMAP_1 \supseteq \SENVMAP_2 \vee
( (\concretelocvar \mapsto \SENV_2) \in \SENVMAP_2 \Rightarrow
(\concretelocvar \mapsto \SENV_1) \in \SENVMAP_1 \wedge \SENV_1 \supseteq \SENV_2
A metafunction that checks if the first argument is a deep superset of the second.

In other words, the first argument can contain a mapping $(\concretelocvar \mapsto \SENV)$
which is not present in the second one and thus be a super set at the outer level.

Or a specific mapping within the first argument can be a super set of the corresponding
mapping within the second, and be a super set at an inner level.

Note that it uses an inclusive-or, and both these conditions may be simultaneously true.

* $deepSupersetEqC(\CENVMAP_1, \CENVMAP_2)$:
A metafunction identical to $deepSupersetEqS$, but for $\CENVMAP$.

* $a \xor b = (a \wedge \neg b) \vee (\neg a \wedge b)$:
A metafunction for the exclusive-or logical operator.

§.§ Well-formedness judgments

In this section we present certain well-formedness criteria for
various elements of the formal model.

Some of these are similar to the corresponding judgments for sequential  given
in <cit.>,
but they are extended to handle ivars, and indirections in the location map and store.

We give an additional judgement to check the well-formedness of the set of
tasks executing in a parallel machine.

Because there are many requirements specified inside the various
well-formedness judgments, we introduce notation for referring
to requirements individually.

For example, the notation
refers to the judgement

specified in Section <ref>,
and in that judgement, rule number <ref>.

§.§.§ Well-formedness of a task set

This judgement specifies certain invariants that should hold
for all tasks executing in a parallel machine
for the task set to be well-formed.

Rule <ref> specifies that for all ivars referenced in an
expression being computed by a certain task,

there is a corresponding ivar in the location map,

and there is exactly one other task in the task set which supplies a
well-typed value for that ivar.

Rule <ref> references a separate judgement for well-formedness of the
store with respect to the location map of a parallel task.

Judgement form

$\SENVMAP;\CENVMAP;\AENVMAP;\NENVMAP \storewftasks{\TASKSET}$

$\forall \taskconfig{\hTYP}{\concretelocvar{}}{\STOR;\MENV;\EXPR} \in \TASKSET.$

\SENV = \SENVMAP(\concretelocvar) ; \;
\CENV = \CENVMAP(\concretelocvar) ; \;
\AENV = \AENVMAP(\concretelocvar) ; \;
\NENV = \NENVMAP(\concretelocvar)

*  $
\concreteloc{\reg}{\indivar{\ivarid}}{\loc} \in Ivars(\EXPR) \wedge
\emptyset;\SENV;\CENV;\AENV;\NENV \vdash \AENV' ; \NENV' ; \concreteloc{\reg}{\indivar{\ivarid}}{\loc} : \hTYP' \Rightarrow\\
(\locreg{\loc}{\reg} \mapsto \concreteloc{\reg}{\indivar{\ivarid}}{\loc}) \in \MENV \wedge
\singlewriter{\TASKSET}{\hTYP'}{\indivar{\ivarid}}

*  $\storewf{\SENV}{\CENV}{\AENV}{\NENV}{\TASKSET}{\MENV}{\STOR}$

§.§.§ Well-formedness of a store

Judgement form

The well-formedness judgement for a parallel task's
store specifies the valid layouts of the store by using the location
map and the various environments from the typing judgement.

Rule <ref> specifies that, for each location $\locreg{\loc}{\reg}$
in the store-typing environment,
there is a corresponding address in the location map.

There are two possible ways in which the value at location $\locreg{\loc}{\reg}$
may be allocated — (1) sequentially, by the current task, or
(2) in parallel, by a different task.

The first disjunct holds when the value is allocated sequentially by the current task.

In this case, the address in the location map is a concrete index,
and it satisfies a corresponding end-witness judgement.

Otherwise, the second disjunct holds.

In this case, the address is an ivar,
there is exactly one task which allocates a value at this ivar,
its location map contains a concrete index as location $\locreg{\loc}{\reg}$'s address,
and if it has evaluated to a value, the concrete index satisfies
a corresponding end-witness judgement.

Note that these disjuncts are connected with an exclusive-or, and only of them
can hold at a time.

Rules <ref> and <ref> reference the judgments for well-formedness concerning
in-flight constructor applications (sec:well-formedness-constructors) and correct allocation in
regions (sec:well-formedness-allocation), respectively.

Finally, Rule <ref> specifies that the nursery and store-typing environments reference
no common locations, which is a way of reflecting that each location is either in the process
of being constructed and in the nursery, or allocated and in the store-typing environment, but
never both.

*  $\mapstoreconsistency{}$

*  $\storewfcfa{\CENV}{}{\MENV}{\STOR}$

*  $\storewfca{\AENV}{\NENV}{}{\MENV}{\STOR}$

*  $dom(\SENV) \cap \NENV = \emptyset $

§.§.§ Well-formedness of constructor application

Judgement form

The well-formedness judgement for constructor application specifies the various constraints
that are necessary for ensuring correct formation of constructors, dealing with constructor
application being an incremental process that spans multiple  instructions.

Rule <ref> specifies that, if a location corresponding to the
first address in a region is in the constraint environment, then there is a corresponding
entry for that location in the location map.

Rule <ref> specifies that, if a location corresponding to the address one past a constructor
tag is in the constraint environment, then there are corresponding locations for the address
of the tag and the address after it in the location map.

Rule <ref> specifies that, if a location corresponding to the address
one past after a fully allocated constructor application is in the constraint environment,
then there are corresponding locations
for the address of the start of that constructor application, and
for the address one past the constructor application in the location map.

There are two possible ways in which the values at locations $\locreg{\loc'}{\reg}$
and $\locreg{\loc}{\reg}$ may be allocated —
(1) sequentially, by a single task, and thus in a single region, or
(2) in parallel with each other, by separate tasks, and thus in separate regions.

The first disjunct holds when the values are allocated sequentially by a single task.

In this case, the starting address of the constructor application is a concrete index,
and an end-witness for it also exists.

The address one past the constructor application is this end-witness.

The second disjunct holds when the values are allocated in parallel by separate tasks.

In this case, the location map $\MENV$ and store $\STOR$ belong to the task
that allocates the value at location $\locreg{\loc}{\reg}$.

The starting address of the constructor application is an ivar,
and the address one past the constructor application is an indirection pointer
pointing to a separate region which has been allocated in the store.

The third disjunct holds when the values are allocated in parallel by separate tasks,
but after those tasks have synchronized with each other, and their memories merged

The merge resets the starting address of the constructor application back to
a concrete index, and an end-witness for it now exists.

The store contains an indirection pointer at this end-witness which points
to the start of the region that contains the value at location $\locreg{\loc}{\reg}$.

In other words, a link between the values at locations $\locreg{\loc'}{\reg}$ and
$\locreg{\loc}{\reg}$ exists.

The address one past the constructor application is the corresponding indirection pointer.

Note that these disjuncts are connected with an exclusive-or, and only of them
can hold at a time.

*  $\wfconstrstart{}$

*  $\wfconstrtag{}$

*  $\wfconstrafter{}$

§.§.§ Well-formedness concerning allocation

Judgement form

The well-formedness judgement for safe allocation specifies the various properties
of the location map and store that enable continued safe allocation, avoiding in particular
overwriting cells, which could, if possible, invalidate overall type-safety.

Rule <ref> requires that, if a location $\locreg{\loc}{\reg}$ is in both the allocation
and nursery environments, i.e., that address represents an in-flight
constructor application, then there is a corresponding location in the location
map and the address of that location is the highest address in the store.

Alternatively, the value at location $\locreg{\loc}{\reg}$ is allocated in parallel by
a separate task, in a separate region,
and its address is the corresponding indirection pointer.

Rule <ref> requires that, if there is an address in the allocation
environment and that address is fully allocated, then the address of that location is the
highest address in the store.

Rule <ref> requires that, if there is an address in the nursery, then
there is a corresponding location in the location map, but nothing at the corresponding
address in the store.

Finally, Rule <ref> requires that, if there is a region that has been
created but for which nothing has yet been allocated, then there can be no addresses
for that region in the store.

*  $ ((\reg \mapsto \locreg{\loc}{\reg}) \in \AENV \wedge \locreg{\loc}{\reg} \in \NENV) \Rightarrow \\
((\locreg{\loc}{\reg} \mapsto \concreteloc{\reg}{\ind}{}) \in \MENV \wedge
%          \ind = \max \set{0} \cup \set{\indj \; | \; \concreteloc{\reg}{\indj}{} \in \MENV} \wedge \\
\ind > \allocptr{\reg}{\STOR})
\xor
(\locreg{\loc}{\reg} \mapsto \indirection{\reg_2}{\ind_2}) \in \MENV

*  $ ((\reg \mapsto \locreg{\loc}{\reg}) \in \AENV \wedge
\, \concreteloc{\reg}{\ind_s}{} = \hat{\MENV}(\locreg{\loc}{\reg}) \wedge
\locreg{\loc}{\reg} \not \in \NENV \wedge
\, \ewitness{\TYP}{\concreteloc{\reg}{\ind_s}{}}{\STOR}{\concreteloc{\reg}{\ind_e}{}}) \Rightarrow
\ind_e > \allocptr{\reg}{\STOR}

*  $ \locreg{\loc}{\reg} \in \NENV \Rightarrow
\concreteloc{\reg}{\ind}{} = \hat{\MENV}(\locreg{\loc}{\reg}) \wedge
(\reg \mapsto (\ind \mapsto \DC)) \not \in \STOR

*  $(\reg \mapsto \emptyset) \in \AENV \Rightarrow
(\reg \mapsto \emptyset) \in \STOR$

§.§ Type-Safety

We state the type-safety theorem as follows:

If        ∅;;;;⊢_taskset ' ; ' ;   ∧  ;;;

and        ^n '

then, either        ∀∈'.

or        ∃  ”.   ' ”.

This theorem states that, if a given task set $\TASKSET$ is well typed
and its overall store is well formed, and if $\TASKSET$

makes a transition to some task set $\TASKSET'$ in $n$ steps,
then either all tasks in
$\TASKSET'$ are fully evaluated or $\TASKSET'$ can take
a step to some task set $\TASKSET''$.

As usual, we prove this theorem by showing progress and preservation.

If        ∅;;;;' ; ' ;

and        ;;;

then        ∀∈.

else        '.

If every $\TASKVAR \in \TASKSET$ has evaluated to a value, we have no further
proof obligations.

Otherwise, the obligation is to show that there is at least one task which
can take a sequential or a parallel step.

By inversion on , and the typing rule given in the premise of this lemma,
we know that all tasks in the task set $\TASKSET$ are well-typed.

Then, by inversion on , we know that the expression $\EXPR$
it is evaluating is also well-typed.

We show that there is at least one $\TASKVAR \in \TASKSET$ which
can take a sequential or a parallel step,

by performing induction on the typing derivation of the expression $\EXPR$
that a task is evaluating.

[, $\; \EXPR = \letpack{\var : \hTYP_1}{\EXPR_1}{\EXPR_2}$]

Because $\EXPR$ is not a value, the proof obligation is to show that there is at least one task which
can take a step. That is, there is a rule in the dynamic semantics whose
left-hand side matches the machine configuration $\TASKSET$.

There are two rules that can match.

By inversion on , the only obligation is to estalish that
$\concretelocvar_1 = \hat{\MENV}(\locreg{\loc_1}{\reg_1})$.

By applying the rule sec:well-formedness-taskswf:task-store-wf for
the well-formedness of the task set given in the premise of this lemma,
we can obtain a well-formedness result for the store and location map used by this task:

We can then perform inversion on the well-formedness of the store,
and apply the rule sec:well-formednesswf:ca to obtain

Finally, we apply sec:well-formedness-allocationwf:impl-write-once
to obtain $\concreteloc{\reg}{\ind}{} = \hat{\MENV}(\locreg{\loc_1}{\reg_1})$.

Thus we have discharged the proof obligation,
and this task can take a parallel step using .

To obtain this result, we use Lemma <ref>
for single thread progress.

There are two preconditions in order to use this lemma:
$\emptyset;\SENV;\CENV;\AENV;\NENV \vdash \AENV';\NENV';\EXPR : \hTYP$, and

The first precondition is already established at the start of the proof,
by performing inversion on , and then on .

The second precondition can be discharged

by performing inversion on the
on the well-formedness of the task set given in the premise
of this lemma, and then applying the rule

[, $\;\EXPR = \datacon{\DC}{\keywd{\locreg{\loc}{\reg}}}{\overharpoon{\VAL}}$]

Because $\EXPR$ is not a value, the proof obligation is to show that there is a task which
can take a step. That is, there is a rule in the dynamic semantics whose
left-hand side matches the machine configuration $\TASKSET$.

There are a single rule that can match.

If any of the fields of the data constructor have evaluated to an ivar,
the only rule that can match is .

By inversion on , the only obligation then is to find a task $\TASKVAR_c$
which supplies a value of that ivar.

To obtain this result we perform inversion on the well-formedness of the task set given in the premise
of this lemma, and apply the rule sec:well-formedness-taskswf:ivar-present.

Thus, we know that exactly one such task $\TASKVAR_c$ exists.

There are two possible states in which the task $\TASKVAR_c$ may be in —
it may have evaluated its expression to a value, or not.

If the former is true, then the rule  matches, and this task
can take a step.

Otherwise, the $\TASKVAR_c$, or one of its child tasks can take a step,
and thus this case.

[, $\;\EXPR = \case{\VAL}{\overharpoon{\pat} : \tyatlocreg{\TYP}{\loc}{\reg}}$]

Because $\EXPR$ is not a value, the proof obligation is to show that there is a task which
can take a step. That is, there is a rule in the dynamic semantics whose
left-hand side matches the machine configuration $\TASKSET$.

There are two rules that can match: , or .

With respect to , it can can be discharged by using similar reasoning
as the  case.

As for , we use Lemma <ref>
for single thread progress like earlier.

The cases for , , , , , , and
use the Lemma <ref>
for single thread progress, and can be discharged by using similar reasoning to
the previous cases.

If        ∅;;;;⊢';';:

then          𝑣𝑎𝑙𝑢𝑒

else        ;;';';'.

The proof is by induction on the typing derivation of $\EXPR$.

[, $\; \EXPR = \letloc{\locreg{\loc}{\reg}}{\afterl{\tyatlocreg{\TYP'}{\loc_{1}}{\reg}}}{\EXPR'}$

Because $\EXPR$ is not a value, the proof obligation is to show that there is a task which
can take a step. That is, there is a rule in the dynamic semantics whose
left-hand side matches the machine configuration $\STOR;\MENV;\EXPR$.

There are two rules that can match: , or

They both have a similar precondition: $\concretelocvar{} = \hat{\MENV}(\locreg{\loc_1}{\reg})$.

To obtain this result, we need to use
rule sec:well-formednesswf:map-store-consistency
of the well-formedness of the store given in the premise of this lemma.

This rule requires that $\SENV(\locreg{\loc_1}{\reg}) = \TYP'$,
which can be obtained by inversion on .

By inversion on
we can establish that either
$\concreteloc{\reg}{\ind}{} = \hat{\MENV}(\locreg{\loc_1}{\reg})$, or
$\concreteloc{\reg}{\indivar{\ivarid}}{} = \hat{\MENV}(\locreg{\loc_1}{\reg})$

The individual requirements for each case are handled by the following case analysis.

* $\concreteloc{\reg}{\ind}{} = \hat{\MENV}(\locreg{\loc_1}{\reg})$

If $\concreteloc{\reg}{\ind}{} = \hat{\MENV}(\locreg{\loc_1}{\reg})$,
the only rule that can match is .

The only remaining obligation is to show that an end-witness $\indj$ for the value
allocated at the address $\concreteloc{\reg}{\ind}{}$ exists:

This can be discharged
by applying the rule sec:well-formednesswf:map-store-consistency.

If $\concreteloc{\reg}{\ind}{} = \hat{\MENV}(\locreg{\loc_1}{\reg})$,
the first disjunct of sec:well-formednesswf:map-store-consistency holds,
and thus discharges our required obligation.

* $\concreteloc{\reg}{\indivar{\ivarid}}{} = \hat{\MENV}(\locreg{\loc_1}{\reg})$

This rule has no remaining obligations, and matches directly, and thus this case.

The cases for , , , , , , ,
are similar to the proof of progress for sequential  given in <cit.>.

If        ∅;;;;⊢_taskset ' ; ' ;

and        ;;;

and        '

then for some       deepSuperSetEqS(', ),
deepSuperSetEqC(', ),
” ⊇',   ” ⊇'.

∅;';';”;” ⊢_taskset ”' ; ”' ; '

and        ';';”;” '.

The proof is by induction on the given derivation of the dynamic semantics.

Let $\SENV = \SENVMAP(\concretelocvar)$,
$\CENV = \CENVMAP(\concretelocvar)$,
$\AENV = \AENVMAP(\concretelocvar)$, and
$\NENV = \AENVMAP(\concretelocvar)$
be the environments corresponding to the task

We instantiate the new environment maps as:

\[
\begin{array}{l}
\SENV' = \SENV \cup \set{\locreg{\loc_1}{\reg_1} \mapsto \hTYP_1} \\
%% \SENVMAP' = \SENVMAP \cup \set{\concretelocvar'_1 \mapsto \SENV, \concretelocvar \mapsto (\SENV \cup \set{\locreg{\loc_1}{\reg_1} \mapsto \hTYP_1})} \\
\SENVMAP' = \SENVMAP \cup \set{\concretelocvar'_1 \mapsto \SENV, \concretelocvar \mapsto \SENV'} \\
\CENVMAP' = \CENVMAP \cup \set{\concretelocvar'_1 \mapsto \CENV} \\
\AENVMAP'' = \AENVMAP' \cup \set{\concretelocvar'_1 \mapsto \AENV} \\
\NENVMAP'' = \NENVMAP' \cup \set{\concretelocvar'_1 \mapsto \NENV}
\end{array}
\]

The task executing the body of the let expression has the target location

In $\SENVMAP'$, we include an updated entry,
$(\concretelocvar \mapsto \SENV')$,
to establish the allocation of the bound expression.

And we extend the environments $\SENVMAP'$, $\CENVMAP'$, $\AENVMAP'$, and $\NENVMAP'$
to contain a entry for $\concretelocvar'_1$,
which is the target location of the task executing the bound expression,
as the incoming environments won't an entry for $\concretelocvar'_1$,
which is a fresh concrete location generated by .

The first obligation is to show that the result $\TASKSET'$ of the evaluation step
is well-typed with respect to the environments $\SENVMAP'$, $\CENVMAP'$, $\AENVMAP''$,
and $\NENVMAP''$.

By inversion on , the obligation then is to show that all tasks in
$\TASKSET'$ are well-typed.

By the typing rule given in the premise of this lemma
and by inversion on ,
we can directly establish the well-typedness of the tasks in $\TASKSET$.

Thus there are only two remaining obligations, namely to show that the two new tasks
spawned by  are well-typed.

* $ \text{Let} \;
\SENV = \SENVMAP(\concretelocvar'_1), \;
\CENV = \CENVMAP(\concretelocvar'_1), \;
\AENV = \AENVMAP(\concretelocvar'_1), \;
\NENV = \AENVMAP(\concretelocvar'_1). \; \text{Obl:} \;
\emptyset;\SENV;\CENV;\AENV;\NENV \vdash_{task} \AENV'; \NENV';\taskconfig{\hTYP_1}{\concretelocvar{}_1'}{\STOR;\MENV;\EXPR_1}$

By inversion on , we see that in order to prove that this task is well-typed,
we must show that the expression $\EXPR_1$
is well-typed with respect to the environments $\SENV$, $\CENV$, $\AENV$, and $\NENV$.

Concretely, the obligation is to show that
$\emptyset;\SENV;\CENV;\AENV;\NENV \vdash \AENV'; \NENV'; \EXPR_1 : \hTYP_1$

We can discharge this obligation as follows.

By the typing rule given in the premise of this lemma, and by inversion on ,
we can establish that the task $\taskconfig{\hTYP}{\concretelocvar{}}{\STOR;\MENV;\EXPR}$ is

By inversion on , we establish that the expression $\EXPR$ is well-typed:
$\TENV;\SENV;\CENV;\AENV;\NENV \vdash \AENV'; \NENV'; \EXPR : \hTYP$.

Then by inversion on , we can obtain the desired result.

* $ \text{Let} \;
\SENV' = \SENVMAP(\concretelocvar), \;
\CENV = \CENVMAP(\concretelocvar), \;
\AENV = \AENVMAP(\concretelocvar), \;
\NENV = \AENVMAP(\concretelocvar). \; \text{Obl:} \;
\emptyset;\SENV';\CENV;\AENV;\NENV \vdash_{task} \AENV'; \NENV';\taskconfig{\hTYP}{\concretelocvar{}}{\STOR;\MENV_2;\EXPR_2'}$

This obligation can be discharged by using similar reasoning as above.

The only difference is that in order for the expression $\EXPR'_2$ to typecheck,
requires the location of bound expression, $\locreg{\loc_1}{\reg_1}$,
to be in the store typing environment.

The environment $\SENV'$ that is instantiated for this task fulfils this requirement,
and thus this obligation is discharged.

The second obligation is to show that the result of the evaluation step
is well-formed.

The individual requirements, labeled
sec:well-formedness-taskswf:ivar-present -
are handled by the following case analysis.

* Case (sec:well-formedness-taskswf:ivar-present):
for each ivar $\concreteloc{\reg}{\indivar{\ivarid}}{}$ in the result $\TASKSET'$,
there exists exactly one task in $\TASKSET'$ which supplies a well-typed value for it.

By the well-formedness of the task set given in the premise of this lemma,
this already holds for all ivars in the task set $\TASKSET$.

The only remaining obligation then is to show that a corresponding unique task exists
for the only new ivar introduced by ,
namely _1_1.

This obligation discharges straightforwardly by inversion on ,
and the typing rule given in the premise of this lemma.

* Case(sec:well-formedness-taskswf:task-store-wf):
the stores of all tasks in the result $\TASKSET'$ are well-formed.

By the well-formedness of the task set given in the premise of this lemma,
we can directly establish the well formedness of stores of all tasks in the task set

Thus there are only two remaining obligations, to show that the stores of the two new tasks
spawned by  are well-formed.

* Case $\taskconfig{\hTYP_1}{\concretelocvar{}_1'}{\STOR;\MENV;\EXPR_1}$;

Since all of the environments remain unchanged in this task,
this case follows immediately by inversion on the well-formedness of the task set
given in the premise of this lemma.

* Case $\taskconfig{\hTYP}{\concretelocvar{}}{\STOR;\MENV_2;\EXPR_2'}$;

and $\storewf{\SENV'}{\CENV}{\AENV'}{\NENV'}{\TASKSET'}{\STOR}{\MENV_2}$:

This task uses the updated environment $\SENV' = \SENV \cup \set{\locreg{\loc_1}{\reg_1} \mapsto \hTYP_1}$, so we must show the store $\STOR$, and location map $\MENV_2$ are well-formed.

The individual requirements, labeled
sec:well-formednesswf:map-store-consistency -
are handled by the following case analysis.

* Case (sec:well-formednesswf:map-store-consistency):