|
Computer Science Seminar Date: Tuesday, 19 August 2025 Time: 3:30 PM Venue: Seminar Hall Machine-Verifying Fast Concurrent Algorithms Siddhartha Jayanti Dartmouth College, USA. 19-08-25 Abstract As computing permeates our lives, the reliability of algorithms has become indispensable. Particularly challenging is the task of ensuring the reliability of concurrent data structures, which underlie the design of fast parallel algorithms for the modern multicores in our phones, laptops, and data center servers. In this talk, I will describe some uses of concurrent data structures, motivate the need for their machine-verification, and describe an elegant technique for machine-verification of concurrent data structures, known as *meta-configuration tracking* [Jayanti, Jayanti, Yavuz, Hernandez: ACM POPL 2024]. This technique is simple to use, requiring only forward reasoning, yet it is universal and complete, i.e., powerful enough to prove the correctness of even intricate data structures with future and far-future dependent linearization structures. We have used meta-configuration tracking to machine-verify impactful data structures, including: the Jayanti-Tarjan concurrent union-find data structure which enables "parallel clustering algorithms which scale to graphs with tens of billions of edges" at Google [received Google Healthys Platinum Award], the ParlayHash data structure which is "the fastest concurrent hash table at Google" [received Google Healthys Gold Award], and MemSnap which is a fast far-future dependent snapshot object [received ACM SPAA 2025 Distinguished Paper Award]. About the speaker: Siddhartha Jayanti is an Assistant Professor of computer science at Dartmouth College, where he leads the Distributed Computing and Verification Lab. His research spans algorithms, verification, and applications with a focus on designing simple, fast, scalable, and reliable solutions to challenging multidisciplinary problems. Siddhartha's work has touched several areas of inquiry, including distributed computing, algorithms and data structures, verification, relativistic physics, economics, security, and machine learning. Prior to Dartmouth, Siddhartha worked as a research scientist at Google Research , where he designed and deployed fast and formally verified algorithms for large-scale data processing and clustering. Siddhartha received his bachelor's from Princeton University, and his Masters and Ph.D. from MIT. His dissertation entitled *Simple, Fast, Scalable, and Reliable Multiprocessor Algorithms*, received the *2023 ACM-EATCS Principles of Distributed Computing Doctoral Dissertation Award*. Siddhartha also wrote the first modern computer science research paper in Telugu; the work is included as a chapter of his dissertation with an abstract in Sanskrit.
|
