Program for the winter quarter of 2021.
1/14: Resource-Aware Session Types for Digital Contracts
Time: Thursday, January 14, 2021, 12 noon - 1pm
Location: Zoom
Speaker: Ankush Das
Abstract: While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges, this talk presents an analysis for statically deriving worst-case bounds on the computational complexity of message-passing processes, respectively. The analysis is based on novel resource-aware session types that describe resource contracts by allowing both messages and processes to carry potential and amortize cost. The talk then applies session types to implement digital contracts. Digital contracts are protocols that describe and enforce execution of a contract, often among mutually distrusting parties. Programming digital contracts comes with its unique challenges, which include describing and enforcing protocols of interaction, analyzing resource usage and tracking linear assets. The talk presents the type-theoretic foundations of Nomos, a programming language for digital contracts whose type system addresses the aforementioned domain-specific requirements. To express and enforce protocols, Nomos is based on shared binary session types rooted in linear logic. To control resource usage, Nomos uses resource-aware session types and automatic amortized resource analysis, a type-based technique for inferring resource bounds. To track assets, Nomos employs a linear type system that prevents assets from being duplicated or discarded. The talk concludes with future work directions on designing an efficient implementation for Nomos and making it robust to attacks from malicious entities.
Food: Doordash,
2/4: AutoMap
Time: Thursday, February 4, 2021, 12 noon - 1pm
Location: Zoom
Speaker: Rohan Yadav
Abstract: Mapping is the process of selecting a processor for each computation, or task, and memories for the data collections that those tasks access. On parallel, heterogeneous, and distributed computing platforms, finding a mapping that yields high performance for a given application is challenging. We show that fast mappings are sensitive to the machine, application, and even input used. Porting to a new machine, modifying the application, or running on a substantially different input may all necessitate re-tuning the application mapping to maintain the best possible performance.
We present AutoMap, a system which, given an application and an input, automatically tunes the mapping to the hardware used. AutoMap searches over the space of possible mappings dynamically, using a search algorithm and judicious pruning methods. We demonstrate that AutoMap finds fast mappings in minutes to a few hours, whereas handwritten mappings often require days of experimentation.
We also describe em constrained coordinate-wise descent (CCD), a search algorithm that explicitly balances the trade-off between running computations as quickly as possible and minimizing data movement. CCD discovers mappings that are as fast as, or up to 20% faster than, hand-tuned mappings, even on the hardware for which the hand-tuned mapping was designed. We find greater speedups (up to 40%) when re-tuning an existing mapping for different hardware or inputs.
Food: Doordash,
2/11: Programming Systems for Bug-Free and Robust Probabilistic Software
Time: Thursday, February 11, 2021, 12 noon - 1pm
Location: Zoom
Speaker: Sasa Misailovic
Abstract: Probabilistic programming languages offer an intuitive way to model uncertainty by representing complex probability models as simple probabilistic programs. Thus, even a programmer with limited exposure to statistical machine learning can benefit from powerful probabilistic inference. A programmer only needs to write a high-level model in a programming language with support for random sampling and conditioning on data. The underlying probabilistic programming systems (which execute the high-level probabilistic programs) hide the complexity of inference algorithms from the program developer. Understanding how to test and debug probabilistic software will have a key role in improving programmer productivity in this emerging domain.
In this talk, I will present our work on testing and analyzing probabilistic programming systems and discuss some common classes of real-world problems that impact the accuracy and correctness in probabilistic programming. Our systems helped discover over 50 bugs in the popular probabilistic programming systems Pyro, Edward, and Stan, as well as their underlying infrastructures PyTorch and TensorFlow.
2/18: Pono Model Checker
Time: Thursday, February 18, 2021, 12 noon - 1pm
Location: Zoom
Speaker: Makai Mann
Abstract: Symbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present Pono, an open-source SMT-based model checker. Pono is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance, Pono prioritizes transparency (developed as an open-source project on GitHub), flexibility (Pono can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers).
Food:
2/25: Reifying Concurrent Programs
Time: Thursday, February 25, 2021, 12 noon - 1pm
Location: Zoom
Speaker: Shaz Qadeer
Abstract: Program reification is a new approach to the construction of verified concurrent programs and their proofs. This approach simplifies and scales (human and automated) reasoning by enabling a concurrent program to be represented and manipulated at multiple layers of abstraction. These abstraction layers are chained together via simple program transformations; each transformation is justified by a collection of automatically checked verification conditions. Program reification makes proofs maintainable and reusable, specifically eliminating the need to write complex invariants on the low-level encoding of the concurrent program as a flat transition system.
I will present Civl, a reifier for concurrent programs. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, consensus protocol, and shared-memory data structures. Civl is publicly available: https://civl-verifier.github.io/.
This work has been done jointly with Bernhard Kragl (IST Austria).
Food: