Commutativity of data structure methods is of ongoing interest, with roots in the database community. In recent years commutativity has been shown to be a key ingredient to enabling multicore concurrency in contexts such as parallelizing compilers, transactional memory, speculative execution and, more broadly, software scalability. Despite this interest, it remains an open question as to how a data structure's commutativity specification can be verified automatically from its implementation.
I will describe our recent work on techniques to automatically prove the correctness of method commutativity conditions from data structure implementations. We introduce a new kind of abstraction that characterizes the ways in which the effects of two methods differ depending on the order in which the methods are applied, and abstracts away effects of methods that would be the same regardless of the order. I’ll then discuss a novel algorithm that reduces the problem to reachability, so that off-the-shelf program analysis tools can perform the reasoning necessary for proving commutativity. Finally, I’ll describe CityProver: a proof-of-concept commutativity verifier and some experimental results on ADTs such as a memory cell, counter, two-place Set, array-based stack, queue, and a rudimentary hash table. I’ll conclude with a discussion of what makes a data structure's commutativity provable with today's tools and what needs to be done to prove more in the future.
Joint work with Kshitij Bansal
Eric Koskinen is an Assistant Professor at Stevens Institute of Technology. Previously, he was a Lecturer/Researcher at Yale University and a Visiting Professor at New York University. Eric received a Ph.D in Computer Science from the University of Cambridge, where he was a Gates Cambridge Scholar. He also spent time at IBM Watson, Microsoft, and from 2002-2005, Eric was a Software Engineer at Amazon.com. Eric’s research is at the intersection of automatic software verification and concurrency and yields techniques that improve the way programmers develop reliable and efficient concurrent software for multi-core and distributed systems.