Reconciling the model-implementation duality in PGo
department or school: Science, Faculty of
department or school: Computer Science, Department of
data provider: DSpace
degree campus: UBCV
creator: Hosseini, Shayan
issued: 2023-11-10T00:42:57Z
issued: 2023
related degree: Master of Science - MSc
degree grantor: University of British Columbia
description: 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.
aggregated CHO: https://circle.library.ubc.ca/rest/handle/2429/86484
note: Reconciling the Model-Implementation Duality inPGobyShayan HosseiniB.Sc., University of Tehran, 2020a thesis submitted in partial fulfillmentof the requirements for the degree ofMaster of Scienceinthe faculty of graduate and postdoctoralstudies(Computer Science)The University of British Columbia(Vancouver)November 2023© Shayan Hosseini, 2023The following individuals certify that they have read, and recommend tothe Faculty of Graduate and Postdoctoral Studies for acceptance, the thesisentitled:Reconciling the Model-Implementation Duality in PGosubmitted by Shayan Hosseini in partial fulfillment of the requirementsfor the degree of Master of Science in Computer Science.Examining Committee:Ivan Beschastnikh, Associate Professor, Computer Science, UBCSupervisorNorman C. Hutchinson, Associate Professor, Computer Science, UBCSupervisory Committee MemberiiAbstractDistributed systems are difficult to design and implement correctly, leadingacademia and industry to explore using formal methods to address thesecomplexities. In previous work, we presented PGo, a framework for build-ing verified distributed system implementations. PGo compiles distributedsystem models into executable programs.Using PGo to build systems, we face a new paradigm where PGo modelsserve dual roles as both models and programs. Models and programs areinherently different. Models are designed for ease of reasoning and provide asimplified representation of the system, while programs prioritize efficiencyand performance for execution on the hardware.This work addresses the duality problem inherent in PGo models, wherethey must serve both as models and programs. We analyze various aspectsof the duality we faced while building distributed systems using PGo. Wepropose techniques that reconcile the model-implementation duality. Addi-tionally, we introduce a framework for constructing modular systems usingPGo. Modularity is essential for building real-world distributed systems, asdistributed systems are rarely …
has type: Thesis/Dissertation
date issued: 2024-05
is shown at: 10.14288/1.0437579
language: eng
degree discipline: Computer Science
provider: Vancouver : University of British Columbia Library
publisher: University of British Columbia
rights: Attribution-NonCommercial-NoDerivatives 4.0 International
rights URI: http://creativecommons.org/licenses/by-nc-nd/4.0/
scholar level: Graduate
contributor: Beschastnikh, Ivan
type: Text
type: Software
identifier URI: http://hdl.handle.net/2429/86484