From adcbb2b5e5a7a5a5fa115b63f9a2cbce4d74608d Mon Sep 17 00:00:00 2001 From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk> Date: Fri, 24 Nov 2017 12:14:11 +0000 Subject: [PATCH] Add new file --- _posts/2017-11-24-siddharth.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 _posts/2017-11-24-siddharth.md diff --git a/_posts/2017-11-24-siddharth.md b/_posts/2017-11-24-siddharth.md new file mode 100644 index 0000000..e966264 --- /dev/null +++ b/_posts/2017-11-24-siddharth.md @@ -0,0 +1,23 @@ +--- +title: Visitor to the group, Siddharth Krishna, New York University, USA +--- +We are very pleased to have welcome [Siddharth Krishna](https://cs.nyu.edu/~siddharth/), from the Courant Institute of Mathematical Sciences, NYU, +who visited the group this week to talk about his work on the verification of concurrent data structures. + +Siddharth is a PhD student in the Computer Science Department of New York University, working on Formal Verification and Machine Learning under the supervision +of [Thomas Wies](https://cs.nyu.edu/wies/). Siddharth gave a talk based on his forthcoming paper on Flow Interfaces: Go with the Flow: Compositional Abstractions +for Concurrent Data Structures, joint work with Dennis Shasha and Thomas Wies, to appear at [POPL 2018](https://cs.nyu.edu/~siddharth/pubs/2018-popl-flows.pdf). + +The abstract of the talk is: Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. +However, a recurring problem in such proofs is that data structure abstractions that work well in the sequential setting, such as inductive predicates, +are much harder to reason about in a concurrent setting due to complex sharing and overlays. To solve this problem, we propose a novel approach to abstracting +regions in the heap by encoding the data structure invariant into a local condition on each individual node. This condition may depend on a quantity associated +with the node that is computed as a fixpoint over the entire heap graph. We refer to this quantity as a flow. Flows can encode both structural properties +of the heap (e.g. the reachable nodes from the root form a tree) as well as data invariants (e.g. sortedness). We then introduce the notion of a flow interface, +which expresses the relies and guarantees that a heap region imposes on its context to maintain the local flow invariant with respect to the global heap. +Our main technical result is that this notion leads to a new semantic model of separation logic. In this model, flow interfaces provide a general abstraction +mechanism for describing complex data structures. This abstraction mechanism admits proof rules that generalize over a wide variety of data structures. +To demonstrate the versatility of our approach, we show how to extend the logic RGSep with flow interfaces. We have used this new logic to prove linearizability +and memory safety of nontrivial concurrent data structures. In particular, we obtain parametric linearizability proofs for concurrent dictionary algorithms +that abstract from the details of the underlying data structure representation. These proofs cannot be easily expressed using the abstraction mechanisms +provided by existing separation logics. \ No newline at end of file -- GitLab