{"id":389,"date":"2025-04-30T07:53:31","date_gmt":"2025-04-30T12:53:31","guid":{"rendered":"https:\/\/www.podc.org\/podc2025\/?page_id=389"},"modified":"2025-07-03T10:54:59","modified_gmt":"2025-07-03T15:54:59","slug":"workshops-and-tutorials","status":"publish","type":"page","link":"https:\/\/www.podc.org\/podc2025\/workshops-and-tutorials\/","title":{"rendered":"Workshops and Tutorials"},"content":{"rendered":"\n

The schedule is tentative and will be updated later.<\/p>\n\n\n\n

Monday, June 16<\/h2>\n\n\n\n

Workshop: Advanced Tools, Programming Languages, and PLatforms for Implementing and Evaluating algorithms for Distributed systems (ApPLIED)<\/strong><\/h2>\n\n\n\n

Time:<\/strong> 08:55 – 18:00
TPC Co-chairs:<\/strong> Wojciech Golab and Andrea Vitaletti
General Co-chairs:<\/strong> Amy Babay, Ioannis Chatzigiannakis, and Elad Michael Schiller
Website:<\/strong> https:\/\/www.cse.chalmers.se\/~elad\/ApPLIED2025\/<\/a>
Proceedings:<\/strong> https:\/\/www.cse.chalmers.se\/~elad\/ApPLIED2025\/toc.html<\/a><\/p>\n\n\n\n

Tutorial: Machine-Verifying Concurrent Algorithms<\/strong><\/h2>\n\n\n\n

Organizer:<\/strong> Siddhartha Jayanti (siddhartha.visveswara.jayanti@dartmouth.edu<\/a>)
Time:<\/strong> 10:00 –<\/p>\n\n\n\n

Abstract: <\/strong>Concurrent algorithms are intricate and their execution patterns on modern multiprocessors are extremely complex due to scheduling asynchrony, thus machine-certified proofs of their correctness are invaluable in ensuring reliability. This need for formal verification is bolstered by several examples of tragic outcomes due to failure to formally machine-verify concurrent algorithms. In fact, history has shown that the consequences of incorrect concurrent code can be catastrophic: a subtle priority inversion bug in its concurrent code crashed the Pathfinder Rover days after its deployment on Mars and jeopardized the entire multi-million dollar NASA space mission [Jones, 2013<\/a>]; a race condition in the Northeast power grid\u2019s energy management system started a cascading electrical outage that affected an estimated 55 million people in eight U.S. states and Ontario, Canada [Poulsen, 2004<\/a>]; race conditions in the Therac-25 radiation therapy machine caused it to administer radiation doses that were over a hundred times as potent as the intended dose, which caused the deaths of at least three people and several more injuries [Leveson and Turner, 1993<\/a>; Lim, 1998<\/a>]. Examples of errors in published concurrent data structures are also not left wanting [Colvin and Groves, 2005<\/a>; Doherty, 2003<\/a>]. These fatal bugs all point to the importance of machine-verification of intricate concurrent algorithms, like the concurrent data structures we design in the distributed computing community.<\/p>\n\n\n\n

Last year, we introduced meta-configurations tracking\u2014<\/em>a forward reasoning<\/em> proof method that aids in producing machine-certified proofs of linearizability [Jayanti et al., POPL 2024]. Meta-configurations tracking is sound,<\/em> complete,<\/em> and universal<\/em>, meaning that it can be used to produce a proof of linearizability for any correct data structure<\/em> implementation of any type<\/em>\u2014including so-called future linearizable and far-future linearizable implementations which have traditionally been considered very hard to prove by the formal methods community. For example, we have used meta-configurations tracking to produce machine-certified proofs of Herlihy and Wing\u2019s queue [Herlihy and Wing, 1990], MemSnap [Jayanti, Jayanti, and Jayanti, 2024], and Jayanti and Tarjan\u2019s set union object [Jayanti and Tarjan, 2016]. The last of these is deployed in Google\u2019s open-source graph-mining library and enables \u201cshared memory parallel clustering algorithms which scale to graphs with tens of billions of edges\u201d. Our work received a Google Code Health Platinum Award for Formal Verification of Multiprocessor Algorithms that Underlie Large-Scale Clustering<\/em>.<\/p>\n\n\n\n

In this tutorial, I will explain the meta-configurations tracking <\/em>method for producing formal proofs of the linearizability of concurrent objects. I will also explain how to deploy the method to produce machine-certified proofs using TLA+ (temporal language of actions) and TLAPS (TLA+ proof system). Two goals of this tutorial are: (1) to introduce more members of the distributed computing community to formal methods and machine-verification; and (2) enable concurrent algorithmists to machine-verify their own data structures. The tutorial is designed to be accessible to a wide-audience in the distributed computing community.<\/p>\n\n\n\n

Friday, June 20<\/h2>\n\n\n\n

Tutorial: Information Theory and Applications<\/strong><\/h2>\n\n\n\n

Organizer:<\/strong> Rotem Oshman
Time:<\/strong> 09:00 – 15:00<\/p>\n\n\n\n

Abstract:<\/strong> The tutorial will cover the basics of information theory, including Shannon entropy and KL divergence, and their relationship to lossless coding. Using these tools we will tackle several communication complexity lower bounds and applications in distributed computing, such as the linear lower bound on the randomized communication complexity of set disjointness, and the lower bound of Izumi and Le Gall on listing triangles in CONGEST.<\/p>\n\n\n\n

Tentative Schedule<\/strong><\/p>\n\n\n\n