Verifying Concurrent Search Structure Templates

Add to your list(s) Download to your calendar using vCal

• Siddharth Krishna, NYU
• Monday 26 November 2018, 15:00-16:00
• SS03.

If you have a question about this talk, please contact Victor Gomes.

Concurrent separation logics have had great success reasoning about concurrent data structures. This success stems from their application of modularity on multiple levels, leading to proofs that are decomposed according to program structure, program state, and individual threads. Despite these advances, it remains difficult to achieve proof reuse across different data structure implementations. For the large class of search structures, we demonstrate how one can achieve further proof modularity by decoupling the proof of thread safety from the proof of structural integrity. We base our work on the template algorithms of Shasha and Goodman, that dictate how threads interact but abstract from the concrete layout of nodes in memory. Building on our recent flow framework [POPL ‘18] of compositional abstractions and the separation logic ReLoC/Iris, we show how to prove contextual refinement for template algorithms, and how to instantiate them to obtain multiple verified implementations. We demonstrate our approach by formalizing three concurrent search structure templates, based on link, give-up, and lock-coupling synchronization, and deriving implementations based on B-trees, hash tables, and linked lists. Our proofs are mechanized and partially automated using the Coq proof assistant and the deductive verification tool GRAS Shopper. Not only does our approach reduce the proof complexity, we are also able to achieve significant proof reuse.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.