UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Reconciling the model-implementation duality in PGo Hosseini, Shayan


Distributed systems are difficult to design and implement correctly, leading academia and industry to explore using formal methods to address these complexities. In previous work, we presented PGo, a framework for building verified distributed system implementations. PGo compiles distributed system models into executable programs. Using PGo to build systems, we face a new paradigm where PGo models serve dual roles as both models and programs. Models and programs are inherently different. Models are designed for ease of reasoning and provide a simplified representation of the system, while programs prioritize efficiency and performance for execution on the hardware. This work addresses the duality problem inherent in PGo models, where they must serve both as models and programs. We analyze various aspects of the duality we faced while building distributed systems using PGo. We propose techniques that reconcile the model-implementation duality. Additionally, we introduce a framework for constructing modular systems using PGo. Modularity is essential for building real-world distributed systems, as distributed systems are rarely implemented as monolithic systems. Our evaluation demonstrates that despite the duality problem, we can satisfy the requirements of both the model and implementation sides in complex systems. We used PGo to model, compile, and evaluate several distributed systems, including key-value stores based on Raft and primary-backup protocols, as well as Conflict-free Replicated Data Types. Our Raft-based key-value store with three nodes is model checked and has 41% higher throughput than similar verified systems.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International