Go with the Flow - Compositional Abstractions for Concurrent Data Structures

Watch a technical presentation from POPL 2018 conference exploring novel approaches to concurrent data structure verification through flow interfaces. Learn how researchers from New York University developed a new semantic model of separation logic that simplifies correctness proofs for concurrent data structures. Discover how flow interfaces provide an abstraction mechanism for describing complex data structures by encoding invariants into local conditions on individual nodes. Follow along as the speakers demonstrate the practical applications of their approach by proving linearizability and memory safety of concurrent dictionary algorithms, showing how their method can create parametric proofs that abstract away from specific data structure implementations. Gain insights into how this advancement addresses the challenges of reasoning about data structure abstractions in concurrent settings, where traditional sequential approaches fall short due to complex sharing and overlays.