Roll Forward, Not Back: A Case for Deterministic Conflict Resolution

Sebastian Burckhardt, Daan Leijen, and Manuel Fahndrich

Abstract

Enabling applications to execute various tasks in parallel is difficult if those tasks exhibit read and write conflicts. In recent work, we developed a programming model based on concurrent revisions that addresses this challenge: each forked task gets a conceptual copy of all locations that are declared to be shared. Each such location has a specific isolation type; on joins, state changes to each location are merged deterministically based on its isolation type. In this paper, we study how to specify isolation types abstractly using operation-based compensation functions rather than state based merge functions. Using several examples including a list with insert, delete and modify operations, we propose compensation tables as a concise, general and intuitively accessible mechanism for determining how to merge arbitrary operation sequences. Finally, we provide sufficient conditions to verify that a state-based merge function correctly implements a compensation table.

Details

Publication typeInproceedings
Published inThe 2nd Workshop on Determinism and Correctness in Parallel Programming (WODET'11)
AddressNewbeach, California
> Publications > Roll Forward, Not Back: A Case for Deterministic Conflict Resolution