Ernestas Poškus

Technical blog

"We must view with profound respect the infinite capacity of the human mind to resist the introduction of useful knowledge." - Thomas R. Lounsbury

| github | linkedin | twitter |

ansible 2 / elasticsearch 2 / kernel 1 / learning 30 / linux 2 / mnemonics 1 / nginx 1 / paper 30 / personal 5 / research 29 / review 30 / rust 2 / scientific 30 / tools 2 /

Uniqueness and Reference Immutability for Safe Parallelism

WC 501 / RT 3min


Key challenge for concurrent programming is that side-effects (memory operations) in one thread can affect the behavior of another thread.

We wish to restrict, or tame, side-effects to make programs easier to maintain and understand. To do so, we build on reference immutability.

To achieve this we give two novel typing rules, which allow recovering isolated or immutable references from arbitrary code checked in environments containing only isolated or immutable inputs. We provide two forms of parallelism:

Reference Immutability, Uniqueness, and Parallelism

The most obvious use for reference immutability is to control where heap modification may occur in a program, similar to the owner-as-modifier discipline in ownership and universe type systems.

Safe Symmetric Parallelism

Fork-join concurrency is deterministic when neither forked thread interferes with the other by writing to shared memory.

Polymorphism

Any practical application of this sort of system naturally re- quires support for polymorphism over type qualifiers. Otherwise code must be duplicated, for example, for each possible permission of a collection and each possible permission for the objects contained within a collection.

Notes