There is an ongoing effort to provide programming abstractions that ease the burden of
exploiting multicore hardware. Many programming abstractions (e.g., concurrent objects,
transactional memory, etc.) simplify matters, but still involve intricate engineering.
We argue that some difficulty of multicore programming can be meliorated through a
declarative programming style in which programmers directly express the independence
of fragments of sequential programs.
In Veracity, programmers write programs in a familiar, sequential manner,
with the added ability to explicitly express the conditions under which code fragments
sequentially commute. Putting such commutativity conditions into source code offers a
new entry point for a compiler to exploit the known connection between commutativity
and parallelism. We give a semantics for the programmer's sequential perspective and,
under a correctness condition, find that a compiler-transformed parallel execution
is equivalent to the sequential semantics. Serializability/linearizability are not
the right fit for this condition, so we introduce scoped serializability and show
how it can be enforced with lock synthesis techniques.
We next describe a technique for automatically verifying and synthesizing commute conditions
via a new reduction from our commute blocks to logical specifications, upon which symbolic
commutativity reasoning can be performed. We implemented our work in a new language called
Veracity, implemented in Multicore OCaml. We show that commutativity conditions can be automatically generated across a variety of new benchmark programs, confirm the expectation that concurrency speedups can be seen as the computation increases, and apply our work to a small in-memory filesystem and an adaptation of a crowdfund blockchain smart contract.
The below works are the most relevant to Veracity, listed in order of importance.
Below are the instructions to fetch a docker.
$ docker pull erickoskinen/veracity:mc-bin-v1 $ docker run -it erickoskinen/veracity:mc-bin-v1 bash $ cat README.md