Recent research on parallel functional programming has culminated in a provably
efficient (in work and space) parallel memory manager, which has been
incorporated into the MPL (MaPLe) compiler for Parallel ML and shown to deliver
practical efficiency and scalability. The memory manager exploits a property of
parallel programs called disentanglement, which restricts computations from
accessing concurrently allocated objects. Disentanglement is closely related to
race-freedom, but subtly differs from it. Unlike race-freedom, however, no known
techniques exists for ensuring disentanglement, leaving the task entirely to the
programmer. This is a challenging task, because it requires reasoning about
low-level memory operations (e.g., allocations and accesses), which is
especially difficult in functional languages.

In this paper, we present techniques for detecting entanglement dynamically,
while the program is running. We first present a dynamic semantics for a
functional language with references that checks for entanglement by consulting
parallel and sequential dependency relations in the program. Notably, the
semantics requires checks for mutable objects only. We prove the soundness of
the dynamic semantics and present several techniques for realizing it
efficiently, in particular by pruning away a large number of entanglement
checks. We also provide bounds on the work and space of our techniques.

We show that the entanglement detection techniques are practical by implementing
them in the MPL compiler for Parallel ML. Considering a variety of benchmarks,
we present an evaluation and measure time and space overheads of less than 5% on
average with up to 72 cores. These results show that entanglement detection has
negligible cost and can therefore remain deployed with little or no impact on
efficiency, scalability, and space.