Talk "Semantics of concurrent data structured"

by Ana Sokolova

Fri, 06 July 2018 at 09:30 am in Royal Holloway, United Kingdom

Joint work with: Andreas Haas, Tom Henzinger, Andreas Holzer, Christoph Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Helmut Veith, Harald Woracek

Abstract: I will speak about a line of research done by myself and a group of collaborators on semantics of concurrent objects, in particular concurrent data structures. The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. It has been noticed that strong semantics might result in poor performance and scalability which initiated the work on relaxed semantics of concurrent objects, in particular concurrent data structures. Relaxing the semantics can be done in both dimensions: (1) by relaxing the sequential specification and/or (2) by relaxing the consistency condition. I will present quantitative relaxations that result in (1) as well as local linearizability that provides (2). This is joint work with many coauthors published at POPL'13 and CONCUR'16. Whether relaxed or strict, the semantics of concurrent objects always relies on linearizability. Therefore, in current work we study the foundations for verifying linearizability via order extension theorems. I will also briefly present these new results in my talk.