Shadaj Laddad*, Conor Power*, Mae Milano, Alvin Cheung, Natacha Crooks, Joseph M. Hellerstein
Conflict-free replicated datatypes (CRDTs) are a promising line of work that enable coordination-free replication and offer certain eventual consistency guarantees in a relatively simple object-oriented API. Yet CRDT guarantees extend only to data updates; observations of CRDT state are unconstrained and unsafe. We propose an agenda that embraces the simplicity of CRDTs, but provides richer, more uniform guarantees. We extend CRDTs with a query model that reasons about which queries are safe without coordination by applying monotonicity results from the CALM Theorem, and lay out a larger agenda for developing CRDT data stores that let developers safely and efficiently interact with replicated application state.
Katara: Synthesizing CRDTs with Verified Lifting
Shadaj Laddad, Conor Power, Mae Milano, Alvin Cheung, Joseph M. Hellerstein
In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Katara is able to automatically synthesize CRDTs for a wide variety of scenarios, from reproducing classic CRDTs to synthesizing novel designs based on specifications in existing literature. Crucially, our synthesized CRDTs are fully, automatically verified, eliminating entire classes of common errors and reducing the process of producing a new CRDT from a painstaking paper proof of correctness to a lightweight specification.
VizSmith: Automated Visualization Synthesis by Mining Data-Science Notebooks
Rohan Bavishi, Shadaj Laddad, Hiroaki Yoshida, Mukul R. Prasad, Koushik Sen
We built a tool called VizSmith which enables code reuse for visualizations by mining visualization code from Kaggle notebooks and creating a database of 7176 reusable Python functions. Given a dataset, columns to visualize and a text query from the user, VizSmith searches this database for appropriate functions, runs them and displays the generated visualizations to the user.
Fluid Quotes: Metaprogramming across Abstraction Boundaries with Dependent Types
Shadaj Laddad and Koushik Sen
We introduce Fluid Quotes, a new technique that uses dependent types to let users pass quotes through abstraction boundaries in runtime code while splicing them ahead-of-time. This technique enables new metaprogramming capabilities by eliminating the traditional requirement of co-locating parameter expressions with call-sites. Fluid Quotes capture not only source code but also associated runtime context to ensure correctness.
ScalaPy: Seamless Python Interoperability for Cross-Platform Scala Programs
Shadaj Laddad and Koushik Sen
In this paper, we introduce ScalaPy, a system for interoperability between Scala and Python. With ScalaPy, developers can use Python libraries in Scala by treating Python values as Scala objects and exposing Scala values to Python. ScalaPy supports both Scala on the JVM and Scala Native, enabling its usage from data experiments in interactive notebook environments to performance-critical production systems.