3.2 Disentanglement
We state and prove one of this paper’s key contributions: that
purely functional programs written in HP have the disentanglement
property. Recall that we have defined disentanglement informally
as the property that parallel tasks can only access data allocated
by ancestors. We have formulated the semantics of HP based on
this property by restricting a task to access only the locations that
are allocated in its own and its ancestors’ heaps. To prove that an
arbitrary HP program has the disentanglement property, we first
show that a well-typed program never gets stuck. This familiar type
safety property guarantees that the restrictions placed on the memory
accesses do not cause a program to get stuck (such as by accessing
a memory location in a sibling or descendant heap).