Trustworthy Systems


Suresh Jagannathan, Purdue University—West Lafayette

DaLi: The Data Store as a Library


Modern day Web applications increasingly rely on distributed, fault-tolerant data stores and databases to provide important management services related to persistence, multi-threading, communication, etc.  that ensure an always-on experience. Unfortunately, the software stack that props up these critical services is a messy and chaotic one, with significant complexity arising from a severe impedance mismatch between application and store-level object semantics and representations.  As a result, distributed data management solutions in these environemnt routinely violate application-level consistency and integrity constraints, comprising correctness guarantees.

To address these concerns, we have embarked on an ambitious project to reimagine how database and the storage systems they manage should interact with the high-level applications they support.  Our system (called DaLi) encapsulates data management functionality within transparent libraries written in the same language as the applications they support (OCaml, in our case).  A unified language representation enables properties and invariants relevant to the application, to be directly interpreted, enforced, and verified by underlying data management services.  Conversely, database functionality related to consistency, integrity, scalability, etc. are now couched in terms of application-aware abstractions and types. 

In this talk, we present several key aspects of this design that help to realize this vision.  These features specifically relate to our treatment of (a) weak consistency specification and enforcement, (b) verification of application invariants with respect to these consistency properties, and (c) data management and type support that bridge application and storage level object representations to help facilitate correctness arguments.


Suresh Jagannathan is a Professor of Computer Science at Purdue University.  His research interests span functional programming languages and their implementation, program verification and synthesis, type systems, and memory and consistency models.  Prior to joining Purdue, he was a Senior Research Scientist at NEC Research, Princeton.  From 2013-2016, he was a Program Manager at DARPA where he conceived and managed several major programs in probabilistic programming and machine learning, automated program synthesis and repair, and adaptive and intensional computing.  He received his Ph.D from MIT.