ABSTRACT. Algorithms that guarantee system-wide progress and throughput have seen significant research interest over the last few decades. System-wide progress becomes even more critical in the context of distributed storage systems, where process failures and network partitions can introduce arbitrary delays. In this talk, we consider the problem of designing wait-free distributed data structures. Recent research shows that certain data structures can indeed be designed to guarantee wait-freedom and consistency in the presence of node failures. We can even characterize conditions under which a wait-free, strongly consistent implementation of a data structure is not possible. On the other hand, we now beginning to understand why distributed algorithms which do not guarantee wait-freedom (such as Paxos), appear to be wait-free in practice. This leads to the following open question – does system-wide progress really matter?

ABSTRACT. With the proliferation of multicore systems, the design of concurrent algorithms and concurrent data structures to support them has becomes critical. Wait-free data structures provide a very basic and natural progress guarantee, assuring that each thread always makes progress when given enough CPU cycles. However, wait-free algorithms were considered difficult to design and too costly to be used in practice. Only the weaker lock-free guarantee, which allows almost all threads to starve, was achievable in practice. In a series of recent papers, we have shown that this pessimistic belief was false and wait-freedom is actually achievable efficiently in practice.

ABSTRACT. We consider the problem of provably verifying that an asynchronous message-passing system satisfies its local assertions. We present a novel reduction scheme for asynchronous event-driven programs that finds almost-synchronous invariants--- invariants consisting of global states where message buffers are close to empty. The reduction finds almost-synchronous invariants and simultaneously argues that they cover all local states. We show that asynchronous programs often have almost-synchronous invariants and that we can exploit this to build natural proofs that they are correct. We implement our reduction strategy, which is sound and complete, and show that it is more effective in proving programs correct as well as more efficient in finding bugs in several programs, compared to current search strategies which almost always diverge. The high point of our experiments is that our technique can prove the Windows Phone USB Driver written in P correct for the receptiveness property, which was hitherto not provable using state-of-the-art model-checkers.