CSE Colloquium: Ji-Yong Shin

Speaker: Ji-Yong Shin, Associate Research Scientist, Yale University

Date: Monday, March 9

Time: 1:30-2:30pm

Location: HBL 1947

Title: Modular foundations for simple, verifiable distributed systems

Abstract:

Distributed systems are difficult to build and even more challenging to verify because of their inherent concurrency and weak failure assumptions. Although prior work has explored various methods to verify many existing systems, distributed system verification is still considered difficult and does not scale well. This is partly because most distributed systems are not designed with formal verification in mind, and because there are not enough generic models and proofs that can be reused for distributed system design and verification. 

In this talk, I will present two novel foundations that significantly simplify the design and verification of distributed systems. First, I will talk about a write-once-register abstraction that demonstrates the power of system and verification co-design. The write-once-register encapsulates distributed consistency, availability, and durability properties. The register abstraction handles the distributed nature of the system and helps programmers to easily build new systems on top. Similarly, when the distributed properties of the register are verified with a layered verification approach, systems that use the register can be incrementally verified as if they were non-distributed. Second, I will present an atomic distributed object, which is a simple high-level model for strongly consistent distributed systems. The atomic distributed object facilitates the verification of individual distributed systems and multiple distributed system interactions. High-level proofs of the object’s safety properties can be reused as a template to verify different low-level system implementations. The verified object model opens up new opportunities to reason and verify distributed system compositions at a simple object-level by hiding low-level protocol details.

Bio:

Ji-Yong Shin is an Associate Research Scientist in the Department of Computer Science at Yale University. His research interests are in designing novel distributed systems and exploring practical formal verification methods that can be applied to system designs. He received his Ph.D. from Cornell University, where he designed cloud storage systems with enhanced isolation support and a completely wireless datacenter.