Colloquium Details

Contemporary online applications are data-intensive, often running on top of large-scale inter-connected geo-distributed databases. The high complexity of these systems coupled with ever-increasing expectations of performance and availability has made it hard for programmers to ensure integrity and safety of data-intensive applications.

In this talk, I demonstrate how techniques rooted in programming languages and automated formal methods can help developers ensure the integrity of data-intensive applications without compromising their runtime performance.  First among such techniques is a method to automatically reason about the safety of non-serializable transactions, which often replace expensive serializable transactions in practice. I show that the semantics of these transactions, albeit non-standard, can be precisely related to the high-level semantics of a database application, making it possible to reason about application safety in the absence of ACID guarantees. Next, I extend this methodology to “weakly-consistent” geo-distributed databases that underlie modern large-scale web services. I present a bounded symbolic execution technique that is effective at identifying and repairing safety violations in realistic distributed database applications. Finally, I present a synthesis technique that can automatically transform ordinary sequential data structures into a class of distributed data structures called Mergeable Replicated Data Types (MRDTs) that can be composed to build linearly-scalable distributed applications. Together, the aforementioned techniques constitute a principled approach towards developing data-intensive applications with strong safety guarantees. I will end the talk with a discussion on the possibility of applying techniques such as these to enforce strong guarantees on an emerging class of distributed applications such as those that enable planet-scale decentralization.