SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 13:40 - 14:00 at OOPSLA/ECOOP - W-4
Thu 19 Nov 2020 01:40 - 02:00 at OOPSLA/ECOOP - W-4

Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously difficult to prove linearizable, which requires identifying a point in time in which the traversal’s result is correct. The problem is that traversing the data structure as it undergoes modifications leads to complex behaviors, requiring intricate reasoning about all interleavings of reads by traversals and writes mutating the data structure.

In this paper, we present a general proof technique for proving unsynchronized traversals correct in a significantly simpler manner, compared to typical concurrent reasoning and prior proof techniques. Our framework relies only on \emph{sequential properties} of traversals and on a conceptually simple and widely-applicable condition about the ways an algorithm’s writes mutate the data structure. Establishing that a target data structure satisfies our condition requires only simple concurrent reasoning, without considering interactions of writes and reads. This reasoning can be further simplified by using our framework.

To demonstrate our technique, we apply it to prove several interesting and challenging concurrent binary search trees: the logical-ordering AVL tree, the Citrus tree, and the full contention-friendly tree. Both the logical-ordering tree and the full contention-friendly tree are beyond the reach of previous approaches targeted at simplifying linearizability proofs.

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

13:00 - 14:20: W-4OOPSLA at OOPSLA/ECOOP +12h
13:00 - 13:20
Talk
OOPSLA
Noam YefetTechnion, Uri AlonTechnion, Eran YahavTechnion
Pre-print
13:20 - 13:40
Talk
OOPSLA
Manuel RiggerETH Zurich, Switzerland, Zhendong SuETH Zurich, Switzerland
Pre-print
13:40 - 14:00
Talk
OOPSLA
Yotam FeldmanTel Aviv University, Artem KhyzhaTel Aviv University, Constantin EneaIRIF, University Paris Diderot & CNRS, Adam MorrisonTel Aviv University, Aleksandar NanevskiIMDEA Software Institute, Noam RinetzkyTel Aviv University, Israel, Sharon ShohamTel Aviv university
14:00 - 14:20
Talk
OOPSLA
Vytautas AstrauskasETH Zurich, Switzerland, Christoph MathejaETH Zurich, Switzerland, Federico PoliETH Zurich, Switzerland, Peter MüllerETH Zurich, Alexander J. SummersThe University of British Columbia

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

01:00 - 02:20: W-4OOPSLA at OOPSLA/ECOOP
01:00 - 01:20
Talk
OOPSLA
Noam YefetTechnion, Uri AlonTechnion, Eran YahavTechnion
Pre-print
01:20 - 01:40
Talk
OOPSLA
Manuel RiggerETH Zurich, Switzerland, Zhendong SuETH Zurich, Switzerland
Pre-print
01:40 - 02:00
Talk
OOPSLA
Yotam FeldmanTel Aviv University, Artem KhyzhaTel Aviv University, Constantin EneaIRIF, University Paris Diderot & CNRS, Adam MorrisonTel Aviv University, Aleksandar NanevskiIMDEA Software Institute, Noam RinetzkyTel Aviv University, Israel, Sharon ShohamTel Aviv university
02:00 - 02:20
Talk
OOPSLA
Vytautas AstrauskasETH Zurich, Switzerland, Christoph MathejaETH Zurich, Switzerland, Federico PoliETH Zurich, Switzerland, Peter MüllerETH Zurich, Alexander J. SummersThe University of British Columbia