Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections

Explore a 25-minute conference presentation from POPL 2018 that introduces a breakthrough in monitoring concurrent data structures. Learn how researchers Michael Emmi and Constantin Enea developed the first sound, complete, and tractable algorithm for monitoring linearizability in collection abstract data types. Discover how their work overcomes the traditional exponential-time complexity requirements by leveraging unique combinatorial properties of collections like stacks, queues, sets, and maps. Understand how this innovative approach reduces linearizability monitoring to Horn satisfiability, making it possible to efficiently verify the correctness of concurrent data structure implementations in polynomial time - a significant advancement over previous methods that were limited to single-value registers.