BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verifying Concurrent Search Structure Templates - Siddharth Krishn
 a\, NYU
DTSTART:20181126T150000Z
DTEND:20181126T160000Z
UID:TALK115303@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Concurrent separation logics have had great success reasoning 
 about\nconcurrent data structures. This success stems from their applicati
 on of\nmodularity on multiple levels\, leading to proofs that are decompos
 ed\naccording to program structure\, program state\, and individual thread
 s.\nDespite these advances\, it remains difficult to achieve proof reuse\n
 across different data structure implementations. For the large class of se
 arch structures\, we demonstrate how one can achieve further proof modular
 ity by decoupling the proof of thread safety from the proof of structural 
 integrity. We base our work on the template algorithms of Shasha and Goodm
 an\, that dictate how threads interact but abstract from the concrete\nlay
 out of nodes in memory. Building on our recent flow framework [POPL\n'18] 
 of compositional abstractions and the separation logic ReLoC/Iris\, we sho
 w how to prove contextual refinement for template algorithms\, and how to\
 ninstantiate them to obtain multiple verified implementations. We\ndemonst
 rate our approach by formalizing three concurrent search structure\ntempla
 tes\, based on link\, give-up\, and lock-coupling synchronization\, and\nd
 eriving implementations based on B-trees\, hash tables\, and linked lists.
 \nOur proofs are mechanized and partially automated using the Coq proof\na
 ssistant and the deductive verification tool GRASShopper. Not only does\no
 ur approach reduce the proof complexity\, we are also able to achieve\nsig
 nificant proof reuse.
LOCATION:SS03
END:VEVENT
END:VCALENDAR