Winter 2023 Seminars

Winter 2023

Organizer: Yao Li

All Talks

Date Title Speaker
Verified Causal Broadcast with Liquid Haskell Lindsey Kuper
Monadic Definitional Interpreters as Formal Semantic Models of Computations in Coq Yannick Zakowski
PaSh: Practically Correct, Just-in-Time Shell Script Parallelization Konstantinos Kallas
HyperQB: Bounded Model Checking for Hyperproperties with QBF-based Algorithms Tzu-Han Hsu
Paper reading group TBA
Paper reading group TBA

Verified Causal Broadcast with Liquid Haskell

Speaker: Lindsey Kuper

Lindsey Kuper is an Assistant Professor at the University of California, Santa Cruz. Her research takes a programming-languages-based approach to building provably correct and practically deployable distributed software systems. She is a co-founder of !!Con (bangbangcon.com), the conference of ten-minute talks on the joy, excitement, and surprise of computing. She is the recipient of the NSF CAREER Award (2022) and a Google Faculty Research Award (2019) and received her Ph.D. in computer science in 2015 from Indiana University.

Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, key-value stores can use causally ordered message delivery to ensure causal consistency, and replicated data structures rely on the existence of an underlying causally-ordered messaging layer. A causal delivery protocol ensures that when a message is delivered to a process, any causally preceding messages sent to the same process have already been delivered to it. While causal delivery protocols are widely used, verification of the correctness of those protocols is less common, much less machine-checked proofs about executable implementations. We implemented a standard causal broadcast protocol in Haskell and used the Liquid Haskell solver-aided verification system to express and mechanically prove that messages will never be delivered to a process in an order that violates causality. We express this property using refinement types and prove that it holds of our implementation, taking advantage of Liquid Haskell's underlying SMT solver to automate parts of the proof and using its manual theorem-proving features for the rest. We then put our verified causal broadcast implementation to work as the foundation of a distributed key-value store.

Monadic Definitional Interpreters as Formal Semantic Models of Computations in Coq

Speaker: Yannick Zakowski

Monadic interpreters have seen in recent years a rise in popularity as a means to model and reason about impure computations in dependently typed theories. The Interaction Tree project in particular implements a set of libraries in the Coq proof assistant providing tools to enable this approach at scale. This talk intents to paint an overview of the project. I will first introduce the core concepts: modelling divergence through coinduction, achieving modularity through layered interpreters in the style of algebraic effects, enabling testing by extraction, and offering equational and Hoare-style relational reasoning up-to a notion of weak bisimilarity. Projects to which the approach have been applied, notably in the modelling of LLVM IR as part of the Vellvm project, will be mentioned on the way. Through the second half of the presentation, I will focus more specifically on so-called Choice Trees, a recent proposal to provide in this ecosystem a proper support for non-deterministic computations.

Monadic interpreters have seen in recent years a rise in popularity as a means to model and reason about impure computations in dependently typed theories. The Interaction Tree project in particular implements a set of libraries in the Coq proof assistant providing tools to enable this approach at scale. This talk intends to paint an overview of the project. I will first introduce the core concepts: modelling divergence through coinduction, achieving modularity through layered interpreters in the style of algebraic effects, enabling testing by extraction, and offering equational and Hoare-style relational reasoning up-to a notion of weak bisimilarity. Projects to which the approach have been applied, notably in the modelling of LLVM IR as part of the Vellvm project, will be mentioned on the way. Through the second half of the presentation, I will focus more specifically on so-called Choice Trees, a recent proposal to provide in this ecosystem a proper support for non-deterministic computations.

PaSh: Practically Correct, Just-in-Time Shell Script Parallelization

Speaker: Konstantinos Kallas

Konstantinos Kallas is a 5th year PhD student at the University of Pennsylvania working with Rajeev Alur. His area of interest is the intersection of programming languages and computer systems. Recently, together with several amazing people Konstantinos has been working on invigorating the research on the shell. The first paper in this line of work, introducing PaSh, a system for parallelizing shell scripts, received the best paper award at EuroSys 2021. He has also published papers improving the shell at ICFP 2021, HotOS 2021, and OSDI 2022. Konstantinos is also interested in programming models and runtimes for stateful serverless computing. He has worked on Azure Durable Functions and has published papers on this topic in OOPSLA 2021, VLDB 2022, and POPL 2023. You can find more information about him here: https://angelhof.github.io/.

Recent shell-script parallelization systems enjoy mostly automated parallel speedups by compiling scripts ahead-of-time. Unfortunately, such static parallelization is hampered by the dynamic behaviors pervasive in shell scripts—e.g., variable expansion and command substitution—which often requires reasoning about the current state of the shell and filesystem. We present a just-in-time (JIT) shell-script compiler, PaSh-JIT, that intermixes evaluation and parallelization during a script's run-time execution. JIT parallelization collects run-time information about the system’s state, but must not alter the behavior of the original script and must maintain minimal overhead. PaSh-JIT addresses these challenges by (1) using a dynamic interposition framework, guided by a static preprocessing pass, (2) developing runtime support for transparently pausing and resuming shell execution; and (3) operating as a stateful server, communicating with the current shell by passing messages—all without requiring modifications to the system's underlying shell interpreter. When run on a wide variety of benchmarks, including the POSIX shell test suite, PaSh-JIT (1) does not break scripts, even in cases that are likely to break shells in widespread use; and (2) offers significant speedups, whenever parallelization is possible. These results show that PaSh-JIT can be used as a drop-in replacement for any non-interactive shell use, providing significant speedups without any risk of breakage.

HyperQB: Bounded Model Checking for Hyperproperties with QBF-based Algorithms

Speaker: Tzu-Han Hsu

Tzu-Han Hsu is a third-year Ph.D. student in Computer Science and Engineering department at Michigan State University, advised by Dr. Borzoo Bonakdarpour. Her research areas include formal methods, model checking, verification, and synthesis for security/privacy policies. She is recently working on the topic of hyperproperties, a framework that can reason about multiple traces simultaneously, which has rich applications in formal analysis especially for multi-threaded and concurrent programs. Before MSU, Tzu-Han received her bachelor's degrees in Computer Science and Music-Piano Performance from Iowa State University in 2020. Tzu-Han can be reached on Twitter (@TzuHanH), LinkedIn (tzuhanhsu), email (tzuhan@msu.edu), and her personal website (https://tzuhancs.github.io/).

Hyperproperties is a powerful framework for specifying and reasoning about important classes of requirements that were not possible with trace-based languages such as the classic temporal logics. This talk will introduce a novel bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. Followed by the reduction of BMC for LTL to SAT solving, our BMC approach naturally reduces to QBF solving, as HyperLTL allows explicit and simultaneous quantification over multiple traces. Our algorithm is sound based on our theory of bounded semantics, which guarantees correct BMC results under finite exploration. A recent extension of our algorithm also supports loop conditions, which incorporate SAT solving; and the asynchronous hyper logic A-HLTL, which utilizes the notion of trajectories to handle traces that advance at different speeds. In this talk, we will also present our implemented tool HyperQB, a push-button QBF-based bounded model checker for hyperproperties, and demonstrate the effectiveness and efficiency of our approach via a rich set of practical applications, including concurrent data structures, path planning for multi-agent systems, secrecy-preserving mapping synthesis, compiler optimization security, cache-based timing attack detection, and program conformance.

Paper reading group

Paper reading group