Science, Faculty of
Computer Science, Department of
DSpace
UBCV
Hosseini, Shayan
Master of Science - MSc
University of British Columbia
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.
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 implemented as monolithic systems.Our evaluation demonstrates that despite the duality problem, we cansatisfy the requirements of both the model and implementation sides incomplex systems. We used PGo to model, compile, and evaluate severaldistributed 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% higherthroughput than similar verified systems.iiiLay SummaryDesigning and implementing distributed systems accurately is challenging.In a prior work, we presented the PGo framework for building correct dis-tributed systems. PGo compiles specifications of distributed systems intoprograms. When using PGo, we encounter a new challenge: the specifica-tion we create must serve as both a simplified representation for reasoning(model) and an efficient program for execution (implementation). This studyaddresses this duality inherent in PGo specification. Our evaluation demon-strates that despite the duality, we can satisfy the requirements of both themodel and implementation sides in complex distributed systems.ivPrefaceThis thesis is based on my contributions to the following publication [29]and includes its text and material:• “Compiling Distributed System Models with PGo”.Finn Hackett, Shayan Hosseini, Renato Costa, Matthew Do, IvanBeschastnikh. 28th ACM International Conference on ArchitecturalSupport for Programming Languages and Operating Systems, 2023.I led the research and development of building distributed systems us-ing the PGo compiler toolchain and evaluated them. In Chapter 11, FinnHackett evaluated related work for comparison. Chapter 12 is based on FinnHackett’s writing of related work in the PGo paper [29]. This work has beendone under the supervision of Ivan Beschastnikh, and he provided commentsand feedback on the writing.vTable of ContentsAbstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iiiLay Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ivPreface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vTable of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . viList of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ixList of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xAcknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . xiv1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 PGo Background . . . . . . . . . . . . . . . . . . . . . . . . . 52.1 Model checking . . . . . . . . . . . . . . . . . . . . . . . . . . 62.2 TLA+ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.3 PlusCal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82.4 MPCal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102.5 PGo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132.6 Assumptions . . . . . . . . . . . . . . . . . . . . . . . . . . . 163 Model-Implementation Duality . . . . . . . . . . . . . . . . . 173.1 Models and Programs . . . . . . . . . . . . . . . . . . . . . . 17vi3.1.1 Models . . . . . . . . . . . . . . . . . . . . . . . . . . 183.1.2 Programs . . . . . . . . . . . . . . . . . . . . . . . . . 193.1.3 Languages . . . . . . . . . . . . . . . . . . . . . . . . . 203.2 Duality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204 RaftStore . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234.1 Raft Basics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234.1.1 Leader Election . . . . . . . . . . . . . . . . . . . . . . 244.1.2 Log Replication . . . . . . . . . . . . . . . . . . . . . . 254.2 Design Overview . . . . . . . . . . . . . . . . . . . . . . . . . 254.3 Checking Correctness . . . . . . . . . . . . . . . . . . . . . . . 285 Performing IO . . . . . . . . . . . . . . . . . . . . . . . . . . . 305.1 Networking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 315.1.1 Unordered Lossy Link . . . . . . . . . . . . . . . . . . 315.1.2 Reliable FIFO Link . . . . . . . . . . . . . . . . . . . 335.1.3 Relaxed Reliable Link . . . . . . . . . . . . . . . . . . 355.2 Storage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 365.2.1 File System . . . . . . . . . . . . . . . . . . . . . . . . 365.2.2 Persistent Log . . . . . . . . . . . . . . . . . . . . . . 376 Modeling and Dealing with Failures . . . . . . . . . . . . . . 396.1 Modeling Failure Behavior . . . . . . . . . . . . . . . . . . . . 406.2 Handling Failures with Failure Detectors . . . . . . . . . . . . 426.3 Resource Implementation . . . . . . . . . . . . . . . . . . . . 457 The Problem with Time . . . . . . . . . . . . . . . . . . . . . 478 Achieving High Concurrency . . . . . . . . . . . . . . . . . . 508.1 Concurrency and Duality . . . . . . . . . . . . . . . . . . . . 508.2 How We Made RaftStore Highly Concurrent . . . . . . . . . . 539 Modular Design . . . . . . . . . . . . . . . . . . . . . . . . . . 5610 Development Process . . . . . . . . . . . . . . . . . . . . . . . 60vii11 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6311.1 Evaluated Systems and Methodology . . . . . . . . . . . . . . 6311.2 Development Effort . . . . . . . . . . . . . . . . . . . . . . . . 6611.3 Model Checking Performance . . . . . . . . . . . . . . . . . . 6611.4 Performance of Raft-Based KV Stores . . . . . . . . . . . . . 6711.5 Performance of Primary-Backup KV Stores . . . . . . . . . . 7111.6 Performance of CRDT-based Systems . . . . . . . . . . . . . 7312 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 7412.1 Model-Checked DSLs . . . . . . . . . . . . . . . . . . . . . . . 7412.2 Automated Theorem-Proving . . . . . . . . . . . . . . . . . . 7512.3 Model Checking Implementations . . . . . . . . . . . . . . . . 7612.4 Go Systems Tooling . . . . . . . . . . . . . . . . . . . . . . . 7613 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78A Supporting Materials . . . . . . . . . . . . . . . . . . . . . . . 87viiiList of TablesTable 3.1 Comparison of models and programs across different aspects. 18Table 11.1 Systems we developed using PGo. Our evaluation focuseson the bolded systems: (1) RaftStoreMod, which is a modu-lar composition of RaftProto and DistKV (see Chapter 9),(2) monolithic RaftStore, (3) PBStore, and (4) PGoCRDT. 65ixList of FiguresFigure 2.1 PGo workflow. The shaded blue components must beprovided by the user. . . . . . . . . . . . . . . . . . . . . . 6Figure 2.2 Example safety and liveness properties of a lock service.ClientSet is the set of all clients in the system, and stateiis the i-th client state. . . . . . . . . . . . . . . . . . . . 7Figure 2.3 Lock server specification in TLA+. . . . . . . . . . . . . . 9Figure 2.4 Lock server specification in PlusCal. . . . . . . . . . . . . 11Figure 2.5 MPCal specification of the lock server, corresponding toFigure 2.4. . . . . . . . . . . . . . . . . . . . . . . . . . . 12Figure 2.6 The serverReceive label from the archetype definition inFigure 2.5 compiled to Go. . . . . . . . . . . . . . . . . . 15Figure 2.7 Go archetype resource interface definition. . . . . . . . . . 15Figure 2.8 Bootstrapping the compiled AServer archetype in Go. ArchetypeAServer is instantiated with appropriate resource imple-mentations. . . . . . . . . . . . . . . . . . . . . . . . . . . 16Figure 4.1 Raft servers’ state transitions. This figure is taken fromthe Raft paper [59]. . . . . . . . . . . . . . . . . . . . . . 24Figure 4.2 RaftStore architecture in a normal operation: (1) Leaderreceives a request from a client. (2) Replicates the newentry to followers by sending AppendEntries. (3) Afterreceiving a majority of responses from followers, leaderreplies back to the client. . . . . . . . . . . . . . . . . . . 26xFigure 4.3 Partial architecture of RaftStore MPCal model. Arrowsshow the interaction between archetypes and mappingmacros. The direction of each read/write arrow denotesthe direction of data flow. . . . . . . . . . . . . . . . . . . 27Figure 5.1 Unordered lossy link modeled in MPCal. . . . . . . . . . . 34Figure 5.2 Reliable FIFO link modeled in MPCal. . . . . . . . . . . . 35Figure 5.3 Modeling atomic broadcast using reliable FIFO links. . . 35Figure 5.4 A simple file system modeled in MPCal. . . . . . . . . . . 37Figure 5.5 Raft persistent log modeled in MPCal. . . . . . . . . . . . 38Figure 5.6 Raft persistent log add and remove operations. . . . . . . 38Figure 6.1 Modeling a faulty network link in MPCal. . . . . . . . . . 40Figure 6.2 Modeling crash failures in MPCal. . . . . . . . . . . . . . 41Figure 6.3 Each branch will be taken non-deterministically at run-time. This makes the process to execute handle failurebranch without even knowing that a failure has happened. 42Figure 6.4 Handling failures with a failure detector in MPCal archetypes. 42Figure 6.5 Perfect failure detector modeled in MPCal. A perfect fail-ure detector guarantees strong completeness and strongaccuracy. . . . . . . . . . . . . . . . . . . . . . . . . . . . 43Figure 6.6 Practical failure detector modeled in MPCal. Practicalfailure detector guarantees strong completeness. . . . . . . 44Figure 6.7 Failure detector and monitor execution example, when anarchetype crashes and monitor replies false to the subse-quent IsAlive request. . . . . . . . . . . . . . . . . . . . . 46Figure 6.8 Failure detector and monitor execution example, in a casewhere the the entire OS process crashed and the failuredetector detects that with a timeout. . . . . . . . . . . . 46Figure 7.1 A timer modeled as a boolean resource in MPCal. Everytime when archetype ANode gets executed, timer t is true,which means it has fired. . . . . . . . . . . . . . . . . . . 49xiFigure 8.1 Archetype SingleThread models a system which eitherdoes TaskA or TaskB at each step. PGo compiles thisarchetype into a sequential program. . . . . . . . . . . . . 52Figure 8.2 Archetypes ThreadA and ThreadB model a system whereeither does TaskA or TaskB at each step. PGo compiles thisarchetype into a concurrent program, where two archetypesrun concurrently. . . . . . . . . . . . . . . . . . . . . . . 52Figure 8.3 TLA+ compilation of Figure 8.1 and Figure 8.2. . . . . . 52Figure 8.4 Architecture of RaftStore. The left side shows the initialversion, which had one archetype. The right side showsthe new architecture that enables concurrency. Arrowsdemonstrate how we create a distinct archetype from eachbranch of the either statement in the initial version. . . 55Figure 9.1 Architecture of RaftStoreMod components. The left sideshows the high level architecture of DistKV. Each KVserver interacts with an abstract state machine replicationcomponent (SMR). The right side shows the RaftProtocomponent, where it communicates with its propose andaccept channels. . . . . . . . . . . . . . . . . . . . . . . . 59Figure 9.2 RaftStoreMod implementation architecture. On the im-plementation side, we use RaftProto to implement theabstract state machine replication (SMR) component ofDistKV. . . . . . . . . . . . . . . . . . . . . . . . . . . . 59Figure 10.1 Development process of building systems using PGo wherewe face model-implementation duality. This is an iter-ative process of model engineering and implementationoptimization. . . . . . . . . . . . . . . . . . . . . . . . . . 62Figure 11.1 Throughput of RaftStore and RaftStoreMod as comparedto various systems for a selection of standard YCSB work-loads. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68xiiFigure 11.2 Latency-throughput data of Raft-based KV systems withvarying number of concurrent clients. . . . . . . . . . . . 69Figure 11.3 Scalability of Raft-based KV systems with varying clustersize. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69Figure 11.4 Throughput of RaftStore over time with three highlightedevents: leader failure, new leader election, follower failure. 72Figure 11.5 Convergence times for PGoCRDT and Roshi. . . . . . . . 73xiiiAcknowledgmentsI had the privilege of working with Ivan Beschastnikh throughout my Mas-ter’s program. Ivan’s support has been an invaluable asset to my growth,and I have gleaned a wealth of knowledge from him. I extend my gratitudeto Finn Hackett, my primary collaborator during this period. We spentcountless hours discussing ideas and implementing cool stuff together. I amgrateful to Norm Hutchinson for serving on my thesis committee.My time as a member of the UBC Systopia lab during my Master’s wastruly remarkable. I am sincerely thankful to all the Systopians who becamemy friends and are awesome people.I also extend my thanks to Behnaz Arzani, who generously hosted meat Microsoft Research during the summer of 2022. This experience gave methe unique opportunity to engage in world-class research in the industry.My heartfelt thanks go to my parents and my younger brother. Theirunwavering support has paved the way for my achievements, and I am pro-foundly grateful for everything they have done for me.This research is supported in part by the NSERC Discovery Grants(RGPIN-202005203, RGPIN-2014-04870), by AWS through an Amazon Re-search Award, by an Azure Education Grant, and by the Institute for Com-puting, Information and Cognitive Systems (ICICS) at UBC.xivChapter 1IntroductionIf an army, that sheddeth theblood of lovers, grief raiseContent together are I and theSaki; and up its foundation, wecastHafizDistributed systems are a key part of the modern software stack. Theysupport important applications such as banking, communication, and socialnetworks. Despite decades of research and industry experience, buildingcorrect distributed systems is still notoriously hard. As a consequence, sys-tems in production often have bugs leading to degraded performance [23],outages [25, 67], and data loss [24]. For example, Roblox, an online gamingservice with more than 100 million users, experienced a 73 hours outagein November 2021 [64] due to bugs in Consul [31], a distributed key-valuestore.In recent years, developers started using formal methods to ensure thecorrectness of their systems [57]. Typically, developers create models of theirsystems and use the available tools to verify the correctness of a model.Then, they translate the model into an actual implementation, which is amanual and error-prone task. This approach leaves the final implementation1unverified, creating a gap between the verified model and the implementa-tion.PGo [29] bridges the model-implementation gap by automatically com-piling a model of a distributed system into a program in the Go programminglanguage. PGo introduces the MPCal modeling language, which is built ontop of PlusCal/TLA+ family of languages [43, 44]. For verification, PGoleverages model checking to verify the correctness of MPCal models. Onthe implementation side, PGo compiles MPCal models into Go programs.Users have to write a few lines of configuration code to make the compiledGo program executable.Building distributed systems using PGo helps developers with the model-implementation gap. However, it introduces a new paradigm where MPCalcode serves both as a model and a program. Modeling and implementa-tion have different purposes and concerns. Models are designed to facilitatereasoning and provide a simplified representation of the system under con-sideration. They aim to capture the essential aspects of the system whileabstracting away unnecessary details. By reducing complexity, models en-able easier analysis and reasoning about system behavior and properties.On the contrary, programs are intended for execution on hardware, whereefficiency and performance are key concerns. Programs operate at a lowerlevel of abstraction, taking into account specific hardware and implementa-tion considerations. While models focus on conceptual understanding andverification, programs prioritize practical execution and optimal utilizationof hardware resources. Thus, models and programs serve different purposesand operate at different levels of abstraction to fulfill their respective goals.Similarly, modeling languages and programming languages serve distinctpurposes and exhibit differences in their design and features. Programminglanguages prioritize aspects such as performance, efficiency, and ease of pro-gramming. On the other hand, modeling languages are specifically designedto facilitate the expression and analysis of systems. As a result, typically,we have different languages for writing programs and models.MPCal code is a model itself but since it is compiled into a program, ithas to fulfill the needs of a program, as well. This introduces a duality in2the MPCal code where it has two purposes, as a model and as a program.When using PGo to build systems, the development process begins withconstructing the model, which is then compiled into an executable program.As a result, considerations and constraints from the program side impactmodeling decisions. In this work, we explore the model-program duality inPGo and discuss how the two sides with different concerns can be reconciled.Managing complexity is a crucial aspect when developing large-scale sys-tems. Modularity plays a fundamental role in the managing of complexity.Mainly, modularity is vital for verified systems to manage the verificationcost [1, 15]. By decomposing the system into smaller, interconnected mod-ules, we can effectively handle the intricacies of system design and verifica-tion. This work introduces a framework for constructing modular systemsusing PGo.Throughout this work, we present RaftStore as an example to addressthe challenges arising from the duality of building a complex distributedsystem. RaftStore is a distributed key-value store database based on theRaft consensus protocol [59]. By employing RaftStore as a running example,we demonstrate how we tackled the duality concerns as a practical showcasefor the concepts and techniques discussed in this work. We built a modularversion of RaftStore, named RaftStoreMod, consisting of consensus and key-value store components. We use RaftStoreMod to demonstrate the modulardesign in an intricate distributed system.In summary, the contributions of this work are:• We propose techniques to reconcile the duality between modeling landand implementation land using the provided PGo primitives. We relyon RaftStore as a running example to show how two sides with differentconcerns can be reconciled.• We show how to build modular verified systems using PGo. This de-sign approach allows us to reduce the trusted-computing base, modelcomplexity, and model-checking cost, while building larger scale sys-tems.• Our evaluation shows that despite the duality problem, we are able3to build high performance and fault-tolerant systems while model-checking them within reasonable bounds.4Chapter 2PGo BackgroundIn the end, it is a social processthat determines whethermathematicians feel confidentabout a theorem.Richard A. De Millo, Richard J.Lipton and Alan J. PerlisPGo is a compiler toolchain that automatically translates MPCal modelsto TLA+ for model-checking. In addition, it compiles MPCal models to theGo programming language for execution.Figure 2.1 shows the PGo workflow. The left side of the workflow is theverification side, where users can model check their MPCal models. Theright side of the workflow is the implementation side, where the MPCalmodel is compiled into a Go program. Note that we use the words pro-gram and implementation interchangeably in this work. Next, we reviewthe necessary information to understand PGo and the different pieces in theworkflow. We use a distributed lock service as a running example through-out the chapter. The lock service has a central server that manages a lock.Clients request to acquire or release the lock through the network.5ModularPlusCalPlusCalTLA+PGoGoCompiledGoPGoMain(program setup)distsyslibrariesGo runtimeModel Checker (TLC)CorrectnessPropertiesDistributed deploymentAbstract model Concrete realizationFigure 2.1: PGo workflow. The shaded blue components must beprovided by the user.2.1 Model checkingModel checking is a technique used to verify whether a given model of asystem meets a specific specification. By exhaustively examining all possi-ble states of the system model, a model checker ensures that the propertiesdefined in the specification hold true in each state. Often, the model check-ing process is confined within a finite search space, limiting the scope ofexploration. If a model checker detects a state that violates a property, itgenerates a counterexample, which represents the execution trace leading tothat state.Specifications are expressed as system properties. Properties can becategorized as either safety or liveness properties [2, 40]. Safety propertiesfocus on preventing undesirable events or states from occurring within thesystem, ensuring that nothing bad happens. On the other hand, liveness6@ i, j ∈ ClientSet : i 6= j ∧ statei = HasLock∧ statej = HasLock(a) Safety property: there are no two clients that hold the lock at the same time(mutual exclusion).∀i ∈ ClientSet : (statei = WaitLock=⇒ ♦(statei = HasLock))(b) Liveness property: always () every client that waits for the lock, eventually(♦) holds the lock. Note that satisfying the safety property above does not guaranteethis fact, since a lock server that never grants the lock to any client trivially satisfiesthe safety requirement.Figure 2.2: Example safety and liveness properties of a lock service.ClientSet is the set of all clients in the system, and statei isthe i-th client state.properties emphasize the guarantee that the system eventually reaches adesirable state or accomplishes some good outcome.Figure 2.2 lists a safety and a liveness property for the lock service.2.2 TLA+TLA+ [43] is a language that employs a declarative approach to modelsystems based on set-theory and first-order logic [61]. The TLC modelchecker [78] can verify that a TLA+ model adheres to both safety and live-ness specifications within bounded limits. A TLA+ model is made of severalpredicates. Predicates define the modeled system’s initial state and the tran-sition relation describing how the system progresses with new states. Thetransitions are atomic steps in the system.For example, Figure 2.3 shows our lock server modeled in TLA+. Theinitial state is defined in the Init predicate, and the Next predicate definesthe transition relations at each step. Possible transitions to the next state7are either serverReceive or serverRespond. A variable without prime (e.g.,msg) represents the value in the old state. A variable with prime (e.g., msg′)represents the value in the new state. We modeled the network by a set ofunbounded arrays, network. The lock server has a queue denoted by thevariable q. The first client in the queue holds the lock, and the rest of theclients in the queue are waiting for the lock. In the serverReceive predicate,the server receives a request and stores it for processing if there is no otherrequest pending. During serverRespond the server processes the receivedmessage. For lock requests, the server grants the lock to the requestingclient if the queue is empty, and it adds that client to the end of its queue.For unlock requests, the server pops the requesting client from the head ofits queue and grants the lock to the next client waiting in the queue, if any.2.3 PlusCalPlusCal [44] is a modeling language for specifying algorithms. PlusCalcode can be translated to TLA+. Within PlusCal, system’s behavior isdefined procedurally, with different processes having their behavior definedby statements and interacting using control flow structures such as whileloops and if statements. To convert PlusCal specifications into TLA+, userscan utilize a PlusCal translator, which enables them to use the TLC modelchecker on PlusCal models.A PlusCal spec is comprised of one or more processes. Each process runssequentially, and different processes can run concurrently. PlusCal processesconsist of labels. Each label contains a block of statements that define anatomic step in the model. PlusCal provides a C-like goto statement thatallows jumping between different labels. We also refer to labels as criticalsections. During compilation to TLA+, each block of labels in PlusCal isconverted into a TLA+ transition. Designers must consider the trade-offpresented by labels, as incorporating more labels enables increased con-currency between labels in different processes, resulting in a more realisticmodel. However, this can lead to an exponential increase in the state spaceand its associated costs.8In the initial state, no message in the network and the1server’s queue is empty.2Init∆= ∧ network = [n ∈ NodeSet 7→ 〈〉]3∧ q = 〈〉4∧msg = Nil5Next∆= Possible transitions to the next state.6∨ serverReceive7∨ serverRespond8serverReceive∆= Receving a request from clients9∧msg = Nil10Ensure that the server’s buffer is not empty.11∧ Len(network [ServerId ]) > 012Receiving a message by reading the first element13in the server’s network buffer.14∧msg ′ = Head(network [ServerId ])15After reading the message, we can remove it from the buffer.16∧ network ′[ServerId ] = Tail(network [ServerId ])17serverRespond∆= Handling the request and responding back18∨ ∧msg .type = LockMsg19∧ q = 〈〉 ⇒20Sending a message to msg.from by adding it21to the end of recipient’s network buffer.22let dst∆= msg .from23in network ′[dst ] = Append(network [dst ], GrantMsg)24∧ q ′ = Append(q , msg .from)25∧msg ′ = Nil26∨ ∧msg .type = UnlockMsg27∧ q ′ = Tail(q)28∧ q ′ 6= 〈〉 ⇒29Sending a message to Head(q ′)30let dst∆= Head(q ′)31in network ′[dst ] = Append(network [dst ], GrantMsg)32∧msg ′ = Nil331Figure 2.3: Lock server specification in TLA+.9Figure 2.4 shows our lock server modeled in PlusCal. It has the samesemantics as the TLA+ model in Figure 2.3. Besides the usual control flowstatements, PlusCal has two other essential statements that do not typicallyexist in programming languages: (1) The await statement has the formawait cond, where cond is a boolean expression. await blocks the processexecution until cond becomes true. For example, in line 11 of Figure 2.4, theserver blocks until its network queue becomes non-empty. (2) The eitherstatement has the form either {clause1} or {clause2}, where clause1 andclause2 are statements. either nondeterministically executes one of theexecutable clauses. The either statement is executable if at least one of theclauses is executable; otherwise, the process blocks.PlusCal mixes the details of the system and its environment such thatit is not possible to distinguish them. For example, in Figure 2.4, the lockserver logic, which is the definition of the system, is mixed with its environ-ment, the buffered network.2.4 MPCalMPCal is a modeling language built on top of PlusCal. MPCal providesextra abstractions to separate the system definition and its environment.Having this separation allows the PGo compiler to compile MPCal mod-els into implementations. PGo compiles MPCal code into PlusCal, whereusers can use the TLC model checker for verification. MPCal adds threeadditional abstractions to PlusCal: (1) archetype definitions, (2) archetypeinstantiations, and (3) mapping macros.Archetypes are similar to PlusCal processes, but they only contain sys-tem definitions. An archetype does not have access to global variables sim-ilar to a PlusCal process. An archetype only can interact with environmentinstances, which are the parameters that an archetype takes. Archetype pa-rameters are called resources. Resources describe archetypes’ environmentdependencies. The definition of an archetype contains all the necessary in-formation for PGo to create a functional system, including the interfacingpoints where the system definition interacts with its environment.101 variables network = [id \in NodeSet |-> <<>>];23 \* fair keyword specifies assumption of fair scheduling4 fair process (Server = 1)5 variables msg, q = <<>>;6 {7 serverLoop:8 while (TRUE) {9 serverReceive:10 \* blocks the process until the there is some message available11 await Len(network[self]) > 0;12 msg := Head(network[self]);13 network[self] := Tail(network[self]);14 serverRespond:15 if (msg.type = LockMsg) {16 \* if q is empty17 if (q = <<>>) {18 network[msg.from] := Append(network[msg.from], GrantMsg);19 };20 q := Append(q, msg.from);21 } else if (msg.type = UnlockMsg) {22 q := Tail(q);23 \* if q is not empty (/= is the not equals operator)24 if (q /= <<>>) {25 network[Head(q)] := Append(network[Head(q)], GrantMsg);26 };27 };28 };29 }Figure 2.4: Lock server specification in PlusCal.Archetypes access environment through their resources and mappingmacros define how resources are working. Mapping macros define the be-havior of resources (e.g. buffered network) through a simple read/write API.PGo does not compile mapping macros into implementation since they con-tain verification-specific parts of the model, such as semantics of an abstractenvironment.Archetype instantiations provide existing archetypes with the right setof resources and connect resources to mapping macros to define the behaviorof resources.Figure 2.5 shows the lock server modeled in MPCal. Archetype AServer111 archetype AServer(ref network[_])2 variables msg, q = <<>>;3 {4 serverLoop:5 while (TRUE) {6 serverReceive:7 msg := network[self];8 serverRespond:9 if (msg.type = LockMsg) {10 if (q = <<>>) {11 network[msg.from] := GrantMsg;12 };13 q := Append(q, msg.from);14 } else if (msg.type = UnlockMsg) {15 q := Tail(q);16 if (q /= <<>>) {17 network[Head(q)] := GrantMsg;18 };19 };20 };21 }2223 mapping macro ReliableFIFOLink {24 read {25 await Len($variable) > 0;26 with (readMsg = Head($variable)) {27 $variable := Tail($variable);28 yield readMsg;29 };30 }31 write {32 yield Append($variable, $value);33 }34 }3536 variables network = [id \in NodeSet |-> <<>>];3738 fair process (Server = 1) == instance AServer(ref network[_])39 mapping network[_] via ReliableFIFOLink;Figure 2.5: MPCal specification of the lock server, corresponding toFigure 2.4.12is defined on line 1, and it has a resource, ref network[_]1. The serverreceives a message from the network in line 7 by reading from the networkparameter. The behavior of this read operation is defined in the read sec-tion of the ReliableFIFOLink mapping macro, starting on line 24. Then,in the serverReceive label, the server processes the received message. Wesend a message by writing to the network variable. Similar to the readcase, the behavior of network write is defined in the write section of theReliableFIFOLink mapping macro.Mapping macros define the behavior of read/write operations on re-sources by injecting code wherever operations are used. These can be ar-bitrary PlusCal code, which the PGo compiler inserts into an instantiatedarchetype definition’s body. Each mapping macro has a read and a write sec-tion that defines the behavior of read and write operations, respectively. Ex-pressions in these sections have access to two special parameters. $variableis the underlying state variable to operate on, and $value is the value writ-ten by the caller (an archetype). In addition, the yield(_) statement yieldsthe computed output of its expression as the result of the operation.Archetype AServer is instantiated on line 1 of Figure 2.5 with ref network[_]as its parameter. The network is a global variable defined on line 36.The statement mapping network[_] via ReliableFIFOLink on line 39 de-clares that the behavior of network resource is being defined by the ReliableFIFOLinkmapping macro.2.5 PGoUsing the PGo compiler, the MPCal code can be translated to PlusCal,and then it can be translated to TLA+. Users can express the propertiesof Figure 2.2 in TLA+ and use the TLC model checker to verify the modelagainst these properties.PGo compiler translates archetypes into implementations in Go. PGoensures that the compiled Go program has the same semantics as its corre-1The ref keyword means this parameter is a passed by reference. The [_] syntaxmeans indexed access and restricts accessing network resource to be only indexed.13sponding MPCal. The distsys Go library is responsible for providing suchguarantees. An essential part of distsys is offering atomicity guarantees foreach label while maximizing concurrency. distsys executes each archetypein a main loop that provides the necessary semantics of critical section andcontrol flow.Figure 2.6 shows the serverReceive critical section of Figure 2.5 compiledinto Go. This is almost a direct translation from MPCal to Go. PGocompiles each archetype into a set of critical sections, and the distsys’smain loop is responsible for correctly executing them. The serverReceivecritical section acquires access to resources msg and network in lines 6-7. Notethat it treats both archetype parameters and local variables as resources;however, the access calls are slightly different. The critical section body hasan archetype interface as input iface that allows the archetype to accessits resources through read and write calls, as demonstrated in lines 11 and15. These correspond to operations on line 7 of Figure 2.5. Line 19 is theimplicit jump at the end of the serverReceive label where it finishes, andthe program goes to the next label, serverRespond.Resource implementations have to follow the interface defined in Fig-ure 2.7. Inspired by the two-phase commit protocol, this API allows thedistsys library to provide correct linearizability semantics for critical sec-tions. distsys main loop starts executing a critical section by applying thechanges temporarily. Then it performs the pre-commit stage across all par-ties participating in a critical section. The main loop proceeds to the com-mit stage if PreCommit does not return any error for any of the resources.In the commit stage, each resource commits the critical section changes. Ifat least one of the resources involved in the critical section fails in the pre-commit stage, the main loop aborts the critical section by calling Abort onall resources and tries to execute the critical section again. Commit alwayssupposed to succeed and this assumption might cause liveness issues, suchas blocking the process execution forever. In addition, distsys provides alibrary of commonly used resources such as networking and storage.The user configures the generated Go code with the resource implemen-tations. Figure 2.8 shows the code that bootstraps the compiled AServer141 distsys.MPCalCriticalSection{2 Name: "AServer.serverReceive",3 Body: func(iface distsys.ArchetypeInterface) error {4 var err error // setup5 _ = err6 msg := iface.RequireArchetypeResource("AServer.msg")7 network, err := iface.RequireArchetypeResourceRef("AServer.network")8 if err != nil {9 return err10 } // read network[self]11 networkRead, err := iface.Read(network, []tla.Value{iface.Self()})12 if err != nil {13 return err14 } // msg := <value>15 err = iface.Write(msg, nil, networkRead)16 if err != nil {17 return err18 }19 return iface.Goto("AServer.serverRespond")20 },21 },Figure 2.6: The serverReceive label from the archetype definition inFigure 2.5 compiled to Go.1 type ArchetypeResource interface {2 Abort()3 PreCommit() error4 Commit()5 ReadValue() (tla.Value, error)6 WriteValue(value tla.Value) error7 }Figure 2.7: Go archetype resource interface definition.archetype. The user begins by creating an MPCalContext object for eacharchetype. MPCalContext contains the main loop for its given archetype. Itrequires an archetype name, an archetype instance, and a list of archetyperesources. In this case, we provided TCPMailboxes for the network resource.Lines 7 to 16 configure the TCPMailboxes with the right set of network ad-dresses. Finally, the user runs the instantiated archetype in line 18.151 ctxServer := distsys.NewMPCalContext(2 serverId,3 AServer,4 distsys.EnsureArchetypeRefParam(5 "network",6 resources.NewTCPMailboxes(func(v tla.Value)7 (resources.MailboxKind, string) {8 addr := addressMap[v.AsNumber()]9 var kind resources.MailboxKind10 if v.Equal(serverSelf) {11 kind = resources.MailboxesLocal12 } else {13 kind = resources.MailboxesRemote14 }15 return kind, addr16 })),17 )18 err := ctxServer.Run()Figure 2.8: Bootstrapping the compiled AServer archetype in Go.Archetype AServer is instantiated with appropriate resource im-plementations.2.6 AssumptionsAs described earlier, PGo has two workflows, verification and implementa-tion. In the verification workflow, the user trusts the MPCal to PlusCaltranslation process provided by the PGo compiler. Moreover, users trustPlusCal to TLA+ translation and the TLC model checker. TLC assumesthe user has provided the right properties in the given specification. Onthe implementation side, users trust the MPCal compilation with PGo, thedistsys library, including all the resource implementations. Also, users haveto trust the Go runtime and the underlying operating system.16Chapter 3Model-ImplementationDualityAren’t programs simpler thanlogical formulas? The answer isno.Leslie LamportPGo offers two distinct workflows, namely verification and implemen-tation, which were previously discussed in Chapter 2. In each of theseworkflows, the MPCal code is utilized as the source code, which is subse-quently compiled into different target languages to serve both as a modeland a program. We define this as model-implementation duality in MPCalcode, where the same code is employed to address two different concerns.This section discusses the similarities and differences between models andprograms, and provides additional insight into the duality problem.3.1 Models and ProgramsA model and a program both involve describing a system in an abstractformal language. Models and programs are defined based on abstractions;however, their abstraction level is different. Models and programs serve17Table 3.1: Comparison of models and programs across different as-pects.Program ModelPurposeExecutionon hardwareReasoningby human/toolsNon-functionalrequirementCorrectness CorrectnessAbstraction level Concrete AbstractPerformancemeasureExecution time,resource usageDegree and costof reasoningComplexity High LowVerification cost High LowLanguage Closer to hardware Closer to mathdifferent purposes. The primary objective of a program is to be executed ona hardware platform, such as a CPU. In contrast, models are not necessarilydesigned for execution. The primary goal of a model is to enable reasoningabout a system. These distinct purposes result in different abstraction levelsand requirements for models and programs, while an essential requirementfor both models and programs is correctness. Table 3.1 summarizes thecomparison of models and programs across different aspects.3.1.1 ModelsDevelopers create models to aid in the analysis and reasoning of their sys-tems. This reasoning can be performed either manually by humans or au-tomatically by tools. For example, Unified Modeling Language (UML) [4]is a modeling language intended to visualize software systems primarily forhuman analysis. In contrast, the TLA+ modeling language is based on logicand enables automated reasoning about models through tools such as modelchecking, automated theorem proving, and randomized testing.Models are designed to facilitate reasoning, and as such, they tend tobe simpler than programs and abstract away details as much as possible.Typically, models are only a few hundred lines of code, making them easyto modify. In addition, models focus on one specific concern and abstract18away unrelated ones. For example, consider a model of a replication protocolwhere nodes communicate through the network. Such a model would focussolely on the replication protocol and would abstract away other systemcomponents, such as the network. To achieve this, the model would onlyuse a simple abstract representation of the network that has the necessaryguarantees for the replication protocol.Models often utilize math because it offers well-defined semantics forvarious constructs, making reasoning easier [42]. Models tend to use math-ematical objects like sets and vectors which are used instead of complexobjects and data structures. Unlike programs, models are not necessarilyexecutable. Models typically adopt a declarative approach and are designedto specify the what rather than the how. Consequently, a model may notdefine a single method of computation, but instead they may declare classesof computation [45]. An example of this is the either statement in MPCal,which indicates that one of several possibilities may occur without specifyingwhich.3.1.2 ProgramsPrograms are designed to be executed on hardware and, as such, they aremore concrete than models, with abstractions that are closer to the under-lying hardware. Programs operate in real environments and need to imple-ment the full stack of the underlying system they rely on. For instance, anetworked system needs to have the complete network stack implementationin order to interact with it. Due to the level of abstraction, programs areoften large. It is not unusual to have programs consisting of hundreds ofthousands of lines of code.A vital requirement for programs is execution performance, which in-cludes factors such as execution time and resource usage (e.g., CPU, mem-ory, and disk). To meet performance and efficiency requirements, programsoften become increasingly complex. This complexity, combined with theirlarge size, can make them difficult to change over time.The complexity of programs presents a significant challenge in verifying19their correctness. As a result, developers often rely on techniques withweaker guarantees, such as testing, to analyze program correctness.3.1.3 LanguagesThe distinct goals and concerns associated with models and programs ne-cessitate the use of different languages to express them. Modeling languagesaim to enhance the understandability of models and enable verification oftheir correctness.Different modeling languages are tailored for specific types of analy-sis. Unified Modeling Language (UML) and Systems Modeling Language(SysML) [22] are designed to visualize software systems, making them eas-ier to understand. Alloy [36], on the other hand, is a declarative modelinglanguage based on first-order logic that can be used to express complex struc-tural constraints and behavior in software systems. Meanwhile, TLA+ andPlusCal are well-suited for specifying concurrent and distributed systems.Isar [70] and Gallina [68] are specification languages for the Isabelle [70]and Coq [69] automated theorem provers, respectively, and are particularlyeffective for writing proofs.Programming languages prioritize execution optimization and ease ofwriting large programs. Each programming language offers its unique set offeatures. For instance, C is a low-level programming language that enableshigh performance, while a language such as Java provides garbage collec-tion, which removes the memory management burden from programmers.However, such convenience comes at the cost of performance.3.2 DualityWe discussed that models and programs have different purposes and levelsof abstraction. When the same code serves both as a model and a program,it has to satisfy two different set of goals and even has to operate in twodifferent levels of abstraction, where models are abstract and programs andimplementations are concrete. We call this model-implementation duality.The PGo workflow begins with the construction of a system model in20MPCal. As the model is compiled into a program, the requirements and con-siderations of the program side begin to impact the model. This integrationof program-specific concerns into the model introduces duality challenges.The main idea behind MPCal is to provide abstractions that effectivelyseparate the concerns of the model and the program. However, effectivelyutilizing these abstractions to build complex systems and navigating throughthe duality can be challenging.Archetypes serve as a common system definition that remains consistentbetween the model and the compiled program in PGo. As a result, thePGo compiler compiles archetypes into the Go code. On the other hand,mapping macros define the system environment, where the model and pro-grams operate at different levels of abstraction. Hence, users provide re-source implementation for mapping macros. The first design considerationrevolves around determining the appropriate division between archetypesand mapping macros in terms of what functionality should be included ineach. Archetypes must be able to compile into executable programs. Writ-ing a model that does not compile into a meaningful program is easy. Wediscuss an example illustrating this point in Chapter 6 in the context offault-tolerant systems. When it comes to mapping macros, it is crucial toprovide resource implementations with similar guarantees. Another pointto consider is that overloading mapping macros with excessive responsibil-ities can increase the trusted computing base (TCB) size, as the resourceimplementations may not be fully verified.Models and programs operate at different levels of abstraction, leadingto fundamental differences between them. For example, there is no notion oftime in an MPCal model, while programs need timing guarantees for variousreasons. Programs require efficient IO and memory access to be performant,while in MPCal models, we only have access to high-level immutable datatypes. Duality reflects programs’ performance optimization concerns on themodel side.Similarly, implementation-side requirements can introduce complexityinto models. For instance, programs aiming for improved performance oftenrely on concurrency. However, a highly concurrent system increases com-21plexity, enlarges the state space, and escalates the cost of model checking.This presents a trade-off in terms of reflecting performance optimization re-quirements in the model while maintaining a manageable level of reasoningcomplexity.In the next chapter, we present an overview of RaftStore, a distributedkey-value store we built using PGo. We use RaftStore as a running examplein the rest of the work, where we more precisely discuss different aspects ofduality.22Chapter 4RaftStoreIn this work, we leverage PGo to develop a distributed key-value store calledRaftStore, which is built upon the Raft consensus protocol. RaftStore servesas our primary example throughout this work. This chapter provides anoverview of RaftStore, starting with a concise review of the Raft consen-sus protocol. Subsequently, we delve into the architecture of RaftStore,highlighting its extended functionalities, including the integration of clientinteraction and a key-value store layer.4.1 Raft BasicsConsensus algorithms are commonly formulated as a state machine replica-tion problem, which can be solved using a replicated log. In this approach,each server maintains a log, with each entry representing a command forexecution. The consensus algorithm ensures that the log remains consistentamong all servers containing the same set of commands in the same order.Raft consensus protocol works by electing a distinguished leader. Theelected leader replicates the commands it receives from clients to otherservers and tells them when it is safe to apply log entries to their statemachines. A Raft cluster consists of multiple servers, each of which can bein one of three states: follower, candidate, or leader. Under normal opera-tion, there is one leader, and all other servers are followers. A follower server23Figure 4.1: Raft servers’ state transitions. This figure is taken fromthe Raft paper [59].recognizes the leader and replicates its log entries. The leader server is re-sponsible for accepting new client requests and replicating them across thefollowers. In the candidate state, a server is not a follower nor a leader andis running an election round to become the new leader. Figure 4.1 depictsthe transitions between different server states.Raft divides time into terms. Terms act as a logical clock [41] and eachserver stores its monotonically increasing clock in its currentTerm variable.Raft guarantees there is at most one leader at any given term.We can divide the Raft protocol into two parts: (1) leader election:servers select a new leader for the cluster when no leader exists or the pre-vious one has failed. (2) log replication: the elected leader replicates newlog entries to the other servers and notifies them when they can apply a logentry to their state machine.4.1.1 Leader ElectionInitially, all the servers in a Raft cluster start in the follower state. Serversrely on heartbeats to initiate a leader election round. A follower remainsin the follower state if it receives period heartbeats. A leader periodicallysends heartbeat messages to followers. A follower times out if it does notreceive a heartbeat after a while. Then, it increases its currentTerm by one,transitions into the candidate state, and starts a new election. A candidatenode sends RequestVote messages to all other servers to run an election24round. A candidate wins an election if it receives votes from at least amajority of nodes. A candidate might become a follower if it receives aheartbeat message from another server. After some time, if none of thesehappen, the candidate times out and starts another election round.4.1.2 Log ReplicationAfter a leader has been elected in a Raft cluster, it begins to process clientrequests. The leader adds each request to its log and then replicates it toother servers in the cluster through AppendEntries messages. These mes-sages also serve as heartbeats for leader election. Raft guarantees that allcommitted log entries are durable and will eventually be executed by allavailable servers’ state machines. An entry is considered committed oncethe leader has successfully replicated it on a majority of the servers in thecluster. Each Raft server stores the index of the latest log entry known to becommitted in a local variable commitIndex, which increases monotonically.4.2 Design OverviewRaftStore is a distributed key-value store that uses the Raft protocol toreplicate data among servers. RaftStore has a cluster of servers. Servers im-plement the Raft protocol with a key-value dictionary as their state machine.Clients interact with the cluster by sending requests to the leader. Clientinteraction is implemented as an extension of the Raft protocol [58, 59].Figure 4.2 shows RaftStore in a normal operation, where one server is theleader and interacts with the clients.RaftStore MPCal model has several archetypes and mapping macros.Figure 4.3 shows a partial architecture of RaftStore MPCal model, includ-ing some of its archetypes and mapping macros. Two IO resources arebeing used in a server: net is the network, and log is the Raft log thatgets persisted on disk. Servers have other resources such as failure detectorsthat they use for fault-tolerance and several timers such as leaderTimeoutfor leader election. In addition, a Raft server has several variables thatare shared among its archetypes. These variables include the server state25Raft clusterClient LeaderFollowerFollowerFollowerFollowerPut(k, v)AppendEntriesAppendEntriesAppendEntriesAppendEntriesOKFigure 4.2: RaftStore architecture in a normal operation: (1) Leaderreceives a request from a client. (2) Replicates the new entryto followers by sending AppendEntries. (3) After receiving amajority of responses from followers, leader replies back to theclient.(state), current term (currentTerm), commit index (commitIndex), and can-didate ID that the server is voted for in the current term (votedFor).A RaftStore server has several archetypes that run concurrently. Thesearchetypes are:• AServerHandler handles the incoming messages in a server.• AServerRequestVote starts a new election round in case of a leadertimeout.• AServerBecomeLeader detects if the current server has a quorum of26votes and then promotes itself to be the leader.• If the current server is the leader, AServerAppendEntries broadcastsnew entries.• AServerAdvanceCommitIndex increases the commit index and repliesback to the clients.The RaftStore client consists of one archetype. The user-facing archetypeAClient relays input requests from a channel (reqCh) to instances of AServervia ReliableFIFOLink. It passes corresponding responses to the user via thechannel (respCh).AServerBecomeLeaderAServerAppendEntriesAServerRequestVoteappendEntriesChChannellogPersistentLognetReliableFIFOLinkAServerHandlerleaderTimeoutTimerAServerAdvanceCommitIndexShared Variables: - state- commitlndex- currentTerm- votedForWrite WriteWriteWriteWriteReadReadReadReadWriteAClientreqChChannelnetReliableFIFOLinkrespChChannelIncomingRequestReceivedResponseWriteReadWriteReadRead(a) Architecture of MPCal Raft server(b) Architecture of MPCal Raft clientArchetype resourceMapping MacroLegend:Figure 4.3: Partial architecture of RaftStore MPCal model. Arrowsshow the interaction between archetypes and mapping macros.The direction of each read/write arrow denotes the direction ofdata flow.274.3 Checking CorrectnessWe specified five properties of the Raft protocol in the RaftStore MPCalmodel. These properties are:• Election Safety: in every term there is at most one elected leader.• Leader Append-Only: a leader only appends new entries to its log,without changing or deleting the log entries.• Log Matching: If there exists an entry with the same index and termin two logs, it indicates that the logs are identical for all entries untilthe specified index.• Leader Completeness: When a log entry is committed during aterm, it implies that the same entry will be found in the logs of theleaders of subsequent higher-numbered terms.• State Machine Safety: Once a server has successfully applied a logentry to its state machine at a specific index, it guarantees that noother server will apply a different log entry for that same index.We used the TLC model checker for the RaftStore model with the prop-erties above. In the model checking mode, TLC explores all the possiblestates the model allows using breadth-first search by default. We boundedthis search by the number of servers, clients, failures, election rounds, andthe number of entries committed to the log.The Raft protocol may not always maintain liveness in an asynchronousnetwork, as the FLP result indicates [19]. However, in scenarios that do notreach the worst-case conditions, Raft is designed to be capable of electinga leader and making progress. The inherent randomness observed in real-world environments enables consensus systems to function effectively despitethe inherent impossibility of achieving consensus.We have specified two liveness properties for RaftStore:• Election Liveness: At any given point, eventually a server will beelected as the leader.28• Client Progress: A client eventually receives a response for the re-quest it had sent. Note that a client can retry and send a requestmultiple times.These properties always get violated during model checking since TLCexplores all possible states. For example, in the execution path where serverskeep timing out before having a majority for election, the election livenessproperty will be violated. We used TLC simulation mode to ensure thatRaftStore is live in a real environment. In simulation mode, TLC startsfrom a randomly selected initial state and chooses the next step randomlyup to a limited number of steps. We expect our liveness properties to holdduring simulation mode with enough steps.29Chapter 5Performing IOPessimists sound smart.Optimists make money.Nat FriedmanReal-world applications often use input/output (IO) operations, such asnetworking and storage, to interact with their environment. However, therepresentation and treatment of IO in models and programs differ signifi-cantly. In models, IO is typically abstracted due to two main reasons. First,the model’s primary focus is often not the IO operation itself. In addition,executing actual IO operations can be costly and time-consuming. As a re-sult, models tend to simplify and abstract IO operations, making them moreconcise and straightforward. Conversely, programs must handle IO opera-tions comprehensively, considering their full intricacies and complexities.IO operations are often regarded as part of the system environment. Inthe context of RaftStore, we consider IO devices such as the network andpersistent log to be elements of the system environment, distinct from thesystem’s core definition, which encompasses the Raft protocol and the key-value store layer. In an MPCal model, IO operations can be abstractedusing mapping macros. Each mapping macro corresponds to a resource im-plementation on the implementation side. These resource implementationsmust adhere to the resource API defined in Figure 2.7. Modeling various IO30interfaces using simple read/write APIs of mapping macros presents a chal-lenge. Ensuring consistent guarantees across both the IO mapping macrosand resource implementations can be difficult, particularly when striving foroptimal performance.Next, we will explore the process of constructing fundamental IO devices,such as networking and storage, using PGo.5.1 NetworkingThe link abstraction serves as a representation of the network components ina distributed system. In this work, we assume a bidirectional link connectsevery pair of nodes, resulting in a topology that ensures complete connec-tivity among all nodes. However, various topologies may be employed inpractical implementations to realize this abstraction, potentially utilizingrouting algorithms [6].Link abstractions must be defined to be modeled effectively in MPCal,and a corresponding resource implementation can be provided. Links re-source implementations must have the same guarantees as the resource inthe MPCal model.5.1.1 Unordered Lossy LinkA simple link abstraction is an unordered lossy link that connects two nodes.Two parties can send messages to each other, but the unordered lossy linkguarantees neither message delivery nor the order. Hence, node A can senda message m to node B, and B might not receive m or it might receive mbefore another message m′ that A has sent before m.Figure 5.1 illustrates a model of an unordered lossy link in MPCal. Eachnode has a network queue, and UnorderedLossyLink utilizes it to model thelink abstraction. In the read part of the UnorderedLossyLink mapping macro,we wait until some message is available in the network queue. We use thewith statement to randomly select one of the messages from the queue, notonly the first one. This modeling approach captures the unordered nature ofthe link. In the write section of the mapping macro, we employ the either31statement for non-deterministic behavior, allowing the message to either beadded to the queue or discarded. This modeling strategy represents thelossy characteristic of the link.It is important to note that in our simulation, we utilized nondetermin-ism to model message loss and out-of-order delivery. However, these aspectsare inherent properties of the environment in the implementation. There-fore, the actual implementation does not need to simulate them explicitly.The unordered lossy link resource implementation makes its best effort to de-liver messages, but it does not incorporate specific mechanisms to guaranteemessage delivery and ordering. Message loss and reordering are propertiesthat arise naturally from the system environment during runtime.To implement the UnorderedLossyLink mapping macro, a resource imple-mentation must adhere to the ArchetypeInterface interface in Figure 2.7.In the absence of delivery and ordering guarantees we can use the UDPprotocol for the implementation of this mapping macro, hence we refer tothe implementation as UDP mailboxes. UDP mailboxes must handle twodistinct cases: local mailbox, which serves received messages through theReadValue method, and remote mailboxes, responsible for transmitting mes-sages to other nodes via the WriteValue method. It is important to notethat a local mailbox does not support the WriteValue method, while remotemailboxes do not support the ReadValue method.A remote UDP mailbox is responsible for sending messages to a specificremote node. It buffers written values in a local buffer. In case of an abort,it discards the buffer content. In case of a commit, it sends the bufferedmessages through a UDP socket to its remote node without waiting for anack. Note that we can skip the pre-commit phase since UnorderedLossyLinkdoes not guarantee message delivery.A local UDP mailbox is responsible for handling received messages fromall nodes. It has a queue to store these received messages. When theReadValue method is invoked, the local UDP mailbox removes the first mes-sage in the queue, returns it as the result, and stores it in a temporary buffer.If the execution of the critical section is successful, the local UDP mailboxdiscards the contents of the temporary buffer. However, in the event of an32abort, the messages in the temporary buffer are added back to the headof the queue. If no message is available during a ReadValue call, the localmailbox returns an error causing the critical section to abort, promptingthe PGo runtime to execute the critical section again. This results in busywaiting instead of the blocking on archetypes’ goroutines.The primary challenge in building a resource implementation lies in man-aging MPCal’s atomicity semantics. The ArchetypeInterface simplifies thisprocess by reducing it to implementing a flexible interface. The key aspecthere is that the interface does not have to be as expensive as a full two-phasecommit protocol. Consequently, in the resource implementation discussedearlier, we could skip the pre-commit phase due to the weak guarantees ofunordered lossy links.The unordered lossy link has an efficient resource implementation. Thecost of sending and receiving messages is the same as normal send andreceive operations. Using the UDP protocol further avoids the intricaciesassociated with more complex protocols like TCP, leading to potential per-formance improvements in specific environments. However, it is importantto note that model checking becomes expensive when using unordered lossylinks due to the increased non-determinism in the model. As a result, weopted not to employ unordered lossy links in most of the systems built inMPCal, including RaftStore, prioritizing model checking efficiency for thesescenarios.5.1.2 Reliable FIFO LinkA reliable FIFO link guarantees both delivery and order to senders andreceivers. Figure 5.2 shows a mapping macro that models this link in MPCal,the network model that we used in the lock server example in Chapter 2 andthe RaftStore MPCal model.Reliable FIFO links combined with the semantics of MPCal labels arepowerful as we can use them to implement atomic broadcast. The AtomicBroadcastarchetype, depicted in Figure 5.3, transmits a message to two nodes withina label. Since labels execute atomically, either both nodes receive the mes-331 mapping macro UnorderedLossyLink {2 read {3 await Len($variable) > 0;4 with (readMsg \in $variable) {5 $variable := $variable \ readMsg;6 yield readMsg;7 };8 }9 write {10 either {11 yield $variable;12 } or {13 yield $variable \cup {$value};14 };15 }16 }Figure 5.1: Unordered lossy link modeled in MPCal.sage or none of them. This characteristic poses a challenge for the resourceimplementation of the ReliableFIFOLink, as the critical section can be ascomplex as a full consensus round [9, 11].The resource implementation of ReliableFIFOLink utilizes the TCP pro-tocol for reliable packet transmission over the network, referred to as TCPmailboxes. Similar to UDP mailboxes, TCP mailboxes handle local and re-mote mailboxes separately. The implementation of TCP mailboxes ensuresthat all nodes participating in a critical section either receive all messages inthe same order or none of them receive anything. Thus, TCP mailboxes im-plement the full two-phase commit protocol [26] in the ArchetypeInterface.During the pre-commit phase, TCP mailboxes ensure that all participatingnodes agree on the messages and their order before attempting to committhe critical section. If the pre-commit phase fails, TCP mailboxes abortthe critical section. TCP mailboxes assume the commit phase always suc-ceeds. This is based on the ArchetypeInterface assumptions and may causesliveness issues as mentioned in Chapter 2.341 mapping macro ReliableFIFOLink {2 read {3 await Len($variable) > 0;4 with (readMsg = Head($variable)) {5 $variable := Tail($variable);6 yield readMsg;7 };8 }9 write {10 yield Append($variable, $value);11 }12 }Figure 5.2: Reliable FIFO link modeled in MPCal.1 archetype AtomicBroadcast(ref network[_]) {2 lbl:3 network[NodeA] := "hi";4 network[NodeB] := "hi";5 }Figure 5.3: Modeling atomic broadcast using reliable FIFO links.5.1.3 Relaxed Reliable LinkPerforming a full consensus round for every network send introduces signifi-cant overhead. However, in many cases, this additional cost can be avoided.For instance, consider the serverReceive operation presented in Figure 2.5within Chapter 2, which involves a single network operation. In this sce-nario, employing TCP mailboxes that implement the complete two-phasecommit protocol would result in unnecessary overhead. Since there is onlyone network send operation within the critical section, and the remainingoperations are local and do not trigger an abort, we can optimize the pro-cess. After sending the message and receiving an acknowledgment for itsdelivery, we can be confident that the execution of the critical section willsucceed. As a result, we can safely skip the pre-commit and commit phases.PGo empowers users to mitigate the additional performance overheadassociated with reliable FIFO links by leveraging extra domain knowledgeto relax resource semantics. In the case of the serverReceive critical section,35a relaxed resource implementation can be employed. This implementationcan simplify the pre-commit and commit phases, treating them as triviallysuccessful and only sending messages without requiring coordination for fail-ure cases. Our relaxed implementation of TCP mailboxes assumes that noabort will occur during execution. Consequently, if an abort does happen,the implementation will panic. To achieve the best performance, we usedthe relaxed version of TCP mailboxes in the implementation of RaftStore.This approach of semantic weakening can be applied to various relevantscenarios with careful consideration. It provides a means to prioritize perfor-mance over heavier-weight correctness guarantees when necessary. However,it is important to note that these relaxations may increase the size of thetrusted computing base as they deviate from the complete implementationof an MPCal resource definition. Nevertheless, through developer disciplineand good practices, we have observed that these trade-offs can be effectivelymanaged while still leveraging the benefits of protocol-level verification. Weleave automated methods of ensuring the correctness of these relaxations tofuture work.5.2 StorageStorage is a crucial IO device for storing data. Storage devices offer variousinterfaces, including block, file system, log, and object. Effectively modelingthese storage interfaces is essential to achieve high performance. We delveinto the techniques and strategies employed in this chapter to ensure efficientmodeling, enabling us to optimize performance with storage operations.5.2.1 File SystemThe file system is a fundamental abstraction that facilitates working withstorage systems. In our modeling approach, we represent the file systemusing a map data structure. Each element of the map will refer to a file, withkeys and values being required to be string-typed, and keys being requiredto refer to valid paths (or create-able paths, if a key is written to before itis read). The file system model in MPCal is illustrated in Figure 5.4.361 mapping macro FileSystem {2 read { yield $variable; }3 write { yield $value; }4 }56 variable fs = [id \in NodeSet |-> []];Figure 5.4: A simple file system modeled in MPCal.The resource implementation of the FileSystem mapping macro incor-porates a buffering mechanism for written values, which temporarily storesthem in memory. Upon invoking the Commit operation, the implementa-tion atomically writes the buffered values to a specified location within thefile system. Conversely, in the event of an abort, the in-memory buffer issimply discarded. Given our assumption that writing to the underlying filesystem is always possible, the pre-commit phase trivially succeeds. This de-sign efficiently handles file system operations while maintaining the desiredsemantics and guarantees of the FileSystem mapping macro.5.2.2 Persistent LogRaftStore has a log that has to be persisted on disk. The log supports thefollowing operations:• Reading a range of elements within the log.• Appending one or more elements to the end of the log.• Removing one or more elements from the end of the log.The file system abstraction does not align well with the requirementsof a log, where elements are added or removed from the end. To addressthis, we have devised an alternative approach to model the log in a waythat provides a streamlined interface within the MPCal specification. ThePersistentLog mapping macro, depicted in Figure 5.5, embodies our logspecification in MPCal. The SubSeq function there returns a subsequenceof log between the given indexes. Leveraging a list as the underlying data371 mapping macro PersistentLog {2 read {3 yield $variable;4 }56 write {7 if ($value.cmd = LogConcat) {8 \* \o is the concatenation operator9 yield $variable \o $value.entries;10 } else if ($value.cmd = LogPop) {11 yield SubSeq($variable, 1, Len($variable) - $value.cnt);12 };13 }14 }Figure 5.5: Raft persistent log modeled in MPCal.1 log[i] := [2 cmd |-> LogConcat,3 entries |-> entries4 ];56 log[i] := [7 cmd |-> LogPop,8 cnt |-> count9 ];Figure 5.6: Raft persistent log add and remove operations.structure for the log, the PersistentLog mapping macro defines the seman-tics of read and write operations. In a read operation, the entire list is sim-ply returned. However, the write operation is more intricate, as it requiresdifferent arguments to distinguish between addition and removal scenarios.The interaction between the archetypes and the log, involving the writingof a record with specific fields, is illustrated in Figure 5.6.The resource implementation of PersistentLog leverages BadgerDB [51,63] as the storage engine, which is an embedded high-performance key-valuestore. The pre-commit, commit, and abort phases in the resource imple-mentation of the PersistentLog mapping macro closely resemble those ofthe file system resource implementation.38Chapter 6Modeling and Dealing withFailuresA distributed system is one inwhich the failure of a computeryou didn’t even know existed canrender your own computerunusable.Leslie LamportFailure is a critical aspect to consider when designing distributed sys-tems. Failures are prevalent in real-world scenarios, and distributed systemsdeployed in a production environment must be able to tolerate failures.In a production environment, failures can arise due to factors includingsoftware errors, hardware malfunctions, network outages, and power disrup-tions. However, failures do not inherently exist in models and users have tomodel them accurately.PGo-based systems have a dual requirement that they must be able tohandle failure both on the model side and implementation side. Duringmodel checking, the model itself must be capable of tolerating simulatedfailures, while the compiled Go program must be equipped to handle failuresduring execution.391 mapping macro FaultyLink {2 read {3 \* same as the reliable FIFO link4 }5 write {6 either {7 yield Append($variable, $value);8 } or {9 yield $variable; \* silently drop message10 };11 }12 }Figure 6.1: Modeling a faulty network link in MPCal.Fault tolerance is dependent on the system model and failure model.In this chapter, we assume an asynchronous computing model where thereis no bound on message delays. We assume nodes fail with crash failuresemantics [6] and/or network partitions might happen. This model is arealistic assumption about distributed systems running in data centers. Webuild RaftStore using this system model.In the rest this chapter, we will describe how we can simulate failurebehavior in the model and how we can handle them in the model and thecompiled system.6.1 Modeling Failure BehaviorNetwork faults in PGo can be represented using a mapping macro that in-corporates weak guarantees. For instance, the fault model depicted in Fig-ure 6.1 demonstrates a faulty network link. When a message is transmittedthrough this link, it may or may not be delivered. To capture this non-deterministic behavior, we employ the either statement, which allows us toexpress the two or more possible outcomes.The idiom presented in Figure 6.2 offers a mechanism to simulate crashfailures. In order to simulate a crash failure for the AServer archetype, aconcurrent process named ServerCrasher is executed alongside it, and itis responsible for triggering the crash of the server. To prevent a failed401 process ServerCrasher(serverId) {2 serverCrash:3 netEnabled[serverId] := FALSE;4 fdUpdate:5 fd[serverId] := TRUE;6 }78 archetype AServer(ref net[_], ref netEnabled[_]) {9 lbl:10 \* beginning of a critical section that might fail11 \* \lnot is the logical negation operator12 if (\lnot netEnabled[self]) {13 await FALSE;14 };15 }Figure 6.2: Modeling crash failures in MPCal.process from receiving any network messages, we use the toggle netEnabledto disable networking for the server. This ensures that the failed process isisolated from incoming network communication.ServerCrasher turns off the networking of its corresponding server inthe first label, serverCrash. In the AServer archetype, there exists a codesnippet at the beginning of its critical sections that stops the server’s exe-cution if its networking is disabled. This is achieved by blocking the serverforever using await FALSE; statement. The disabled networking serves as areliable indication of a server failure. Moving on to the fdUpdate label ofServerCrasher, it updates the state of its failure detector, which is furtherdiscussed in Section 6.2.We used PlusCal processes for ServerCrasher because we only want themfor model checking, and there is no need to compile them to Go since, duringruntime, failures manifest as a result of the environment. Similarly, weprovide dummy resource implementation for netEnabled such that it doesnot interfere with normal execution of an archetype.411 either {2 network[id] := msg; \* some communication3 } or {4 \* handle failure...5 };Figure 6.3: Each branch will be taken non-deterministically at run-time. This makes the process to execute handle failure branchwithout even knowing that a failure has happened.1 either {2 network[id] := msg; \* some communication3 } or {4 await fd[id]; \* only run if failure detector reports <id> has failed5 \* handle failure...6 };Figure 6.4: Handling failures with a failure detector in MPCalarchetypes.6.2 Handling Failures with Failure DetectorsProducing a model of failure handling from which PGo can generate a rea-sonable implementation can be subtle. For example, an either statementcan be used to explore failures with model checking, but this expresses whatcould happen. Consider Figure 6.3, which over-approximates failure in away that does not work in an implementation. During verification, thiscode means that either line 2 will execute successfully, or a failure will behandled on line 4. This is fine for verification, as it expresses what couldhappen, either due to some transient issue, or due to the failure of a peer.This type of pattern would allow an implementation to spontaneously handlea failure, regardless of whether any failure was detected. Since the PGo run-time schedules attempts at executing branches of an either statement usinga round-robin strategy, this means that, while the system would technicallyimplement the specification, roughly one in two network operations woulddirectly jump to failure recovery without even attempting communication.In the implementation, we want to attempt the network send operation421 mapping macro PerfectFailureDetector {2 read { yield $variable; }3 write { yield $value; }4 }Figure 6.5: Perfect failure detector modeled in MPCal. A perfect fail-ure detector guarantees strong completeness and strong accu-racy.initially and, if a timeout occurs, proceed to execute the failure handlingcode. However, MPCal has no notion of time, and we discuss this more inChapter 7.To handle failures, we use failure detectors to abstract time and eliminateunwanted executions. This approach is depicted in Figure 6.4. By employinga suitable implementation of the fd resource, the failure handling branch willonly be executed when the fd resource indicates that the remote process hasfailed. If fd[id] returns FALSE, the execution will be rolled back, allowingthe other branch to be attempted. This design enables having practicalfailure checks during runtime and parameterizes verification with differentfailure detectors.Failure detectors are characterized by two properties, completeness andaccuracy [9]. Strong completeness states that eventually every node thatcrashes is permanently suspected by every correct node. Strong accuracystates that no process is suspected before it crashes. A perfect failure de-tector is a failure detector that is both strongly complete and accurate.Figure 6.5 depicts a mapping macro in MPCal that represents a perfect fail-ure detector. The resource fd is associated with this failure detector andits values are updated by the ServerCrasher, as illustrated in Figure 6.2.When a server fails, its networking is first disabled, and eventually its fail-ure is detected by the failure detector. A failure detector eventually detectsnode failures by updating the fd resource in a separate label following theserverCrash label within the ServerCrasher process.In an asynchronous environment in practice, we do not have any accuracyguarantee for failure detectors. Chandra and Toueg [9] showed that it is431 mapping macro PracticalFailureDetector {2 read {3 if ($variable = FALSE) { \* process is alive4 \* no accuracy guarantee5 either { yield TRUE; } or { yield FALSE; };6 } else {7 yield $variable; \* strong completeness8 };9 }1011 write { yield $value; }12 }Figure 6.6: Practical failure detector modeled in MPCal. Practicalfailure detector guarantees strong completeness.possible to solve consensus in an asynchronous environment using a perfectfailure detector. From the FLP result [19], we know solving consensus inan asynchronous network environment is impossible. Thus, having a perfectfailure detector in an asynchronous network environment is impossible too.We can have a failure detector in practice that guarantees strong com-pleteness. This failure detector eventually detects crashed nodes as failed,but alive nodes might get detected as failed due to the lack of accuracy.Figure 6.6 captures this failure detector in MPCal, named practical failuredetector.We used failure detectors in RaftStore to detect failed nodes while send-ing messages to other nodes. We have tried both perfect and practical failuredetectors in RaftStore. Using practical failure detectors gives us strongerguarantees as it is closer to the runtime environment; however, it makes themodel checking process more expensive by adding more non-determinism.A model with a failure detector is still a model, and the essential questionis how close of an approximation one desires to the real runtime environment.Full fidelity is neither feasible nor desirable, considering a model’s purposeis to be an abstract verification tool.446.3 Resource ImplementationFailure detectors resource implementation consist of two abstractions: mon-itor and failure detector resource.A monitor monitors archetypes execution. It provides an API for reg-istering archetypes and it monitors the archetypes by wrapping them. Amonitor provides the IsAlive API, which can be queried to find out whethera specific archetype is alive. At most one monitor should be defined in eachOS process and it catches all archetypes’ goroutines errors and panics. Inthe case of an error or a panic, the monitor responds false to IsAlive re-quests. The Monitor exposes the IsAlive API as a Remote Procedure Call(RPC). In the event of a complete failure of the OS process, subsequent callsto IsAlive times out. This timeout behavior serves as an indication of thefailure of the queried archetype.Failure detector is an archetype resource that provides guarantees of afailure detector in practice, as modeled in Figure 6.6. Each server is assignedan index, such that fd[i] represents the state of the failure detector forserver i. The failure detector periodically initiates the IsAlive RPC to checkthe state of the corresponding servers. On a false response or a timeout ofthe RPC call, the failure detector marks the respective archetype as failed.An example scenario demonstrating the execution of the monitor and failuredetector, where the monitor responds with false, is illustrated in Figure 6.7.Another scenario is depicted in Figure 6.8, where the monitor’s OS processcrashes, resulting in a timeout during the failure detector’s call.45OS Process OS ProcessServer 1 Failure Detector Monitor Server 2IsAlivetrueIsAlivetruefd[2]FALSEfd[2]FALSE IsAlivefalse XServer 2 failsfd[2]TRUEFigure 6.7: Failure detector and monitor execution example, when anarchetype crashes and monitor replies false to the subsequentIsAlive request.OS Process OS ProcessServer 1 Failure Detector Monitor Server 2IsAlivetrueIsAlivetruefd[2]FALSEfd[2]FALSE IsAlive XOS process crashesfd[2]TRUEXTimeoutFigure 6.8: Failure detector and monitor execution example, in a casewhere the the entire OS process crashed and the failure detectordetects that with a timeout.46Chapter 7The Problem with TimeOther times are just specialcases of other universes.David DeutschTiming plays a pivotal role in the design of systems, finding applica-tion in numerous common patterns. Time-based mechanisms are vital foraddressing challenges like timeouts, scheduling periodic activities, cache ex-piration, leases, and leader election. However, a key duality problem arisesconcerning time in the context of models and programs. While programsrequire timing for the aforementioned purposes, MPCal models lack thenotion of time. This raises the fundamental question of how to constructmodels that lack the concept of time, while at the same time enabling theircorresponding programs to use timing effectively.In the context of failure detection, as outlined in Section 6.2, we proposedthe abstraction of failure detectors as a means to abstract time. However,failure detectors are limited to the failure detection problem and we cannotsolve all the problems that need timing with failure detectors. Because manyof the problems that deal with timing, such as scheduling activities, do notnecessarily involve failures.On the implementation side timing problems can be effectively addressedby employing a straightforward timer abstraction. Algorithm 1 presents a47timer implementation that offers a viable solution. In the first line of thealgorithm, a timer object t is created to trigger after the specified timeoutduration. This timer object includes a method called t.Wait(), which sus-pends the execution of the current process until the timer fires. By usingsuch timer objects, we can solve the timing-related problems in programs.The duality problem arises where there is no notion of time in models.Hence, we cannot have such a timer object in MPCal models.Algorithm 1 Simple timer objectt← timer(timeout)t.Wait() . process blocks until t firesWe propose an abstract timer on the model side and a concrete timerresource on the implementation side. We demonstrate that the executionsemantics of the concrete timer resource aligns with the timer on the modelside. We ensure that both sides consistently handle timing-related aspectswhile satisfying their concerns.In an MPCal model, we represent a timer by a boolean value that servesas a resource passed to archetypes. The resource, denoted as t, is true whenthe timer has fired, and false otherwise. To illustrate this, consider thearchetype ANode shown in Figure 7.1, where it is has the timer resource t.The archetype ANode will be blocked until the timer t fires, indicating t istrue.The key question to address is when does t fire and what is its timeoutvalue. On the model side, we assume that regardless of the timeout value,every time the archetype ANode executes, the timer t also fires. Essentially,this treats t as a dummy value on the model side that is always true.The timer resource implementation provides a proper implementation ofa timer object. It takes a timeout value and implements the timer objectdescribed in Algorithm 1 as an archetype resource. The implementation in-cludes an internal timer object, and when this timer has fired, the ReadValuefunction returns true; otherwise, it returns false. In the await statementdemonstrated in Figure 7.1, waiting on the timer implies that the executionof the critical section will be aborted if the timer resource’s value is false.481 \* archetype Node has access to timer t as a resource2 archetype ANode(ref t) {3 lbl:4 await t; \* ANode blocks until t fires5 \* some work6 }Figure 7.1: A timer modeled as a boolean resource in MPCal. Everytime when archetype ANode gets executed, timer t is true, whichmeans it has fired.Consequently, the archetype will execute only when the timer value is true,indicating that its internal timer has fired.On both the implementation side and the model sides, a critical sectionwith a timer gets executed only if its timer is true. Therefore, the timerresource has the same semantics both on the model and implementationside. It is important to note that this is not a formal proof showing thestrict equivalence, and particularly, we did not reason about implementationof the timer resource.In RaftStore, we employ timers in two different places. First, the leaderemploys a timer to schedule the periodic sending of AppendEntries messagesto its followers. This ensures that the followers receive regular updates fromthe leader. Second, each follower maintains a timer that triggers if it doesnot receive an AppendEntries message within a specified timeout period.Once this timeout occurs, the follower transitions into a candidate state andinitiates a new round of leader election.Note that instead of using failure detectors, we could handle failures byimplementing timeouts using timers. However, this approach significantlyincreases the state space on the model side. It also reduces the flexibility offailure detection and leads to exploring the failure handling branch on themodel side regardless of the receiving node’s state. In contrast, using failuredetectors, as discussed in Chapter 6, provides greater flexibility in handlingfailures and improves the efficiency of model checking.49Chapter 8Achieving High ConcurrencyThe wise use of leisure, it mustbe conceded, is a product ofcivilization and education.Bertrand RussellIn this chapter, we explore the process of building concurrent systemsusing PGo. Initially, we examine the duality challenges that arise during thedevelopment of such systems, considering both the model and implementa-tion aspects. Subsequently, we present our experience in building RaftStoreand how we addressed its need for a concurrent server implementation.8.1 Concurrency and DualityEfficiency and performance are essential requirements for a software imple-mentation. High concurrency plays a significant role in attaining betterperformance. By leveraging high concurrency, software systems can effec-tively utilize available resources and maximize throughput. Concurrent exe-cution allows multiple tasks to be executed simultaneously, minimizing idletime and maximizing the utilization of processing capabilities, resulting inimproved throughput and latency in the system.In the context of model-implementation duality in PGo, achieving high50performance, which often involves high concurrency, is primarily an imple-mentation concern. However, when building systems using PGo and compil-ing models into programs, this requirement also influences the model side.As users develop an MPCal model, they must consider how this model com-piles into Go.Introducing a high level of concurrency in an MPCal model can lead toincreased complexity and a larger state space. We can increase the con-currency level in an MPCal model by having more concurrently executingarchetypes or by utilizing finer-grained labels. However, such expansionsresult in a larger state space, which in turn escalates the cost of modelchecking. As a result, a duality trade-off emerges, wherein a more concur-rent model becomes more challenging to reason about while offering thepotential for improved implementation concurrency. Striking a balance be-tween these factors is crucial for users, as they must identify a point wherethe model checking cost remains feasible while achieving a desired level ofimplementation concurrency.When building a highly concurrent system in PGo, users must considerthe compilation semantics that influence the execution behavior. It is pos-sible to have two different models that describe the same system; however,when compiled into a Go program, one may execute concurrently while theother does not. For instance, consider the system depicted in Figure 8.1,which comprises an archetype SingleThread having an either statement thatnon-deterministically executes either TaskA or TaskB. In contrast, Figure 8.2models the same system using two archetypes, ThreadA or ThreadB, each ex-ecuting TaskA and TaskB respectively. Both models, ultimately, compile tothe same TLA+ specification, illustrated in Figure 8.3, capturing the twopossible transitions for the next step, TaskA and TaskB, in the system’s statemachine. The resulting PGo program from Figure 8.1 runs sequentially asa single archetype, while the program generated from Figure 8.2 comprisestwo archetypes capable of concurrent execution.It is important to mention that high concurrency does not necessarilyresult in a high performance. In a highly concurrent program, problems suchas resource contention and process coordination can be expensive. Some of511 archetype SingleThread() {2 lbl:3 while (TRUE) {4 either {5 \* TaskA6 } or {7 \* TaskB8 };9 };10 }Figure 8.1: Archetype SingleThread models a system which eitherdoes TaskA or TaskB at each step. PGo compiles this archetypeinto a sequential program.1 archetype ThreadA() {2 lbl:3 while (TRUE) {4 \* TaskA5 };6 }78 archetype ThreadB() {9 lbl:10 while (TRUE) {11 \* TaskB12 };13 }Figure 8.2: Archetypes ThreadA and ThreadB model a system whereeither does TaskA or TaskB at each step. PGo compiles thisarchetype into a concurrent program, where two archetypes runconcurrently.Next , TaskA ∨ TaskBFigure 8.3: TLA+ compilation of Figure 8.1 and Figure 8.2.52these problems actually have to be addressed on the model side, however,are not visible during model checking and they become apparent by runningthe compiled program.In an MPCal model, archetypes typically represent individual nodes inthe system, and each archetype runs sequentially. However, high-performancesystems often involve multiple threads executing concurrently. To accom-modate such scenarios in PGo-based systems, we adopted a new designapproach to run multiple archetypes on the same node simultaneously. Al-though this pattern enables enhanced performance, it introduces new chal-lenges, such as the need to share resources between these archetypes andcoordinate their execution.To facilitate communication between archetypes running on the samemachine, we use channels inspired by the Go programming language andcommunicating sequential processes (CSP) [34]. In this design, senders cantransmit messages through a channel, and the receiver will receive the mes-sage. If a channel happens to be empty, the receiver will be blocked untila message becomes available on the channel. This mechanism enables syn-chronization and coordination among concurrent archetypes.Sharing variables among different archetypes works as expected with-out any additional work on the model side. However, on the implementa-tion side, using unprotected local resources when different archetypes accessthem can lead to data inconsistency and race conditions. To address this, weintroduced a shared resource that encapsulates a local resource with a read-/write lock. This approach allows multiple readers to access the resourcesimultaneously, while ensuring that only one writer can modify it at a time.The shared resources use timeout when acquiring the lock to prevent dead-locks. In case of a timeout, the execution of the critical section is abortedand the PGo runtime retries the execution.8.2 How We Made RaftStore Highly ConcurrentIn the initial version of RaftStore, the Raft server was represented by asingle archetype. This resulted in a long either statement in the Raft server53archetype, with various tasks specified in each branch. During execution, thePGo runtime would nondeterministically select a branch to execute. If theexecution failed, the runtime would abort and attempt the critical sectionagain, choosing a different branch. The original model of the Raft serverarchetype is depicted on the left side of Figure 8.4.After compiling the initial RaftStore version to Go, we noticed someproblems. Specifically, we realized that leader election is not working due tothe sequential execution of the Raft server. According to the Raft consensusalgorithm, when a node becomes the leader, it should promptly notify theother nodes by sending them AppendEntries messages. However, the sequen-tial execution caused a delay in sending these messages, leading to timeoutsin other nodes, which triggered new election rounds repeatedly.To address this problem, we separated the AppendEntries branch fromthe main Raft server archetype and created a new archetype dedicated solelyto sending AppendEntries messages, if the current server is the leader. Withthis change, the AppendEntries logic can now execute concurrently with therest of the Raft server, allowing for faster and more efficient communicationbetween the nodes during leader election. This change made the leaderelection work in RaftStore.To further improve RaftStore performance, we deleted the entire eitherstatement from the server archetype and created separate archetypes foreach branch. This architectural transformation allowed us to execute eachtask concurrently, resulting in a significant performance boost. The revisedRaftStore server architecture is depicted on the right side of Figure 8.4.Each of these archetypes now corresponds to a specific task, allowing themto execute concurrently. Additionally, we introduced shared variables andchannels for synchronization and data sharing among the archetypes.Throughout the development of the RaftStore model, we adopted a de-liberate strategy to minimize the number of labels in each archetype. Thisapproach was crucial in ensuring that the model checking cost remains fea-sible and manageable. Additionally, we made the assumption that all serverarchetypes fate-share, thereby eliminating the possibility of partial failureamong them.54archetype AServer() {serverLoop: while (TRUE) { either { \* HandleMsg } or { \* AppendEntries } or { \* RequestVote } or { \* AdvanceCommitIndex } or { \* BecomeLeader }; };}AServerAppendEntriesAServerHandlerAServerAdvanceCommitIndexAServerRequestVoteAServerBecomeLeaderShared Variables: - state- commitlndex- currentTerm- votedForappendEntriesChChannelbecomeLeaderChChannelArchetype resourceMapping MacroLegend:Old RaftStore Model New RaftStore ModelFigure 8.4: Architecture of RaftStore. The left side shows the initialversion, which had one archetype. The right side shows the newarchitecture that enables concurrency. Arrows demonstrate howwe create a distinct archetype from each branch of the eitherstatement in the initial version.One of the major challenges we encountered while transforming Raft-Store into a concurrent system was the management of complexity. In addi-tion to carefully designing the model to ensure that the model checking costremains feasible, we had to address the issue of managing shared variablesamong the five server archetypes in RaftStore. To tackle this, we definedall the shared variables as resources and passed them to each archetype.However, this approach resulted in a significant amount of error-prone boil-erplate code, both in the model and the implementation, to initialize thesystem. With more appropriate language features in MPCal, we could havemitigated these complexities and provided a more seamless developer ex-perience. We consider these potential improvements as a topic for futurework.55Chapter 9Modular DesignMake each program do one thingwell.Douglas McIlroySo far, we have been talking about systems that consist of a single model.This chapter explores a design approach where a system comprises severalmodels. We call this a modular design.Building systems modularly is an essential step in building large-scalesystems. Modularity allows us to manage the complexity in large systems.This design approach makes models smaller and easier to reason about.It also reduces the state space of each component model, which makes itpossible to scale MPCal models beyond the conventionally viable limits ofmodel-checked systems.The fundamental principle behind modular design is to divide the sys-tem into smaller, more manageable components. Let us consider a modularsystem denoted as S, having n components, namely c1, . . . , cn. Each compo-nent, such as ci, interacts with a specific set of other components denoted asMi. The model of component ci abstractly defines its interactions with eachcomponent cj ∈ Mi and establishes the communication protocol betweenci and cj . Moreover, component cj adheres to the communication contractspecified by ci and defines compatible communication channels in its own56specification to ensure correct interaction.We model check each component ci individually. This technique signifi-cantly reduces the model checking cost. Let ci be a component with at mostai enabled actions in each step, and we run the model checker for traces upto depth d. If we consider a monolithic system L consisting of c1, . . . , cn,the size of state space that the model checker needs to explore is(n∑i=1ai)d.While the size of state space that model checker explores for a modularsystem S consisting of c1, . . . , cn isn∑i=1aid.It is trivial to see that size of state space in system S is smaller than L’sstate space, knowing ai and d values are positive.We compile each module to Go and connect them on the implementationside with respect to the communication contract that is defined in eachcomponent’s model.Modularity in PGo-based systems offers the advantage of reducing thetrusted computing base (TCB). We provide hand-written resource imple-mentations in Go, which allows for maximum flexibility and the oppor-tunity to perform various performance optimizations. However, such re-source implementations contribute to the system’s TCB. To mitigate thisrisk and minimize the TCB, it is essential to allow verification of resourceimplementations, particularly since these resources may encapsulate com-plex distributed protocols (e.g., distributed mailboxes). Users can definecomponents and necessary communication channels in a way that one com-ponent uses the other component as a resource, and this way they can havea verified resource implementation.At this time, it is not feasible to integrate different MPCal specificationsin a way that ensures soundness during verification. The verification pro-57cess is limited to one specification at a time. Nevertheless, it is still possibleto manually link MPCal specifications and align the semantics of differ-ent components through manual correspondence. When combining differentspecifications, users must ensure that the contracts between the componentsremain valid after compilation. We recognize this as a challenge that couldbenefit from further tooling automation, and we leave it as a topic for futureinvestigation and improvement.To demonstrate the modular design in PGo, we developed a modularversion of RaftStore, called RaftStoreMod, which consists of two distinctcomponents. The high level architecture of RaftStoreMod is shown in Fig-ures 9.1 and 9.2. The first component is the Raft protocol, named RaftProto,represents the core Raft protocol without client interaction semantics. Thesecond component is the key-value store system, called DistKV, which oper-ates as a distributed key-value store, handling client requests and interactingwith an abstract state machine replication component.RaftProto and DistKV interact using two channels: accept and pro-pose. Each RaftProto server has a pair of accept and propose channels.A RaftProto server accepts new requests through its propose channel andbroadcasts committed entries through its accept channel.DistKV is composed of multiple servers, each responsible for maintain-ing a local key-value database. These servers interact with an abstract statemachine replication system to keep their local database in sync. Similar toRaftProto, each DistKV server possesses a pair of accept and propose chan-nels. When a client request is received, a DistKV server forwards the requestto the state machine replication component via its propose channel. Oncethe new entry is committed in the state machine replication component, theDistKV servers receive notifications through their accept channels, allowingthem to update their local database and respond to the clients accordingly.By compiling each of these individual models and linking them in Go, weobtain the full implementation of RaftStoreMod.In Chapter 11 we compare the runtime performance of RaftStoreModstore with several others, including RaftStore.58DistKVAcceptChAcceptChProposeChKV Server SMRRaftProtoProposeChFigure 9.1: Architecture of RaftStoreMod components. The left sideshows the high level architecture of DistKV. Each KV serverinteracts with an abstract state machine replication component(SMR). The right side shows the RaftProto component, whereit communicates with its propose and accept channels.AcceptChKV ServerSMRProposeChRaft ProtoDistKVAcc ChKV rverPro eChRaft r toFigure 9.2: RaftStoreMod implementation architecture. On the im-plementation side, we use RaftProto to implement the abstractstate machine replication (SMR) component of DistKV.59Chapter 10Development ProcessSoftware engineering is whathappens to programming whenyou add time and otherprogrammers.Ross CoxIn this chapter, we outline our development process, which draws fromour experience in building systems using PGo. Managing duality is an inte-gral aspect of our development approach, as we strive to optimize for bothmodel and program concerns. Balancing the requirements of the model andthe implementation is a central challenge, and our process aims to find themost effective trade-offs to achieve a well-optimized and reliable system. Weshare instances of our experience using this process while building RaftStore.Our development process of building systems using PGo is an iterativeprocess of (1) model engineering and (2) implementation optimization.Our system development process begins with model engineering. Duringthis stage, our focus is on modeling concerns, disregarding implementationdetails. Our objective is to create an MPCal model of the system andperform model checking to verify its correctness without delving into theintricacies of implementation. To keep the model checking cost manageable,we start by modeling the simplest system, comprising the minimal number60of archetypes and labels. This approach ensures that we establish a solidfoundation by confirming the correctness of a basic system through modelchecking.Once we have our initial model-checked specification, we proceed withcompiling the model into Go and crafting the necessary glue code to createthe first version of the running system. At this stage, we begin to identify therequirements originating from the implementation side, some of which haveimplications on the model side. In cases where the model does not translatecoherently into a program, alternative specifications must be considered.Additionally, due to the unique execution behavior of the implementation,certain adjustments might be required in the model. An example of thisscenario is the RaftStore leader election, which we previously discussed inChapter 8.The subsequent step involves improving the performance of the imple-mentation. During the implementation optimization phase, we identify bot-tlenecks in the implementation and strategize how to address them. Someproblems can be resolved on the implementation side, such as using relaxedresources to get a performance boost. Some other problems require a dif-ferent approach to modeling, for example, building a model that compilesinto a concurrent program. Furthermore, certain bottlenecks may be inher-ent to the model itself, requiring the development of a more efficient model.For instance, in RaftStore, we have implemented Raft optimizations, suchas batching [58], to improve performance. These protocol-level optimiza-tions must be applied directly to the MPCal model to achieve the desiredefficiency.After identifying the implementation requirements, we return to themodel engineering phase, where we incorporate these changes. Neverthe-less, the primary focus remains on addressing the modeling concerns andensuring the system can be model-checked. Once the adjustments are made,we compile the model into Go, and this iterative process continues until weachieve the desired system. Figure 10.1 demonstrates this iterative process.We recommend that new users interested in building systems with PGoor similar frameworks follow this development process, commencing with61Model EngineeringImplementation OptimizationFigure 10.1: Development process of building systems using PGowhere we face model-implementation duality. This is an it-erative process of model engineering and implementation op-timization.the simplest model. As they progress from the model to a functioning im-plementation, they will inevitably encounter duality challenges. Our workaddresses various duality challenges we faced while constructing complexdistributed systems using PGo. We believe that other users will also con-front similar challenges, and we encourage them to refer to this paper forguidance in addressing these issues.62Chapter 11EvaluationThe Eiffel Tower was built in 2years and 2 months; that is, in793 days. When completed in1889, it became the tallestbuilding in the world, a record itheld for more than 40 years.Jill JonnesIn our evaluation, we address three key questions: (1) To what extentwere the requirements of each side (model and program) satisfied in thepresence of duality? Specifically, we assess how effectively we managed tofulfill the requirements of both the model side and the program side. (2)What is the development effort involved in building systems using PGo,considering the challenges posed by duality? (3) What is the performanceoverhead incurred when building modular systems using PGo?11.1 Evaluated Systems and MethodologyTable 11.1 lists the seven systems we have constructed using MPCal. TheMPCal along with the compiled PlusCal, TLA+, and compiled and glue Gocode for these systems are available in our GitHub repository [28]. RaftStoreand RaftStoreMod are consensus-based key-value stores that we discussed63in Chapters 4 and 9. RaftStoreMod is a modular composition of the pureRaft protocol specification (RaftProto) and DistKV as described in Chap-ter 9. PBStore is a primary-backup key-value store where the primary nodesynchronously replicates client requests to backup nodes. PGoCRDT is anadd-wins observed removed set (AWORSet) state-based Conflict-free Repli-cated Data Type (CRDT) [3] that uses vector clocks for merging and conflictresolution. Lock service is the simple lock service system that we discussedin Chapter 2.We conducted a performance evaluation of multiple systems listed inTable 11.1. Our experiments were conducted on Azure, with each systemdeployed across Ubuntu 20.04 Standard B8ms VMs, utilizing default AzureCloud routing. To ensure reliability, we made our best effort to fully re-initialize the server state between measurements, and each benchmarkingscenario was repeated 5 times. Each scenario involved tens of thousandsof operations and ran for an average duration of 10 minutes. To monitornetwork performance, we examined network interface metrics to ensure thatno network connections were saturated. For reporting our results, we calcu-lated the medians of the trials and represented the 10th and 90th percentilesusing whiskers on bar graphs.6465Table 11.1: Systems we developed using PGo. Our evaluation focuses on the bolded systems: (1) Raft-StoreMod, which is a modular composition of RaftProto and DistKV (see Chapter 9), (2) monolithicRaftStore, (3) PBStore, and (4) PGoCRDT.SystemEffort(person days)Properties model checkedChecked# statesCheckingtime (m)ArchetypeCountMPCalSLOCGlue GoSLOCRaftProto 22 Five Raft properties [59] 2.7× 109 312 9 771 676DistKV 3 Client interaction, consistency 2.6× 107 4 3 256 383RaftStoreMod 25 - - - - - 1059RaftStore 25 Client interaction plus Raft 3.1× 109 404 7 758 1099Lock service 2 Mutual exclusion and liveness 4.6× 107 73 2 67 87PBStore 10 Strong consistency 4.5× 107 235 4 420 270PGoCRDT 10 Convergence and termination 5.8× 106 3954 2 160 18511.2 Development EffortAll MPCal specifications were written primarily by me, with some help andcontributions from two other students. Table 11.1 lists their effort in persondays. The most complex systems we have developed are RaftStore andRaftStoreMod. Table 11.1 also lists the number of archetypes and SLOC ineach MPCal spec, and SLOC for the Go code we hand-wrote to bootstrapthe generated Go implementation of each system.Table 11.1 presents a comparison of the efforts required to build dif-ferent systems. RaftStore was developed in less than one person-month,whereas the construction of a similar system in Ivy [21] demanded 3 person-months, Verdi [71] took 12 person-months, and IronFleet [32] required 18person-months. These results are promising; however, it is important toacknowledge that all these figures, including ours, are based on anecdotaland self-reported data. Moreover, the efforts were undertaken by researcherswho may not represent the average software developer. Future studies shouldfocus on user-based evaluations to assess the usability of tools within thisdomain.During the process of constructing these systems, we observed a recur-ring pattern of reusing mapping macros across different systems that shareidentical or similar assumptions regarding failures or the environment. Ad-ditionally, we have created and reused various implementations of commonlyused resources, such as the network and the file system.11.3 Model Checking PerformanceTable 11.1 presents the properties we defined and verified, the number ofstates explored by the TLC model checker, and the time taken for TLCchecking. Our experiments were conducted on a machine equipped with 64CPU cores and 128GB of RAM.TLC is an exhaustive explicit state model checker. It comprehensivelyexplores the entire reachable state space provided to it before terminating.This approach offers more robust guarantees compared to heuristic statespace sampling since it ensures the consideration of all reachable states.66However, due to its bounded nature, TLC requires a finite state space forexploration. As a result, we needed to impose restrictions on each system’sstate space during the verification process.For the model checking of RaftStore and RaftProto, our configurationincluded three servers, a single round of election, and at most two entriescommitted to the log with the possibility of one node failure. For DistKV,the model checking setting comprised five servers and three clients, wherethe servers could process up to three client requests. For the lock service,we used a model checking configuration with eight servers. In the PBStoremodel, the configuration consisted of five servers and four clients. Similarly,for PGoCRDT, the model checking configuration included five servers.A previous study has demonstrated that reproducing all failures in acomplex distributed system can be achieved with a setup comprising atmost three nodes [79]. This highlights the effectiveness of our boundedmodel checking setting in capturing bugs. Furthermore, by utilizing morepowerful machines, we could potentially apply even looser bounds and checkmore states, as shown in Table 11.1.11.4 Performance of Raft-Based KV StoresWe conduct a comparative analysis of our Raft-based KV stores againstseveral verified KV stores: Vard [72], a KV store verified in Verdi [71];IronKV [33], a KV store verified in Dafny; and Ivy-Raft [21], a KV storeverified in Ivy. All the KV stores are Raft-based, except IronKV that im-plements MultiPaxos. These implementations are extracted in OCaml, C#,and C++ accordingly. To interact with the underlying platform, each im-plementation employs custom shim code, communicating via plain TCP orUDP. While IronKV supports SSL, we disable it for consistency with itsoriginal evaluation. RaftStore and Vard incorporate disk-based durability,whereas IronKV and Ivy-Raft do not. To assess the impact of disk-baseddurability, we re-run selected benchmarks with this feature disabled in ourartifact, observing minimal changes in throughput. We also include bench-mark results for etcd v3.5.4 [18] as a baseline, a widely used Raft-based KV67A B C D FYCSB Workload500100015002000Throughput(op/s)12621785180816171441865127713271124644656949996939758207205 29825415723 33 31 34 18RaftStore Ivy-Raft RaftStoreMod IronKV VardFigure 11.1: Throughput of RaftStore and RaftStoreMod as com-pared to various systems for a selection of standard YCSBworkloads.store implemented in Go.We attempted to include Coyote [13] and StateRight [55] in our evalu-ation since they appeared to have Raft and Paxos prototypes, respectively.However, we discovered that these prototypes were not directly comparablewith practical consensus implementations. The Raft prototype in Coyotewas designed solely as a model checking target, as confirmed by the au-thors. Similarly, the authors of StateRight clarified that their Paxos proto-type could only agree on a single value during an execution, necessitating asystem reset process for a second value to be agreed upon.We assess the performance of these KV stores using the Yahoo! CloudServing Benchmark (YCSB) suite [10], where we measure throughput andlatency. Our evaluation comprises five YCSB workloads: (A) 50/50 read-/update Zipfian, (B) 95/5 read/update Zipfian, (C) read-only Zipfian, (D)95/5 read/update latest (where the most recently inserted records are atthe head of the Zipfian distribution), and (F) 50/50 read/read-modify-write(causally linked read/write) Zipfian. We exclude YCSB workload E as oursystems do not support scans.Figure 11.1 illustrates the performance comparison between RaftStoreand RaftStoreMod, as well as other related work KV stores, across vari-ous YCSB workloads. All systems were deployed in 3-node clusters. To68102 103 104Throughput (op/s)0100200OperationLatency(ms)RaftStore RaftStoreMod Ivy-Raft IronKV etcdFigure 11.2: Latency-throughput data of Raft-based KV systemswith varying number of concurrent clients.3 5 7 9Number of Nodes05001000Throughput(op/s) 1262992843701865 87276368165665659051120764 29 4423 16 13 12RaftStore Ivy-Raft RaftStoreMod IronKV VardFigure 11.3: Scalability of Raft-based KV systems with varying clus-ter size.obtain the peak possible throughput for each system and workload, we con-ducted repeated benchmarks with varying numbers of concurrent clients andrecorded the highest achieved throughput.Among all workloads, RaftStore had the highest throughput. It outper-formed Ivy-Raft, the closest performing system, in terms of overall meanthroughput by 41%.This demonstrates the level of flexibility enabled by the model-implementationduality allows us to optimize I/O behavior and achieve an efficient multi-threaded implementation. Our optimization efforts encompass dividing the69MPCal model into multiple communicating processes, each dedicated to aspecific task, thus enabling more concurrent processing compared to existingapproaches. To achieve multi-threading, we had to modify and recompilethe model, which we subsequently model checked to ensure its correctness.Additionally, we fine-tuned timeout values and the delay between log syn-chronization attempts between nodes to maximize runtime performance.These optimizations were performed on the Go side since our model doesnot account for physical time.Furthermore, we note that RaftStoreMod has a lower performance com-pared to RaftStore, with a slightly lower maximum throughput than Ivy-Raft. This observation indicates that partitioning a system into two separateMPCal models might introduce some performance overhead. However, it isworth considering that the discrepancy in performance could also be at-tributed to our focus on fine-tuning the RaftStore implementation, whichmight have contributed to its superior performance.All systems, including RaftStore, have considerably lower performancecompared to the etcd baseline (not shown), with etcd achieving peak through-put ranging from 5,866 to 10,504 operations per second across all workloads.We attribute RaftStore’s lower throughput to two main factors. First, etcd’sarchitecture allows for significantly higher concurrency in processing clientrequests when compared to RaftStore. This difference arises due to a designdistinction between etcd and the other evaluated Raft-based KV stores.Specifically, etcd implements a threaded extension of Raft [58], enablinggreater concurrency than the core Raft specification. While RaftStore lever-ages more multi-threading than related systems, it remains rooted in theoriginal Raft TLA+ specification, without significant deviations from thecore protocol specification. Second, RaftStore uses inherently less efficientimmutable data structures within its compiled TLA+ representation. Al-though these data structures offer asymptotically good performance, theyare known to carry substantial overheads compared to mutable counter-parts. Addressing these issues and approaching performance levels closer toproduction-grade tools like etcd is left for future research and improvements.We analyze the relationship between latency and throughput for the70benchmarked systems in Figure 11.2. This analysis involves clusters of size3, executing workload A, and presents the median throughput and clientlatency curves for different numbers of clients used in calculating maximumthroughput (as shown in Figure 11.1). For clarity, Vard has been excludedfrom the plot; its maximum throughput was 31 op/s, and its minimum la-tency was 738ms. The comparison shows that, on the whole, RaftStorehas 42% lower median latency than the lowest-latency related system, Ivy-Raft, while achieving latency similar to that of etcd. This improved latencyin RaftStore can be attributed to our optimized multi-threaded implemen-tation, which allow for internal data buffering and concurrent task execu-tion when possible, rather than strictly adhering to the model’s higher-leveltotally-ordered semantics.Figure 11.3 demonstrates the scalability of each system concerning vary-ing cluster sizes while utilizing workload A. Similar to Figure 11.1, we de-termined the number of concurrent clients that resulted in peak throughputfor each system and cluster size. For consensus-based systems, it is ex-pected that peak throughput will decrease as the cluster size increases dueto the increased coordination work required. This effect is clearly shown inFigure 11.3.Figure 11.4 depicts the fault tolerance capabilities of RaftStore duringthe execution of YCSB workload A with a cluster size of 5, displaying thethroughput over time. The plot reveals a leader failure at approximately22 seconds. Subsequently, after a timeout, the clients initiate the process offinding a new leader. Later, at around 41 seconds, we deliberately terminatea follower, which has minimal impact as the client communication with theleader remains unaltered.11.5 Performance of Primary-Backup KV StoresPBStore is a distributed key-value store that operates based on the primary-backup protocol. The PBStore architecture consists of a primary node re-sponsible for synchronously replicating data to one or more backup nodes.We compared PBStore’s performance with Redis, a widely-used key-value710 10 20 30 40Time (s)0200400600Throughput(op/s)Read OpsUpdate OpsLeader fails Follower failsNewleader electedFigure 11.4: Throughput of RaftStore over time with three high-lighted events: leader failure, new leader election, follower fail-ure.store written in C. We configured Redis’s replication to utilize the primary-backup protocol in synchronous replication mode to closely match PBStore’sbehavior. Also, we attempted to evaluate Verdi’s primary-backup system,but we could not proceed as we confirmed with the authors that they hadnot implemented the necessary runtime glue code for evaluation purposes,as it was solely used for verification purposes.To perform the evaluation, we deployed both PBStore and Redis on threemachines, with one serving as the primary and the other two as backups. Weused the YCSB workload A to evaluate the systems’ performance. The peakthroughput of PBStore was found to be 340 op/s, while Redis demonstratedan impressive throughput of over 50,000 op/s.The performance disparity between PBStore and Redis is attributed to alack of protocol optimizations and tuning in PBStore. Specifically, PBStorelacks support for batching incoming requests for replication and sendingreplication requests to backups in parallel, which requires a more complexset of correctness properties and implementation semantics that we did nothave sufficient time to implement and optimize.724 8 12Number of Nodes0204060TimetoConverge(ms) 60 6068293662PGoCRDT RoshiFigure 11.5: Convergence times for PGoCRDT and Roshi.11.6 Performance of CRDT-based SystemsIn scenarios where strict consistency is not required for shared state, com-mutative replicated data types (CRDTs) offer a reliable and efficient ap-proach to represent such data. We evaluated our state-based CRDT set,PGoCRDT, and an open-source CRDT set developed by SoundCloud, calledRoshi [5].To compare these systems, we assessed the time it took for all nodes’states to converge to a consistent value, which we refer to as convergencetime. During the experiment, each node participated in multiple rounds. Inround r, a node n added the pair 〈r, n〉 to its set and then waited until itsset contained all pairs of the form 〈r, i〉, for every node i. For each round,we recorded the duration from when a node updated its local set until thespecified condition was met. We repeated this process for a total of 100rounds. It is important to note that both systems apply updates locally,and each node broadcasts its state every 50ms.Figure 11.5 illustrates that Roshi outperforms PGoCRDT by up to 2×in terms of performance, but PGoCRDT scales more consistently. Althoughthe performance gap is smaller compared to that between RaftStore andetcd, it is likely attributed to Roshi benefiting from more person-hours ded-icated to tuning and optimization, as well as potential inefficiencies in thedata structures utilized by PGo’s compiled output.73Chapter 12Related Work12.1 Model-Checked DSLsP [12, 14] presents a verifiable state machine model that shares similaritieswith MPCal, although it employs a lower-level language similar to C aug-mented with actor-like features. Mace [37, 38] introduces a model based onnested state machines, working as a DSL integrated with C++. Mace lackssome of the abstraction capabilities found in MPCal. StateRight [55] is aDSL designed for model checking, built in Rust. It represents distributedsystems as state machines, resembling the approach taken by Mace. Sta-teRight provides exhaustive model checking capabilities and leverages Rust’srobust low-level safety assurances. Coyote [13], serves as an implementationmodel checker for unaltered C# code, optionally incorporating an actor-based DSL. ModP [15] is a programming system that enables compositionalreasoning (assume-guarantee) of distributed systems. ModP does not havea model checker and employs systematic testing with weaker verificationguarantees.The duality problem also arises in this category of work. We believeMPCal provides more flexibility to developers, such that they can changethe model to optimize the implementation while avoiding the state spaceexplosion problem. Our evaluation shows we could build more performantsystems while exploring a larger state space during model checking.7412.2 Automated Theorem-ProvingTechniques based on automated theorem proving provide a logical frame-work in which a system can be formally specified, formal proofs can bewritten about its properties, and an implementation can be automaticallygenerated. Explicit proofs avoid the state space explosion inherent to modelchecking, and can provide strong guarantees about a given specification.These proofs can, however, be prohibitively difficult to write, requiring manyperson-years and measuring up to ten times the size of the system’s specifi-cation [39]. Many efforts in this space aim to minimise proof effort for users,often by automating or generalising certain proof patterns into DSLs.Verdi [71] and Adore [35] present Coq [69] libraries and support im-plementation extraction. Verdi primarily emphasizes relaxing assumptionsthrough refinement, while Adore reduces proof effort through protocol ab-straction. EventML[62] is designed for Nuprl rather than Coq and em-ploys a logic based on causal ordering of events. PSync [17] facilitates semi-automated verification and operates under the assumption of a round-basedprogram structure. Disel [65] presents a Coq DSL designed for creating andvalidating imperative specifications, utilizing a Hoare-style logic that offersstraightforward composition of verified elements. Chapar [48], another CoqDSL, is specialized in specifying and verifying key-value stores and theircorresponding clients. IronFleet [32] supplies tools that enable developersto demonstrate that practical implementations refine a high-level specifica-tion created in Dafny [47]. Ivy [60], DuoAI [77], DistAI [76], SWISS [30],and I4 [53] reduce the complexity associated with formulating inductiveinvariants for verification. It is important to note that Ivy serves as theverifier, while Ivy-Raft, a KV store [21], is a separate work by differentauthors. Sift [54] presents a methodology centered around proof decomposi-tion, utilizing automated refinement. Armada [16] introduces a specificationlanguage similar to C for verified concurrent programs.Building systems using automated theorem provers requires a significanteffort for writing proofs [74], while implementation concerns tend to be asecondary concern. Reflecting implementation requirements on the system’s75specification can be particularly difficult, as these adjustments can lead toextensive modifications in the proofs.12.3 Model Checking ImplementationsPrior research has extended the concept of exploring state spaces to actualsystem implementations [27, 46, 52, 56, 66, 75]. This pragmatic approachsuccessfully addresses challenging specification problems [20]. However, thisapproach to model checking has inherent scalability limitations due to theheightened concurrency and larger state space inherent in system implemen-tations compared to system models. The duality problem does not arise inthese works since they do not have a model, and as a result, state spaceexplosion becomes an essential problem.12.4 Go Systems ToolingRecent research has introduced tools for detecting and addressing concur-rency problems in Go [49, 50], as well as verifying the correctness of Gocode [7, 8, 73]. This body of work aligns with our framework, as it of-fers a complementary approach to enhance users’ confidence in the Go codegenerated by PGo.76Chapter 13ConclusionIn this work, we introduced the model-implementation duality and providedsolutions to reconcile the modeling land and implementation land. Dualityarises in different aspects and imposes trade-offs while building systems usingPGo. We proposed a framework for building modular systems to managethe complexity and size of the trusted computing base. Our evaluationshows that in the presence of duality, we satisfied the requirements of bothsides of the duality. We built several distributed systems and model-checkedthem with at least three nodes. Our systems perform at least 40% betterthan verified systems from related work and take at least 3× less time toconstruct.Our experience with duality can offer valuable insights for shaping fu-ture efforts in building better frameworks for verified systems. Users canrefer to our shared experience in this to address duality-related challenges.We believe that by addressing the duality challenge effectively, we can gotowards having practical and verified distributed system implementations.77Bibliography[1] M. Abadi and L. Lamport. Conjoining specifications. ACM Trans.Program. Lang. Syst., 17(3):507–535, may 1995. ISSN 0164-0925.doi:10.1145/203095.201069. URL https://doi.org/10.1145/203095.201069.→ page 3[2] B. Alpern and F. B. Schneider. Recognizing safety and liveness.Distributed Computing, 2(3):117–126, Sep 1987. ISSN 1432-0452. →page 6[3] A. Bieniusa, M. Zawirski, N. Preguic¸a, M. Shapiro, C. Baquero,V. Balegas, and S. Duarte. An optimized conflict-free replicated set.arXiv preprint arXiv:1210.3368, 2012. → page 64[4] G. Booch, J. Rumbaugh, and I. Jacobson. Unified Modeling LanguageUser Guide, The (2nd Edition) (Addison-Wesley Object TechnologySeries). Addison-Wesley Professional, 2005. ISBN 0321267974. →page 18[5] P. Bourgon. Roshi: A CRDT system for timestamped events, May2014. https://developers.soundcloud.com/blog/roshi-a-crdt-system-for-timestamped-events. → page 73[6] C. Cachin, R. Guerraoui, and L. Rodrigues. Introduction to reliableand secure distributed programming. Springer Science & BusinessMedia, 2011. → pages 31, 40[7] T. Chajed, J. Tassarotti, F. M. Kaashoek, and N. Zeldovich. Verifyingconcurrent Go code in Coq with Goose. In Proceedings of theInternational Workshop on Coq for Programming Languages (CoqPL),2020. → page 76[8] T. Chajed, J. Tassarotti, M. Theng, M. F. Kaashoek, andN. Zeldovich. Verifying the DaisyNFS concurrent and crash-safe file78system with sequential reasoning. In USENIX Symposium onOperating Systems Design and Implementation (OSDI), 2022. → page76[9] T. D. Chandra and S. Toueg. Unreliable failure detectors for reliabledistributed systems. J. ACM, 43(2):225–267, Mar 1996. ISSN0004-5411. → pages 34, 43[10] B. F. Cooper, A. Silberstein, E. Tam, R. Ramakrishnan, and R. Sears.Benchmarking cloud serving systems with YCSB. In Proceedings ofthe ACM Symposium on Cloud computing (SoCC), 2010. → page 68[11] X. De´fago, A. Schiper, and P. Urba´n. Total order broadcast andmulticast algorithms: Taxonomy and survey. ACM Comput. Surv., 36(4):372–421, dec 2004. ISSN 0360-0300. doi:10.1145/1041680.1041682.URL https://doi.org/10.1145/1041680.1041682. → page 34[12] P. Deligiannis, A. F. Donaldson, J. Ketema, A. Lal, and P. Thomson.Asynchronous Programming, Analysis and Testing with StateMachines. In Proceedings of the ACM SIGPLAN Conference onProgramming Language Design and Implementation (PLDI), 2015. →page 74[13] P. Deligiannis, N. Ganapathy, A. Lal, and S. Qadeer. BuildingReliable Cloud Services Using Coyote Actors. In Proceedings of theACM Symposium on Cloud computing (SoCC), 2021. → pages 68, 74[14] A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, andD. Zufferey. P: Safe Asynchronous Event-driven Programming. InProceedings of the ACM SIGPLAN Conference on ProgrammingLanguage Design and Implementation (PLDI), 2013. → page 74[15] A. Desai, A. Phanishayee, S. Qadeer, and S. A. Seshia. Compositionalprogramming and testing of dynamic distributed systems. Proc. ACMProgram. Lang., 2(OOPSLA), oct 2018. doi:10.1145/3276529. URLhttps://doi.org/10.1145/3276529. → pages 3, 74[16] A. F. Donaldson, E. Torlak, J. R. Lorch, Y. Chen, M. Kapritsos,B. Parno, S. Qadeer, U. Sharma, J. R. Wilcox, and X. Zhao. Armada:low-effort verification of high-performance concurrent programs. InProceedings of the ACM SIGPLAN Conference on ProgrammingLanguage Design and Implementation (PLDI), 2020. → page 7579[17] C. Dra˘goi, T. A. Henzinger, and D. Zufferey. PSync: A PartiallySynchronous Language for Fault-Tolerant Distributed Algorithms. InProceedings of the ACM on Programming Languages (POPL), 2016.→ page 75[18] etcd. etcd, 2021. https://etcd.io/. → page 67[19] M. J. Fischer, N. A. Lynch, and M. S. Paterson. Impossibility ofdistributed consensus with one faulty process. J. ACM, 32(2):374–382, apr 1985. ISSN 0004-5411. doi:10.1145/3149.214121. URLhttps://doi.org/10.1145/3149.214121. → pages 28, 44[20] P. Fonseca, K. Zhang, X. Wang, and A. Krishnamurthy. An EmpiricalStudy on the Correctness of Formally Verified Distributed Systems. InProceedings of the European Conference on Computer Systems(EuroSys), 2017. → page 76[21] J. S. Foster, D. Grossman, M. Taube, G. Losa, K. L. McMillan,O. Padon, M. Sagiv, S. Shoham, J. R. Wilcox, and D. Woos.Modularity for decidability of deductive verification with applicationsto distributed systems. In Proceedings of the ACM SIGPLANConference on Programming Language Design and Implementation(PLDI), 2018. → pages 66, 67, 75[22] S. Friedenthal, A. Moore, and R. Steiner. A Practical Guide toSysML: Systems Modeling Language. Morgan Kaufmann PublishersInc., San Francisco, CA, USA, 2008. ISBN 9780080558363. → page 20[23] GitHub. October 21 post-incident analysis, 2018.https://github.blog/2018-10-30-oct21-post-incident-analysis. → page 1[24] GitLab. Postmortem of database outage of January 31, 2017.https://about.gitlab.com/2017/02/10/postmortem-of-database-outage-of-january-31/. → page 1[25] Google. global: Elevated HTTP 500s errors for a small number ofcustomers with load balancers on Traffic Director-managed backends,2022. https://status.cloud.google.com/incidents/LuGcJVjNTeC5Sb9pSJ9o.→ page 1[26] J. Gray and A. Reuter. Transaction Processing: Concepts andTechniques. Morgan Kaufmann Publishers Inc., San Francisco, CA,USA, 1st edition, 1992. ISBN 1558601902. → page 3480[27] H. Guo, M. Wu, L. Zhou, G. Hu, J. Yang, and L. Zhang. PracticalSoftware Model Checking via Dynamic Interface Reduction. InProceedings of the ACM Symposium on Operating Systems Principles(SOSP), 2011. → page 76[28] F. Hackett, S. Hosseini, R. Costa, M. Do, and I. Beschastnikh. PGo,2022. https://github.com/DistCompiler/pgo. → page 63[29] F. Hackett, S. Hosseini, R. Costa, M. Do, and I. Beschastnikh.Compiling Distributed System Models with PGo. In Proceedings ofthe 28th ACM International Conference on Architectural Support forProgramming Languages and Operating Systems, Volume 2, ASPLOS2023, page 159–175, New York, NY, USA, 2023. Association forComputing Machinery. ISBN 9781450399166.doi:10.1145/3575693.3575695. URLhttps://doi.org/10.1145/3575693.3575695. → pages v, 2[30] T. Hance, M. Heule, R. Martins, and B. Parno. Finding Invariants ofDistributed Systems: It’s a Small (Enough) World After All. InProceedings of the USENIX Conference on Networked Systems Designand Implementation (NSDI), 2021. → page 75[31] HashiCorp. Consul, 2023. https://www.consul.io/. → page 1[32] C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L.Roberts, S. Setty, and B. Zill. IronFleet: Proving Safety and Livenessof Practical Distributed Systems. Commun. ACM, 60(7):83–92, 2017.ISSN 0001-0782. → pages 66, 75[33] C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L.Roberts, S. Setty, and B. Zill. IronClad commit at which IronKVimplementation was evaluated, 2022. https://github.com/microsoft/Ironclad/tree/bcb296737df6541c9542ad4e35499b347992f238. → page 67[34] C. A. R. Hoare. Communicating sequential processes. Commun.ACM, 21(8):666–677, aug 1978. ISSN 0001-0782.doi:10.1145/359576.359585. URL https://doi.org/10.1145/359576.359585.→ page 53[35] W. Honore´, J.-Y. Shin, J. Kim, and Z. Shao. Adore: AtomicDistributed Objects with Certified Reconfiguration. In Proceedings ofthe ACM SIGPLAN Conference on Programming Language Designand Implementation (PLDI), 2022. → page 7581[36] D. Jackson. Software Abstractions: logic, language, and analysis. MITpress, 2012. → page 20[37] C. Killian, J. W. Anderson, R. Braud, R. Jhala, and A. Vahdat.Mace: Language Support for Building Distributed Systems. InProceedings of the ACM SIGPLAN Conference on ProgrammingLanguage Design and Implementation (PLDI), 2007. → page 74[38] C. Killian, J. W. Anderson, R. Jhala, and A. Vahdat. Life, Death,and the Critical Transition: Finding Liveness Bugs in Systems Code.In Proceedings of the USENIX Conference on Networked SystemsDesign and Implementation (NSDI), 2007. → page 74[39] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin,D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell,H. Tuch, and S. Winwood. seL4: Formal Verification of an OS Kernel.In Proceedings of the ACM Symposium on Operating SystemsPrinciples (SOSP), 2009. → page 75[40] L. Lamport. Proving the correctness of multiprocess programs. IEEETrans. Softw. Eng., 3(2):125–143, Mar 1977. ISSN 0098-5589. → page6[41] L. Lamport. Time, clocks, and the ordering of events in a distributedsystem. Commun. ACM, 21(7):558–565, jul 1978. ISSN 0001-0782.doi:10.1145/359545.359563. URL https://doi.org/10.1145/359545.359563.→ page 24[42] L. Lamport. The temporal logic of actions. ACM Trans. Program.Lang. Syst., 16(3):872–923, May 1994. ISSN 0164-0925. → page 19[43] L. Lamport. Specifying Systems: The TLA+ Language and Tools forHardware and Software Engineers. Addison-Wesley LongmanPublishing Co., Inc., Boston, MA, USA, 2002. ISBN 032114306X. →pages 2, 7[44] L. Lamport. The pluscal algorithm language. Theoretical Aspects ofComputing-ICTAC 2009, Martin Leucker and Carroll Morgan editors.Lecture Notes in Computer Science, number 5684, 36-60., Jan 2009.URL https://www.microsoft.com/en-us/research/publication/pluscal-algorithm-language/. → pages 2, 8[45] L. Lamport. A PlusCal’s User Manual. Online material, Aug 2018. →page 1982[46] T. Leesatapornwongsa, M. Hao, P. Joshi, J. F. Lukman, and H. S.Gunawi. SAMC: Semantic-aware Model Checking for Fast Discoveryof Deep Bugs in Cloud Systems. In USENIX Symposium on OperatingSystems Design and Implementation (OSDI), 2014. → page 76[47] R. Leino. Dafny: An automatic program verifier for functionalcorrectness. In E. M. Clarke and A. Voronkov, editors, Logic forProgramming, Artificial Intelligence, and Reasoning, pages 348–370,Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. ISBN978-3-642-17511-4. → page 75[48] M. Lesani, C. J. Bell, and A. Chlipala. Chapar: certified causallyconsistent distributed key-value stores. ACM SIGPLAN Notices, 51(1):357–370, 2016. ISSN 0362-1340. → page 75[49] Z. Liu, S. Zhu, B. Qin, H. Chen, and L. Song. AutomaticallyDetecting and Fixing Concurrency Bugs in Go Software Systems. InProceedings of the 26th ACM International Conference onArchitectural Support for Programming Languages and OperatingSystems (ASPLOS), 2021. → page 76[50] Z. Liu, S. Xia, Y. Liang, L. Song, and H. Hu. Who Goes First?Detecting Go Concurrency Bugs via Message Reordering. InProceedings of the 27th ACM International Conference onArchitectural Support for Programming Languages and OperatingSystems (ASPLOS), 2022. → page 76[51] L. Lu, T. S. Pillai, H. Gopalakrishnan, A. C. Arpaci-Dusseau, andR. H. Arpaci-Dusseau. WiscKey: Separating Keys from Values inSSD-Conscious Storage. ACM Transactions on Storage (TOS), 13(1):1–28, 2017. → page 38[52] J. F. Lukman, H. Ke, C. A. Stuardo, R. O. Suminto, D. H.Kurniawan, D. Simon, S. Priambada, C. Tian, F. Ye,T. Leesatapornwongsa, A. Gupta, S. Lu, and H. S. Gunawi. FlyMC:Highly Scalable Testing of Complex Interleavings in DistributedSystems. In Proceedings of the European Conference on ComputerSystems (EuroSys), 2019. → page 76[53] H. Ma, A. Goel, J.-B. Jeannin, M. Kapritsos, B. Kasikci, and K. A.Sakallah. I4: Incremental Inference of Inductive Invariants forVerification of Distributed Protocols. In Proceedings of the ACM83Symposium on Operating Systems Principles (SOSP), 2019. → page75[54] H. Ma, H. Ahmad, A. Goel, E. Goldweber, J.-B. Jeannin,M. Kapritsos, and B. Kasikci. Sift: Using Refinement-guidedAutomation to Verify Complex Distributed Systems. In USENIXAnnual Technical Conference (ATC), 2022. → page 75[55] J. Nadal. Building Distributed Systems With Stateright.https://www.stateright.rs/. Accessed: 2022-10-27. → pages 68, 74[56] L. Nelson, J. Bornholt, R. Gu, A. Baumann, E. Torlak, and X. Wang.Scaling symbolic evaluation for automated verification of systems codewith Serval. In Proceedings of the ACM Symposium on OperatingSystems Principles (SOSP), 2019. → page 76[57] C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, andM. Deardeuff. How Amazon Web Services Uses Formal Methods.Commun. ACM, 58(4):66–73, Mar 2015. → page 1[58] D. Ongaro. Consensus: Bridging theory and practice. StanfordUniversity, 2014. → pages 25, 61, 70[59] D. Ongaro and J. Ousterhout. In Search of an UnderstandableConsensus Algorithm. In USENIX Annual Technical Conference(ATC), 2014. → pages x, 3, 24, 25, 65[60] O. Padon, K. L. McMillan, A. Panda, M. Sagiv, and S. Shoham. Ivy:Safety verification by interactive generalization. In Proceedings of theACM SIGPLAN Conference on Programming Language Design andImplementation (PLDI), 2016. → page 75[61] A. Pnueli. The Temporal Logic of Programs. In Proceedings of theAnnual Symposium on Foundations of Computer Science, 1977. →page 7[62] V. Rahli, D. Guaspari, M. Bickford, and R. L. Constable. FormalSpecification, Verification, and Implementation of Fault-TolerantSystems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci.Technol., 72, 2015. → page 75[63] M. Rai Jain. Introducing Badger: A fast key-value store writtenpurely in go, May 2017. https://dgraph.io/blog/post/badger/. → page 3884[64] Roblox. Roblox Return to Service 10/28-10/31 2021, 2022. https://blog.roblox.com/2022/01/roblox-return-to-service-10-28-10-31-2021/. →page 1[65] I. Sergey, J. R. Wilcox, and Z. Tatlock. Programming and provingwith distributed protocols, 2017. → page 75[66] J. Simsa, R. Bryant, and G. Gibson. dBug: Systematic Evaluation ofDistributed Systems. In Proceedings of the 5th InternationalConference on Systems Software Verification (SSV), 2010. → page 76[67] T. Strickx and J. Hartman. Cloudflare outage on June 21, 2022, 2022.https://blog.cloudflare.com/cloudflare-outage-on-june-21-2022/. → page 1[68] G. D. Team. The Gallina specification language, 2023. https://coq.github.io/doc/v8.9/refman/language/gallina-specification-language.html. →page 20[69] T. C. D. Team. The Coq Proof Assistant, version 8.9.0, 2019. https://web.archive.org/web/20190415015254/https://zenodo.org/record/2554024.→ pages 20, 75[70] M. Wenzel et al. The isabelle/isar reference manual, 2004. → page 20[71] J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D.Ernst, and T. Anderson. Verdi: a framework for implementing andformally verifying distributed systems. ACM SIGPLAN Notices, 50(6):357–368, Jun 2015. ISSN 03621340. → pages 66, 67, 75[72] J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D.Ernst, and T. Anderson. verdi-raft commit at which Vardimplementation was evaluated, 2022. https://github.com/uwplse/verdi-raft/tree/ea99a7453c30a0c11b904b36a3b4862fad28abe1. → page67[73] F. A. Wolf, L. Arquint, M. Clochard, W. Oortwijn, J. a. C. Pereira,and P. Mu¨ller. Gobra: Modular specification and verification of goprograms. In International Conference on Computer AidedVerification (CAV), 2021. → page 76[74] D. Woos, J. R. Wilcox, S. Anton, Z. Tatlock, M. D. Ernst, andT. Anderson. Planning for change in a formal verification of the raftconsensus protocol. In Proceedings of the 5th ACM SIGPLAN85Conference on Certified Programs and Proofs, CPP 2016, page154–165, New York, NY, USA, 2016. Association for ComputingMachinery. ISBN 9781450341271. doi:10.1145/2854065.2854081. URLhttps://doi.org/10.1145/2854065.2854081. → page 75[75] J. Yang, T. Chen, M. Wu, Z. Xu, X. Liu, H. Lin, M. Yang, F. Long,L. Zhang, and L. Zhou. MODIST: Transparent Model Checking ofUnmodified Distributed Systems. In Proceedings of the USENIXConference on Networked Systems Design and Implementation(NSDI), 2009. → page 76[76] J. Yao, R. Tao, R. Gu, J. Nieh, S. Jana, and G. Ryan. DistAI:Data-Driven automated invariant learning for distributed protocols.In USENIX Symposium on Operating Systems Design andImplementation (OSDI), 2021. → page 75[77] J. Yao, R. Tao, R. Gu, and J. Nieh. DuoAI: Fast, AutomatedInference of Inductive Invariants for Verifying Distributed Protocols.In USENIX Symposium on Operating Systems Design andImplementation (OSDI), 2022. → page 75[78] Y. Yu, P. Manolios, and L. Lamport. Model checking tla+specifications. In L. Pierre and T. Kropf, editors, Correct HardwareDesign and Verification Methods, pages 54–66, Berlin, Heidelberg,1999. Springer Berlin Heidelberg. ISBN 978-3-540-48153-9. → page 7[79] D. Yuan, Y. Luo, X. Zhuang, G. R. Rodrigues, X. Zhao, Y. Zhang,P. U. Jain, and M. Stumm. Simple testing can prevent most criticalfailures: An analysis of production failures in distributeddata-intensive systems. In Proceedings of the 11th USENIXConference on Operating Systems Design and Implementation,OSDI’14, page 249–265, USA, 2014. USENIX Association. ISBN9781931971164. → page 6786Appendix ASupporting MaterialsWe include parts of the RaftStore MPCal model here.1 \* A perfect failure detector. Can be replaced with other failure2 \* detectors with different guarantees.3 mapping macro PerfectFailureDetector {4 read {5 yield $variable;6 }78 write {9 yield $value;10 }11 }1213 \* Persistent log mapping macro. It provides efficient add and14 \* remove operations.15 mapping macro PersistentLog {16 read {17 yield $variable;18 }1920 write {21 if ($value.cmd = LogConcat) {22 yield $variable \o $value.entries;23 } else if ($value.cmd = LogPop) {24 yield SubSeq($variable, 1, Len($variable) - $value.cnt);8725 };26 }27 }2829 \* A helper for handling failure when sending a network message.30 macro Send(net, dest, fd, m) {31 either {32 net[dest] := m;33 } or {34 await fd[dest];35 };36 }3738 archetype AServerHandler(...) {39 serverLoop:40 while (TRUE) {41 m := net[srvId];42 handleMsg:43 if (m.mtype = RequestVoteRequest) {44 UpdateTerm(self, m, currentTerm, state, votedFor, leader);4546 \* HandleRequestVoteRequest47 with (48 i = srvId, j = m.msource,49 logOK = \/ m.mlastLogTerm > LastTerm(log[i])50 \/ /\ m.mlastLogTerm = LastTerm(log[i])51 /\ m.mlastLogIndex >= Len(log[i]),52 grant = /\ m.mterm = currentTerm[i]53 /\ logOK54 /\ votedFor[self] \in {Nil, j}55 ) {56 assert m.mterm <= currentTerm[i];57 if (grant) {58 votedFor[i] := j;59 };60 Send(net, j, fd, [61 mtype |-> RequestVoteResponse,62 mterm |-> currentTerm[i],63 mvoteGranted |-> grant,64 msource |-> i,8865 mdest |-> j66 ]);67 };68 } else if (m.mtype = RequestVoteResponse) {69 \* HandleRequestVoteResponse70 } else if (m.mtype = AppendEntriesRequest) {71 \* HandleAppendEntriesRequest72 } else if (m.mtype = AppendEntriesResponse) {73 \* HandleAppendEntriesResponse74 } else if (75 \/ m.mtype = ClientPutRequest76 \/ m.mtype = ClientGetRequest77 ) {78 \* HandleClientRequest79 };80 };81 }8283 archetype AServerAppendEntries(...) {84 serverAppendEntriesLoop:85 while (appendEntriesCh[srvId]) {86 await state[srvId] = Leader;87 idx := 1;88 appendEntriesLoop:89 \* AppendEntries90 while (91 /\ state[srvId] = Leader92 /\ idx <= NumServers93 ) {94 if (idx /= srvId) {95 with (96 prevLogIndex = nextIndex[srvId][idx] - 1,97 prevLogTerm = IF prevLogIndex > 098 THEN log[srvId][prevLogIndex].term99 ELSE 0,100 entries = SubSeq(log[srvId], nextIndex[srvId][idx],101 Len(log[srvId]))102 ) {103 \* Leader server sending new entries to follower servers104 Send(net, idx, fd, [89105 mtype |-> AppendEntriesRequest,106 mterm |-> currentTerm[srvId],107 mprevLogIndex |-> prevLogIndex,108 mprevLogTerm |-> prevLogTerm,109 mentries |-> entries,110 mcommitIndex |-> commitIndex[srvId],111 msource |-> srvId,112 mdest |-> idx113 ]);114 };115 };116 idx := idx + 1;117 };118 };119 }120121 archetype AClient(...) {122 clientLoop:123 while (TRUE) {124 req := reqCh;125 sndReq:126 if (leader = Nil) {127 with (srv \in ServerSet) {128 leader := srv;129 };130 };131 Send(net, leader, fd, [132 mtype |-> ClientPutRequest,133 mcmd |-> [134 idx |-> reqIdx,135 type |-> Put,136 key |-> req.key,137 value |-> req.value138 ],139 msource |-> self,140 mdest |-> leader141 ]);142 rcvResp:143 either {144 resp := net[self];90145 leader := resp.mleaderHint;146 if (\lnot resp.msuccess) {147 goto sndReq;148 } else {149 respCh := resp;150 };151 } or {152 await \/ /\ fd[leader]153 /\ netLen[self] = 0 \* no unread message154 \/ timeout; \* timeout injection155 leader := Nil;156 goto sndReq;157 };158 };159 }91
Thesis/Dissertation
eng
Computer Science
Vancouver : University of British Columbia Library
Attribution-NonCommercial-NoDerivatives 4.0 International
Graduate
Beschastnikh, Ivan
Reconciling the model-implementation duality in PGo
Text
Software