Science, Faculty of
Computer Science, Department of
DSpace
UBCV
Costa, Renato Mascarenhas
Master of Science - MSc
University of British Columbia
Distributed systems are notoriously difficult to get right: the inherently asynchronous nature of their execution gives rise to a fundamentally non-deterministic system. Previous work has shown that the use of formal methods to reason about distributed systems is a promising area of research. In particular, model-checking allows developers to verify system models against a correctness specification by performing an exhaustive search over the system's possible executions. However, the transition from a trusted specification to a valid implementation is a manual, error-prone process that could introduce subtle, hard to find bugs. In this work, we aim to bridge this gap by automatically translating a specification into an implementation that refines it. Specifically, we leverage the clear separation between application-specific logic and abstract components in the Modular PlusCal language to define an interface that concrete implementations must follow in order to implement the abstractions. Our evaluation shows that this approach is able to handle complex specifications and generate systems that preserve the correctness properties verified via model-checking.
Compiling Distributed System Specifications intoImplementationsbyRenato Mascarenhas CostaB. Computer Science, University of SaËo Paulo, 2012A 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)April 2019c© Renato Mascarenhas Costa, 2019The following individuals certify that they have read, and recommend to the Fac-ulty of Graduate and Postdoctoral Studies for acceptance, the thesis entitled:Compiling Distributed System Specifications into Implementationssubmitted by Renato Mascarenhas Costa in partial fulfillment of the requirementsfor the degree of Master of Science in Computer Science.Examining Committee:Ivan Beschastnikh, Computer ScienceSupervisorRonald Garcia, Computer ScienceSupervisory Committee MemberiiAbstractDistributed systems are notoriously difficult to get right: the inherently asynchronousnature of their execution gives rise to a fundamentally non-deterministic system.Previous work has shown that the use of formal methods to reason about distributedsystems is a promising area of research. In particular, model-checking allows de-velopers to verify system models against a correctness specification by performingan exhaustive search over the systemâs possible executions. However, the transi-tion from a trusted specification to a valid implementation is a manual, error-proneprocess that could introduce subtle, hard to find bugs.In this work, we aim to bridge this gap by automatically translating a speci-fication into an implementation that refines it. Specifically, we leverage the clearseparation between application-specific logic and abstract components in the Mod-ular PlusCal language to define an interface that concrete implementations mustfollow in order to implement the abstractions. Our evaluation shows that this ap-proach is able to handle complex specifications and generate systems that preservethe correctness properties verified via model-checking.iiiLay SummaryDistributed systems are at the heart of many online services that people use everyday, such as email, file storage, and messaging. Despite this pervasiveness, dis-tributed systems are complex to build and often fail in unexpected ways. Thesefailures may lead to service outages and even data loss, impacting all users of theservice. There has been increasing interest in the application of formal methodsas an alternative to deal with the complexity of a distributed system. In particular,model checking is a technique that allows system designers to verify the correct-ness of a model by performing exhaustive testing. However, the transition from themodel to a correct implementation is manual and can introduce bugs, even if themodel is believed to be correct. In this work, we propose a technique to bridge thisgap by automatically translating from a trusted model to a correct implementationof a distributed system.ivPrefaceAll the work presented henceforth was conducted in the NSS (Networks, Sys-tems and Security) lab in the Department of Computer Science at the University ofBritish Columbia, Point Grey campus.The work presented in this thesis is original and unpublished work by the au-thor, Renato Mascarenhas Costa. It builds on top of the PGo compiler, a researchproject in which Matthew Do and Finn Hackett are also core contributors. Theentirety of this work was designed and written with the assistance of Dr. IvanBeschastnikh.vTable of ContentsAbstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iiiLay Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ivPreface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vTable of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . viList of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ixList of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xGlossary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiiAcknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiii1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52.1 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . 52.2 TLA+ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.3 PlusCal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92.4 Modular PlusCal . . . . . . . . . . . . . . . . . . . . . . . . . . 102.5 PGo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 Compiling Modular PlusCal Specifications . . . . . . . . . . . . . . 143.1 Modular PlusCal Execution Semantics . . . . . . . . . . . . . . . 14vi3.2 Preserving Execution Semantics . . . . . . . . . . . . . . . . . . 173.2.1 Resources Mapped as Functions . . . . . . . . . . . . . . 193.3 Archetypes as APIs . . . . . . . . . . . . . . . . . . . . . . . . . 213.4 Resources as Interfaces . . . . . . . . . . . . . . . . . . . . . . . 223.4.1 Handling Errors . . . . . . . . . . . . . . . . . . . . . . . 253.5 Long Running Processes . . . . . . . . . . . . . . . . . . . . . . 253.6 Dealing with Failures . . . . . . . . . . . . . . . . . . . . . . . . 273.6.1 Recovering from Errors in the Environment . . . . . . . . 283.6.2 Crash Failures . . . . . . . . . . . . . . . . . . . . . . . 294 Execution Runtime . . . . . . . . . . . . . . . . . . . . . . . . . . . 314.1 Synchronized Start . . . . . . . . . . . . . . . . . . . . . . . . . 314.2 Distributed Global State . . . . . . . . . . . . . . . . . . . . . . 344.2.1 Data Store . . . . . . . . . . . . . . . . . . . . . . . . . . 344.2.2 Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . 364.3 Communication Channels . . . . . . . . . . . . . . . . . . . . . . 424.4 Other Common Resources . . . . . . . . . . . . . . . . . . . . . 445 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 465.1 PGo Compiler . . . . . . . . . . . . . . . . . . . . . . . . . . . . 465.2 Distributed Runtime . . . . . . . . . . . . . . . . . . . . . . . . . 476 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 486.1 Specification Complexity . . . . . . . . . . . . . . . . . . . . . . 486.2 Semantic Equivalence . . . . . . . . . . . . . . . . . . . . . . . . 506.3 Performance Comparison . . . . . . . . . . . . . . . . . . . . . . 516.3.1 Experimental Setup . . . . . . . . . . . . . . . . . . . . . 516.3.2 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . 517 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 548 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 569 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58viiBibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59viiiList of TablesTable 3.1 Possible errors an archetype resource implementation may return. 25Table 5.1 Lines of code (Lines of code (LOC)), excluding comments andblank lines, changed for the components of PGo updated in thiswork. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46Table 6.1 Complexity of the specifications used in the evaluation. Ab-stractions are counted based on the number of implementation-specific concerns that were not included in the model, each ex-pressed as one or multiple mapping macros; #Lines includeslines of Modular PlusCal, excluding comments and blank lines. 49Table 6.2 Generating a running implementation from the models evalu-ated. Generated LOC indicates lines of code produced by PGofrom the archetype definitions; Manual LOC counts lines ofcode manually written to bootstrap the system. Both numbersexclude comments and blank lines. . . . . . . . . . . . . . . . 50Table 6.3 Effort required to implement both models evaluated in this work,in terms of the number of lines of code involved. Numbers ex-clude comments and blank lines. . . . . . . . . . . . . . . . . 51ixList of FiguresFigure 1.1 PGo workflow proposed in this thesis. Programmers specifytheir distributed protocols or applications using the ModularPlusCal language. PGo translates that specification into Plus-Cal, allowing developers to compile it to TLA+ and model-check it against relevant system properties. Once the specifi-cation is believed to correctly describe the system, PGo can au-tomatically generate an implementation that exhibits the samebehavior as the abstractly defined specification. The devel-oper provides concrete implementations for the componentsthat were left abstract in the specification and is able to run thesystem in a distributed environment. . . . . . . . . . . . . . . 4Figure 2.1 Examples of safety and liveness properties in the context ofdistributed job scheduling. In this model, AssignedJobs isa map from job to node identifiers; and JobSet and NodeSetrepresent the set of jobs to be scheduled and nodes in the clus-ter, respectively. . . . . . . . . . . . . . . . . . . . . . . . . . 6Figure 2.2 Definition of the distributed job scheduler example in TLA+.To make the example more interesting, the scheduler here ismodeled to load jobs from some source and schedule themconcurrently (expressed as a disjunction in the definition ofNext). The safety and liveness properties of Figure 2.1 areredefined here using TLA+ syntax. . . . . . . . . . . . . . . . 8xFigure 3.1 Executing an action that uses resources mapped as functions. . 20Figure 4.1 Synchronization protocol provided by the PGo runtime to al-low applications to optionally coordinate their start. . . . . . . 32Figure 4.2 State of the data stores in every node in a system at a certainpoint in time. A value is only associated with a global vari-able if the node owns the data. Ownership information may beoutdated: for instance, P3 believes that history is owned by P1when it is, in fact, owned by P2 at this moment. . . . . . . . . 35Figure 4.3 Borrowing a single variable from another process. . . . . . . . 38Figure 4.4 Requesting multiple references in the same message. In thisexample, P2 no longer owns variable b, and it informs P1 thatthe new owner is believed to be P3. . . . . . . . . . . . . . . . 39Figure 4.5 A complex interaction between processes P1, P2 and P3 whereownership is moved and concurrent access to global variablesneeds to be resolved. Names in curly braces indicate whichvariables are owned by the processes at different times. . . . . 41Figure 4.6 Three processes connected to each other. Each have a localmailbox of fixed capacity; when processes want to communi-cate, they send a message that is appended to the receiverâsmailbox. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42Figure 6.1 Execution time for the load balancer system, with one or mul-tiple clients performing 10 (left) or 100 (right) requests per client. 52Figure 6.2 Time it takes for three clients to perform 100 operations, firstsequentially (left), and then with Go routines (right). . . . . . 52xiGlossaryAPI application programming interfaceAST abstract syntax treeBMC bounded model checkingFIFO first-in, first-outLOC Lines of codeRSM replicated state machineSAT satisfiabilityTLA Temporal Logic of ActionsxiiAcknowledgmentsThis research was funded by a grant from the National Science and EngineeringResearch Council of Canada (NSERC) Discovery Grant.I would like to thank Dr. Ivan Beschastnikh for his supervision and guidanceduring the development of this work. Our weekly meetings were very helpful inthe process of defining the direction of the project.I would also like to thank Matthew Do and Finn Hackett for their contributionsto the project and the many hours we spent together discussing design decisions ona whiteboard.Finally, I would like to thank my family and friends for their support duringmy time at UBC.xiiiChapter 1IntroductionEngineering performant and correct distributed systems is a hard task, despite theirubiquitous presence in systems behind popular software services offered by com-panies like Google, Amazon, Netflix, and many others. One of the main reasonsthat makes writing distributed systems difficult is the inherently concurrent andasynchronous environment in which they are deployed: processes execute on dif-ferent machines and independently from one another, networks connecting theseprocesses may fail, drop, or reorder packets; and, individual nodes may crash atany time. This dynamic setting gives rise to a fundamentally non-deterministicsystem, in which it is not possible to predict the exact sequence of events for agiven input. As a consequence, distributed systems running in production todayoften have critical bugs that lead to degraded performance [11], service outage[3, 15] and even data loss [12].Due to the asynchronous nature of distributed systems, protocol designers facethe challenging task of reasoning about concurrent execution. Even when com-munication protocols are formally specified, they may make certain assumptionsabout the execution environment that do not hold in practical systems. This gapforces engineers to fill in the missing pieces and potentially introduce bugs in theprocess [6]. Practical distributed systems resort to adding error handling code inan ad-hoc manner, making it more difficult to correspond the implementation withthe original protocol description; this has the undesirable consequence of makingprotocol changes a significantly harder and more error-prone process.1These difficulties have motivated the research community to look for and de-vise a number of solutions. In particular, the use of formal verification methodsin the context of distributed systems is an area of active research. For instance,model-checking is a technique that can be used to exhaustively explore a distributedsystemâs model in order to find violations of correctness properties of the system.The main advantage of model checking is its ability to uncover bugs hiding in cor-ner cases of a protocol or implementation, testing scenarios that manually writtentests would generally not exercise [20]. In addition, model checkers are also ableto provide a trace when a property is violated, making it easier for the developer tounderstand how the system reached an invalid state.Many model checking languages and tools exist. TLA+ [26] is a declarativespecification language that allows developers to formalize the behavior of theirsystems as a collection of steps and transitions between them. PlusCal [27] is aspecification language built on top of TLA+ that makes it easier to specify systemsin a procedural style: more specifically, users can specify how different processesin a system interact using familiar control flow constructs such as if statementsand while-loops. Protocol designers using TLA+ or PlusCal can write propertiesabout their system and verify that they hold for every possible execution inter-leaving by using the TLC model checker. This gives them more confidence aboutthe correctness of the protocol. Both TLA+ and PlusCal, however, only describea system abstractly: implementation details are intentionally not included in thespecification.Despite being a useful tool to find subtle bugs in distributed systems, modelchecking suffers from a major drawback: state-space explosion. Complex sys-tems generally have very large state spaces that grow exponentially with respectto certain parameters of the model (for example, the number of replicas in a clus-ter). This is even more pronounced if a concrete implementation, rather than anabstract specification, is being explored since it has more states, many of which areirrelevant to the high level properties of the distributed protocol the developer is in-terested in. By checking only a model, the protocol designer is able to leave certainimplementation details abstract, focusing exploration on protocol-specific behav-ior and reducing the state space. The obvious downside of this approach is that theprocess of writing an implementation of the protocol model that was checked is a2manual, error-prone process and bugs could be introduced during translation.In this work, we aim to bridge the gap between the design and verification ofa distributed protocol specification and the construction of a correct implementa-tion for the model. More specifically, we use a variant of PlusCal called ModularPlusCal (MPCal for short) to mechanize the translation from a verified model toan implementation that exhibits the same behavior. In other words, the imple-mentation is a refinement of the model. This is achieved by exploiting ModularPlusCalâs clear separation between the specification of a systemâs behavior and theimplementation details that are modeled abstractly. By providing developers withconcrete implementations of abstract components typically found in a distributedsystem specification (for instance, network models, file systems, time, etc), we areable to generate implementations of model-checked specifications that have perfor-mance comparable to handwritten systems. Figure 1.1 depicts the different stagesof the process in this workflow.In summary, this thesis makes the following contributions:â¢ The definition of a general application programming interface (API) thatgives users the ability to create their own abstractions in Modular PlusCaland define how they match to concrete implementations.â¢ A compiler from Modular PlusCal specifications to implementations in theGo programming language, and a distributed execution environment thatincludes concrete implementations for common abstractions needed in dis-tributed applications and protocols. This work was developed as part of thePGo [39] compiler1.â¢ An evaluation of distributed systems generated from specifications and howthey compare against handwritten systems in terms of execution time andsource code complexity.1PGo is open source and is available at https://github.com/ubc-nss/pgo.3Figure 1.1: PGo workflow proposed in this thesis. Programmers specify theirdistributed protocols or applications using the Modular PlusCal lan-guage. PGo translates that specification into PlusCal, allowing devel-opers to compile it to TLA+ and model-check it against relevant systemproperties. Once the specification is believed to correctly describe thesystem, PGo can automatically generate an implementation that exhibitsthe same behavior as the abstractly defined specification. The developerprovides concrete implementations for the components that were leftabstract in the specification and is able to run the system in a distributedenvironment.4Chapter 2BackgroundThis work builds on top of multiple languages, tools and concepts previously de-signed and built to solve specific problems. In this chapter, we briefly outline themost important ideas this work is based on. Section 2.1 describes model-checking,a technique used to verify whether a model satisfies a certain correctness specifica-tion; sections 2.2 and 2.3, respectively, present an overview of TLA+ and PlusCal,two specification languages that can be used to model arbitrary systems; section2.4 describes Modular PlusCal, a variant of PlusCal used in this work. Finally, sec-tion 2.5 introduces PGo, a compiler from specifications to implementations. Thework described in this thesis is part of the PGo compiler.2.1 Model CheckingModel checking is a technique to algorithmically determine whether a model of asystem satisfies a certain correctness specification. Models are typically expressedas a transition relation that defines the states that a system can be in, as well as howthe transitions between them may occur. Model checking performs an exhaustivesearch over the state space of a system in order to determine whether the correct-ness specification is satisfied on every possible execution. When an execution isfound to violate a correctness property, model checking has the ability to produce acounterexample, in the form of an execution trace, that informs the system designerhow the system reached an invalid state.5Correctness specifications are written as properties about the system. In orderto prove correctness of the model with respect to these properties, it is commonto divide them into two categories: safety and liveness properties [23]. Informallyspeaking, safety asserts that bad states are not reachable from the initial state; live-ness properties express that the system must eventually do something good. Thiscategorization is useful because different techniques are used to prove each type ofproperty, and previous work has shown that every property can be constructed asa conjunction of safety and liveness properties [2]. Figure 2.1 lists some examplesof safety and liveness properties in the context of distributed systems.A note on wording: it is common to refer to a model and correctness propertiesof a system as its âspecificationâ. Unless otherwise stated, this is the interpretationused in this thesis when referring to a specification of a system.â jâ JobSet : ( j /âDOMAIN(AssignedJobs))â¨(ânâNodeSet : AssignedJobs( j)= n)(a) Safety property: every job is either not scheduled yet, or assigned to a valid node in thecluster. This property must hold for every reachable state in the system.â¦(â j â JobSet : ân â NodeSet : AssignedJobs( j) = n)(b) Liveness property: eventually (â¦), all jobs must be assigned to a valid node in thecluster. Note that satisfying the safety property above does not guarantee this fact, since ascheduler that never schedules any job trivially satisfies the safety requirement.Figure 2.1: Examples of safety and liveness properties in the context of dis-tributed job scheduling. In this model, AssignedJobs is a map fromjob to node identifiers; and JobSet and NodeSet represent the set ofjobs to be scheduled and nodes in the cluster, respectively.The biggest issue with model checking as a correctness verification techniqueis state-space explosion. Complex systems have state space that grows exponen-tially with respect to data-structure sizes and parameters of the model. This isexacerbated when execution is concurrent (such as in distributed systems): modelchecking needs to explore every possible execution interleaving, further increasingthe state space.A complementary approach to traditional model checking is bounded model6checking (BMC) [5]. In this approach, the transition relation is unfolded a fixednumber of times k, conjoined into a single formula and the search for a violatingtrace is given to a satisfiability (SAT) solver. While this approach is useful forfinding shallow bugs, it is generally incomplete.Many techniques exist that aim to alleviate the problem of state-space explo-sion without bounding the search depth. Partial-order reduction [10, 13] groupstransitions into equivalence classes and avoids exploring interleavings that do notmatter to prove correctness. Abstraction can also significantly reduce the statespace by treating certain aspects of a system abstract: instead of exploring all statesassociated with the steps required to perform a certain task, abstraction allows thesystem designer to express the same behavior as an abstract component. TLA+is one example of a specification language that allows systems to be specified atarbitrary levels of abstraction. This work aims to match the use of abstractionsin model checking with concrete implementations that exhibit the same behavior,specifically in the context of distributed systems.2.2 TLA+TLA+ [26] is a declarative specification language designed by Leslie Lamport. Itsmain goal is to allow the specification of practical systems on top of a simple, yetrigorous mathematical foundation. TLA+ is based on Lamportâs Temporal Logicof Actions (TLA) [25], a variant of Pnueliâs Temporal Logic [35] and uses first-order logic and set theory to formalize mathematics.Typical specifications in TLA+ consist of a definition of the systemâs initialstate as well as the transition relation that describes the possible ways that the sys-tem can make progress. The transitions between states define atomic steps in thesystem and a sequence of them form a behavior of the system. TLA+ was specif-ically designed to allow the description of what the system does in all its possiblebehaviors, as well as the verification of its functional properties. Other kinds ofproperties, such as average runtime performance or probabilistic guarantees, arenot supported by the underlying formalism.TLA+ has seen greater adoption in an industrial setting than most distributedsystem verification tools [9, 34]. Two important factors contribute to this success:7its effectiveness at describing concurrent and asynchronous systems, very impor-tant for the specification of practical distributed systems; and the development ofTLC, a model checker for the TLA+ language that is capable of verifying bothsafety and liveness properties.Figure 2.2 uses the distributed job scheduler example from Figure 2.1 and il-lustrates how distributed systems can be modeled using TLA+ and how propertiesabout the system are translated from the mathematical notation used previously.Figure 2.2: Definition of the distributed job scheduler example in TLA+. Tomake the example more interesting, the scheduler here is modeled toload jobs from some source and schedule them concurrently (expressedas a disjunction in the definition of Next). The safety and livenessproperties of Figure 2.1 are redefined here using TLA+ syntax.One advantage of TLA+ is that it allows the description of some behavior bothin terms of what a component is supposed to do as well as how that task is ac-8complished. This powerful notion of abstraction (or refinement) enables a TLA+specification to describe a system at different levels of detail and is at the core ofthe formalism.2.3 PlusCalPlusCal [28] is another specification language designed by Leslie Lamport. It is analgorithm description language that enables correctness verification. PlusCal canbe compiled to TLA+, has precise semantics and, due to its integration with TLA+,allows the designer to specify a system at different levels of abstraction.PlusCal changes the way that specifications are written from a declarative toa procedural style in order to make it easier for engineers without a strong back-ground in mathematics or formal verification to start specifying their systems with-out a lot of training. Listing 2.1 uses PlusCal to model the previous job schedulerexample.1 (* same constants as defined in Figure 2.2 *)23 --algorithm JobScheduler {4 variables AssignedJobs = [job in JobSet |-> Unassigned],5 LoadedJobs = << >>;67 macro Assign(job) {8 (* assigns a job to a node *)9 with (node in NodeSet) { AssignedJobs[job] := node };10 }1112 macro LoadJob() {13 (* loads a new job *)14 }1516 process (Scheduler = 0) {17 schedule:18 either { LoadJob() }19 or { with (job in LoadedJobs) { Assign(job) } };20 }21 }Listing 2.1: Job scheduler in the PlusCal language.PlusCal requires the user to structure a system being specified around labels(such as schedule on Listing 2.1, line 17). The statements within a label are9the atomic steps in the model. Just like in TLA+, there is a tradeoff to be madewith respect to the use of labels in a model: the more concurrency (in the formof interleavings) is allowed in the model, the closer it will be to a concrete envi-ronment; however, this comes at the cost of exponential growth of the state space,substantially increasing the model-checking time. It is up to the system designerto decide how granular these atomic steps should be to meaningfully capture asystemâs behavior.2.4 Modular PlusCalModular PlusCal is a variant of the PlusCal language developed as part of the PGoproject (see section 2.5). The language inherits PlusCalâs syntax, but adds a coupleof constructs to enable the separation between the description of the system and itsabstract components. Modular PlusCal can be compiled to PlusCal, which in turncan be translated to TLA+ and model checked against system-specific properties.Modular PlusCal introduces three important concepts:Archetypes define the components of the system being specified. They are iso-lated from one another and can only interact with the outside environment(for instance, other archetypes) by making use of parameters passed to them.Since these parameters typically represent the execution environment, theyare called resources in Modular PlusCal.Mapping macros allow the system designer to specify how the parameters passedto archetypes are abstractly modeled. They are expanded when the specifi-cation is compiled to PlusCal.Instances specify how archetypes are mapped to PlusCal processes for model-checking purposes. Archetypes are given abstractions for every parameterdeclared in its definition, as well as which mapping macros should be ap-plied, if any.In PlusCal, algorithm variables have global scope: every process in the systemcan read and update their values; this is, in fact, the only way to express communi-cation across two different PlusCal processes. Modular PlusCal, however, takes a101 --mpcal JobScheduler {2 mapping macro FIFOChannel {3 read {4 await Len($variable) > 0;5 with (msg = Head($variable)) {6 $variable := Tail($variable);7 yield msg;8 };9 }1011 write {12 await Len($variable) < BUFFER_SIZE;13 yield Append($variable, $value);14 }15 }1617 archetype JobScheduler(ref connections)18 variables j, targetNode;19 {20 schedule:21 (* schedules a job âjâ to a âtargetNodeâ *)22 sendJob:23 connections[targetNode] := j;24 }2526 variables AssignedJobs = [job in JobSet |-> Unassigned],27 (* incoming messages for scheduler: initially, no messages *)28 network = [job in NodeSet |-> << >>];2930 (* create an instance of the JobScheduler archetype with ID 0 *)31 process (Scheduler = 0) == instance JobScheduler(network)32 mapping network[_] via FIFOChannel;33 }Listing 2.2: Sending a job to an assigned node in Modular PlusCal.different approach: archetypes do not have access to global state and can only man-ifest externally visible changes by interacting with the parameters they are passed.This separation makes it easier to use different communication abstractions withoutsignificantly changing the systemâs logic.Listing 2.2 illustrates the concepts introduced in this section by having our jobschedulers communicate with one another over a network that is abstractly mod-eled as a first-in, first-out (FIFO) sequence of messages (FIFOChannel mappingmacro, lines 2-15).The specification in Listing 2.2 also demonstrates how parameters passed toarchetypes can be mapped as functions (network[ ] syntax on line 32). This11distinction between archetype resources that are mapped as functions and thosethat are not becomes relevant in the code generation process, as discussed in section3.2.1.Together, archetypes, mapping macros and instances enable the complete sep-aration between the description of system behavior and implementation-specificcomponents that are intentionally left abstract in model checking. These primitivesalso encourage a more modular specification construction by allowing abstractionsto be shared and reused across models. In this work, we leverage the clear separa-tion between the system and its execution environment to generate efficient imple-mentations of distributed systems specified in Modular PlusCal.For a more comprehensive description of Modular PlusCal, consult the lan-guage manual1.2.5 PGoPGo [39] is a source-to-source compiler from PlusCal specifications to Go imple-mentations. It was developed with the same goal as this work: automatically gen-erating an implementation for a model-checked specification. However, PGo wasinitially focused only on concurrent systems and did not support the generation ofdistributed systems.While the idea of using of PlusCal to generate implementations of distributedsystems sounds promising, it presents a number of challenges in practice. First,PlusCal requires that processes communicate by making updates to globally visibledata structures. In order to maintain PlusCal semantics, a concrete implementationwould need to provide the same globally accessible, distributed data structures, in-curring a prohibitive performance penalty. In addition, system designers typicallywish to leave certain implementation-specific details abstract. For instance, it iscommon to model whether a certain operation fails by using the either keyword(introducing a non-deterministic choice). From the compilerâs perspective, there isno way to find out the real component being abstracted away. The consequence ofthis mismatch is that the developer is then required to manually edit the generatedsource code to provide a concrete implementation for components that were left1https://github.com/UBC-NSS/pgo/blob/v0.1.4/manual.pdf12abstract in the specification. This process is error-prone and is precisely what PGoproposes to reduce (or eliminate).This work is part of the PGo compiler and adds support to the compilation ofspecifications written in Modular PlusCal to Go implementations, focused on thechallenges of compiling distributed systems.13Chapter 3Compiling Modular PlusCalSpecificationsThis chapter describes the challenges faced and techniques used in the process ofcompiling distributed systems specified in Modular PlusCal into correct implemen-tations of the model in the Go programming language. Section 3.1 introduces whatthis process means by describing how valid behaviors of a system specified us-ing Modular PlusCal are derived by the model checker; section 3.2 continues thediscussion by detailing the strategy used in this work to maintain the same execu-tion semantics in the compiled implementation in Go. Section 3.3 describes howarchetypes can be seen as the API that can be used to interact with the system beingspecified. Section 3.4 discusses the role of resources in the compilation process:how they conform to a well-defined API, and challenges faced when resources aremapped as functions. Section 3.5 introduces a common pattern in modeling longrunning processes in PlusCal, and how it can be accommodated in the design pro-posed in this work. Finally, section 3.6 discusses how failures can be dealt with ifthe specification does not account for them.3.1 Modular PlusCal Execution SemanticsVerifying whether a model described in Modular PlusCal satisfies a set of user-defined correctness properties requires it to be model-checked. This process in-14volves compiling the specification to PlusCal and translating that output to TLA+,which is the language being model-checked by TLC (see diagram in Figure 1.1).The algorithm used compute all behaviors expressed in a model (documented in[26]) is, therefore, important to this work: in order to consider the generated im-plementation correct with respect to the specification, we need to ensure that allexecutions are possible behaviors defined by the specification.To motivate the discussion, consider the specification in Listing 3.1. It de-scribes how a producer adds jobs to a shared queue and consumers read jobs fromthe queue and process them somehow. Since archetypes can only make externallyvisible changes by performing operations on parameters passed to them, the queueis passed to both the Producer and Consumer archetypes.Modular PlusCal is an extension of PlusCal and inherits the same executionsemantics [27]. In summary, behaviors of a specification are derived as follows:â¢ Labels represent atomic steps (or actions) in the specification. The modelchecker will only perform one atomic step at a time when exploring the statespace. Execution of an action consists of the evaluation of all statementsfrom that label to the next. Modular PlusCal enforces the same labeling rulesdefined by PlusCal, which are documented in the language manual [29].â¢ For an action to be scheduled (and become an event in the behavior beingexplored), it needs to be enabled. One scenario where a step is not enabled isif it contains an await statement with a predicate that evaluates to FALSE.For example, in Listing 3.1, the operations that the consumer performs onthe queue are defined by the AbstractQueue mapping macro (lines 40-41). Since the doWork action (line 25) reads a job from the queue (line 26),it will not be enabled if the queue is empty (line 4).â¢ All PlusCal processes run âconcurrentlyâ. This means that the model checkerwill explore every possible interleaving of the atomic steps (labels) definedin every process. In the context of Modular PlusCal, this implies that everyinstance created in the model executes concurrently.151 --mpcal Queue {2 mapping macro AbstractQueue {3 read {4 await Len($variable) > 0;5 with (job = Head($variable)) {6 $variable := Tail($variable);7 yield job;8 }9 }1011 write {12 await Len($variable) < QUEUE_SIZE;13 yield Append($variable, $value);14 }15 }1617 mapping macro AbstractJob {18 read { yield 0; }19 write { yield $value }20 }2122 archetype Consumer(queue)23 variable job;24 {25 doWork:26 job := queue;27 (* do some work with âjobâ *)28 }2930 archetype Producer(ref queue, jobs) {31 enqueue:32 while (TRUE) {33 queue := jobs;34 }35 }3637 variable q = << >>,38 job_stream;3940 process (ConsumerP = 0) == instance Consumer(q)41 mapping q via AbstractQueue;4243 process (ProducerP = 1) == instance Producer(ref q, job_stream)44 mapping q via AbstractQueue45 mapping job_stream via AbstractJob;46 }Listing 3.1: A queue specification in Modular PlusCal163.2 Preserving Execution SemanticsFrom the rules outlined in section 3.1, we can conclude that a naı¨ve but correctimplementation of the system could rely on a runtime scheduler to decide the orderin which actions in the Modular PlusCal specification execute. This, however,comes at a prohibitive performance cost, especially in the context of distributedsystems: no concurrency is allowed across different archetypes, even if they aredeployed separately and perform local computation that is not externally visible.To allow concurrent execution of atomic steps defined in the Modular PlusCalspecification, we let the resources dictate the safety of concurrent execution. Thisseparates the discussion into two kinds of actions:Labels that do not use any resource. Since resources are the only way an archetypecan interact with its environment, an action that does not make use of anyresource performs only local computation and is, therefore, safe to run con-currently with other atomic steps.Labels that use one or more resources. These are labels that potentially interactwith the environment. To ensure that execution semantics are preserved, theimplementation generated by PGo first acquires access to the resources usedin the label before the statements in the label are evaluated. An archetyperesource that requires exclusive access, then, can make sure that other pro-cesses attempting to use the same resource will block until the resource be-comes available again. We further refine this case by analyzing whether theresource is being used in read-only mode, a property that can be staticallydetermined from the Modular PlusCal specification.Resource acquisition has semantics that are specific to the environment theyrepresent: for instance, a resource that encapsulates shared state may use locks toensure that access is exclusive. Resources are acquired at the start of every label.We analyze the specification and determine which resources are used in each ac-tion, as well as the permissions necessary (read-only or read-write). The resultingimplementation, then, first acquires all resources that are used in the atomic step,performs the operations defined in it, and releases the resources. However, thisprocess is unsafe: suppose two actions, A1 and A2, use resources r1 and r2, which17require exclusive access. Also, suppose that concurrent execution of A1 and A2leads to the following sequence of events:â¢ A1 acquires exclusive access to r1.â¢ A2 acquires exclusive access to r2.â¢ A1 attempts to acquire exclusive access to r2; it blocks because A2 alreadyhas access to it.â¢ A2 attempts to acquire exclusive access to r1; it blocks because A1 alreadyhas access to it.In other words, acquiring all resources at the start of an action can lead todeadlocks. For this process to be safe, resources need to be acquired in a consistentorder: if r1 and r2 are used in two different actions, they need to be acquiredalways as either ãr1,r2ã or ãr2,r1ã. This is ensured by enforcing that concreteimplementations of archetype resources are comparable to one another.While we do not provide a proof that the concurrent execution model presentedhere actually preserves the execution semantics of Modular PlusCal and the TLCmodel checker, we sketch an informal reduction [32] argument, as has been donein previous work [17]. Consider two actions running concurrently in an implemen-tation of a Modular PlusCal specification. There are three cases to consider:1. One of the labels does not use resources. This case is always safe to beexecuted concurrently. Since local computation is not externally visible, weargue that concurrent execution is equivalent to an execution where all of thestatements involved in the local computation step happen before (or after) theother actionâs statements. Both event orderings should have been exploredby TLC and are, therefore, possible behaviors of the system.2. The labels use disjoint sets of resources. This case is always safe to beexecuted concurrently. Since the actions interact with disjoint parts of theenvironment (represented by the resources they use), concurrent executionis equivalent to an execution where all statements in one label are evaluatedbefore (or after) the statements in the other. As with the previous scenario,the model checker should have explored both possibilities.183. The labels use overlapping sets of resources. This case is not always safe tobe executed concurrently. However, with the strategy described above whereresources are first acquired before they are used, execution will run one ofthe actions to completion first, and only then execute the statements in theother; this sequential execution is similar to the execution model used byTLC.3.2.1 Resources Mapped as FunctionsArchetype resources in Modular PlusCal can be mapped as functions (see section2.4 for an example). If a resource r is mapped as a function, it will only be ex-panded (according to the abstraction defined in the mapping macro) if it is used asa function (i.e., r[expr]). This is useful, for example, if an archetype parameterrepresents connections to a set of nodes (the number of which is a parameter of themodel) and, as a system designer, you intend to express the sending of a messageto a particular node in that set of connections.Resources mapped as functions, however, pose a challenge to the compilationstrategy described in section 3.2. In particular, it becomes no longer possible to ac-quire all resources used in an action before it executes because the argument passedto the function may not be known when control reaches the start of the atomicstep. For example, consider the specification in Listing 2.2, where the networkresource passed to JobScheduler is mapped as a function. In the sendJobaction, the job j is sent to a targetNode; if the value of targetNode changesin the action before it is used as an argument to connections, acquiring allresources beforehand would lead to incorrect behavior. Listing 3.2 illustrates theissue.1 sendJob:2 targetNode := targetNode + 1;3 connections[targetNode] := j;Listing 3.2: An example where it is not possible for an implementation toacquire access to all resources before an action starts. targetNode ismutated before it is used as an argument to connections; using its valuefor resource acquisition before the action starts leads to incorrect be-havior.19Algorithm 1: Action ExecutionactionCompleted = FALSE;while ¬ actionCompleted doAcquire all resources not mapped as functions in consistent order;... action statements ...;/* A resource mapped as function is required atthis point */error = Acquire(resourceMappedAsFunction);if error 6= NULL thenAbort all resources acquired so far;if ShouldRetry(err) thencontinue;endreturn errorend... more action statements ...;/* End of action */Release all acquired resources;actionCompleted = T RUE;endFigure 3.1: Executing an action that uses resources mapped as functions.Due to the impossibility of acquiring all resources that are mapped as func-tions before an atomic step begins, we resort to a best-effort approach. Resourcesmapped as functions are acquired at the time of use; this guarantees that the valuesof the arguments used are accurate. In addition, the implementation we generatekeeps track of all resources previously acquired in each step to make sure that noresource is acquired twice in the same action. This approach, however, can lead todeadlock: since resources are acquired at the time of use, we can no longer enforcea consistent order as described in 3.2. To circumvent this issue, we allow resourceacquisition to fail and, when a failure is detected, we abort any changes made to theenvironment and try again. Figure 3.1 specifies how an action in Modular PlusCalis translated to a concrete implementation in light of the discussion presented here.Since an action has no externally visible interactions with the environment be-fore it completes, and the changes proposed here to support resources mapped as20functions never leave the boundaries of a single action, we argue that the the exe-cution model described in Figure 3.1 does not impact the reduction argument madein section 3.2.3.3 Archetypes as APIsModular PlusCal uses archetypes to describe the behavior of components in a sys-tem; therefore, they can be seen as defining execution entrypoints of the systembeing designed. For this reason, the implementations we compile transform eacharchetype instantiated in the Modular PlusCal specification into a Go function.Listing 3.3 shows the signatures of the resulting functions when the queue specifi-cation in 3.1 is compiled.1 package queue2 import "pgo/distsys"3 var QUEUE_SIZE int4 func init() {5 QUEUE_SIZE = 106 }7 func Consumer(self int, queue distsys.ArchetypeResource) error {8 // body9 }10 func Producer(self int,11 queue distsys.ArchetypeResource,12 jobs distsys.ArchetypeResource) error {13 // body14 }Listing 3.3: Function signatures in Go when the specification in Listing 3.1is compiled with PGo.A few points are worth highlighting in this transition:â¢ The compiled code lives in a separate package (called queue in Listing3.3). The developer wishing to use the the system compiled by PGo canimport this package and call the functions defined there, passing a concreteimplementation for every resource.â¢ TLA+ constants (parameters of the model) used in the specification are givena concrete value when the user compiles their specification. All constants21are assigned in the init function, which the Go runtime ensures will beexecuted exactly once if the package is imported.â¢ Every function compiled for an archetype needs to be passed self as thefirst argument. This is an implicit variable in PlusCal specifications thatcontains the process identifier.â¢ For every parameter declared in the archetype definition, a correspondingArchetypeResource is expected in Go. Archetype resources have awell defined interface (see section 3.4). It is up to the caller to ensure that theconcrete implementation passed in has the same semantics as the abstractionused in the specification. The PGo runtime provides a number of commonlyused components in distributed systems, such as communication channels,access to the file system, time, among others; their implementation is thefocus of Chapter 4.â¢ Functions derived from archetypes return errors. These errors are used toindicate when the specification reached a state that cannot be mapped toa state in the specification. For example, the AbstractQueue mappingmacro of Listing 3.1 does not specify what happens if the queue cannot beaccessed. However, a practical implementation may require that the queue bestored across multiple servers, and a network failure could render the queueunavailable. In these scenarios, the error is returned to the caller, that is thenresponsible for determining what to do in response. Fault tolerance in thissetting is discussed in section 3.6.Once the specification is compiled to a Go package, the user is required to writethe programâs main function. In general, this will involve writing âglueâ code thatsets up the connections between processes and creates the concrete implementa-tions for archetype resources. Most of the difficulties of this process, however, arealleviated by the execution runtime provided by PGo.3.4 Resources as InterfacesListing 3.1 defines two archetypes, Consumer and Producer. Both the queueand the jobs that are submitted to it are abstractly modeled in the specification; the22system designer can still write and verify properties about how jobs are processedwithout having to specify lower-level details of the queue. An implementation ofthis specification, however, would need to inject a concrete implementation fora queue and a stream of jobs to be processed. These could come from anotherserver, the file system, or another source: as long as the semantics provided bythe concrete implementation match the abstraction used in the specification, thesystemâs behavior is preserved.In order for the Modular PlusCal execution semantics to be preserved as de-scribed in the previous section, however, the implementation of resources mustsatisfy a set of functional requirements. For that reason, we view archetype re-sources as implementations of a well-defined interface. Resources and resourcesmapped as functions defined as Go interface types are provided in Listing 3.4.1 type ArchetypeResource interface {2 Acquire(access ResourceAccess) error3 Read() (interface{}, error)4 Write(value interface{}) error5 Release() error6 Abort() error7 Less(other ArchetypeResource) bool8 }910 type ArchetypeResourceCollection interface {11 Get(value interface{}) ArchetypeResource12 }Listing 3.4: Type definitions for archetype resourcesThe Go language considers that a type implements a certain interface if it de-fines the same set of functions with matching signatures. A valid implementationof an archetype resource, however, has to obey stronger rules. The precise mean-ing and expectations for every function defined in the ArchetypeResourceinterface in Listing 3.4 are described as follows:Acquire is invoked when access to a resource is required in the execution of anaction. In the case of a resource mapped as a function, it is called imme-diately before the statement that uses it. Acquire takes as parameter aResourceAccess struct that defines how the resource is used in the ac-tion (for instance, read-only or read and write).23Read is called when the archetype resource is used within an expression. Thereturn type of this function may be relevant depending on the expression inwhich it is used: if the Modular PlusCal specification uses a resource r inthe expression r + 1, then the return of the Read function will be cast toan integer in the code generated by PGo. It is up to the archetype resourceimplementation to make sure that the types returned by this function arecompatible with the expectations of the caller.Write is invoked when an archetype resource is used on the left side of a ModularPlusCal assignment; the value being assigned corresponds to the valueargument that this function receives. If Write has to perform type-specificoperations, it needs to cast the received value to the appropriate type. It is upto the resource implementation to ensure that casting is safe and compatiblewith how the resource is used in the specification.Release is called on all resources that are used in an action that is executed to com-pletion. This is the only function in an archetype resource implementationthat is allowed to perform externally visible changes.Abort is used when interactions performed with a resource (in the form of Readand Write calls) need to be aborted. For instance, Figure 3.1 aborts re-sources acquired until a certain point when an error occurs and the actionneeds to be restarted. After Abort returns, the caller no longer holds accessto the resource.Less defines how the archetype resource can be compared with another resource.This allows PGo to generate code that acquires resources in a consistentorder, as discussed in section 3.2. The semantics of Less are defined by thesort package of the Go language1.Resources mapped as functions are seen as a map from a certain domain (spe-cific to the environment they describe) to implementations of concrete resources.They are defined as implementations of the ArchetypeResourceCollection1https://golang.org/pkg/sort24interface. The Get method is invoked when resource[expr] is used in a state-ment: it is given the expression passed as argument and is expected to return animplementation of an archetype resource. In addition, implementations should en-sure that if Get is called multiple times with the same argument, it should return areference to the same resource implementation (and not copies of it).3.4.1 Handling ErrorsWith the exception of Less, all functions that must be implemented by archetyperesources may return errors (Listing 3.4). To ensure that PGo generates correct im-plementations, these functions can return two types of errors: AbortRetryErrorand ResourceInternalError.Archetype resource implementations may choose to request the current actionto be aborted: this avoids the deadlock issue described in section 3.2.1. Whenanother failure happens during the processing of an operation, the implementationcan also return internal errors: these represent unrecoverable situations and arepropagated back to the caller. Internal errors can be seen as the implementationreaching states that are not part of any behavior in the specification. Table 3.1describes some examples of the two different kinds of errors.Error ExamplesAbortRetryError Locking a resource that is alreadylocked; reading a network messagewhen none was received; sending amessage to a node that has no bufferspace to process it.ResourceInternalError I/O error when reading a file orsocket; timeout when performing anetwork operation.Table 3.1: Possible errors an archetype resource implementation may return.3.5 Long Running ProcessesA common idiom when specifying how different components in a system inter-act concurrently is to express them as long running PlusCal processes. This is25especially important in the context of distributed systems: application designersare interested in verifying that certain correctness properties are maintained whenthe execution of multiple roles in the system (clients, servers, leaders, replicas)is concurrent. In Listing 3.1, for example, the Producer process runs withouttermination and keeps pushing jobs to the queue.A more interesting case is illustrated in the definition of the Consumer pro-cess in the same specification. The consumer reads the next job to be processedin the queue, does some work, and terminates. While this might be the behaviorintended by the system designer specifying an API to interact with this system, itcauses subsequent jobs pushed by the producer to not be processed if all consumersterminated. This need to model a system that is constantly pushing new jobs andworking on them concurrently, coupled with the fact that PlusCal does not supportâdynamicâ process spawning leads to processes like Consumer to also be definedas infinite loops.This potential mismatch, however, can be unified using the notion of archetyperesources presented in this work. If the Consumer archetype is changed to beexecuted in a loop that is conditioned by an argument passed to it, the developeris able to have an infinite loop for model checking purposes, and still be able tocontrol the execution of the resulting function as if it were a regular, one-off call.Listing 3.5 describes the proposed change.1 archetype Consumer(queue, startSignal)2 variable job;3 {4 consumerLoop:5 while (startSignal) {6 doWork:7 job := queue;8 (* do some work with âjobâ *)9 }10 }1112 instance (ConsumerP = 1) == instance Consumer(queue, TRUE)13 mapping queue via AbstractQueue;Listing 3.5: Updating the definition of the Consumer archetype to run in aloop: the consumer processes jobs as long as a signal sent to it is true.When using the code generated by PGo for the consumer process as defined in26the previous listing, the developer can call the Consumer function generated bythe compiler in the background, passing as startSignal an implementation thatblocks when attempted to be acquired. When the user actually wishes to processa job in the queue, the resource unblocks and returns true, allowing executionto continue. Fortunately, the Go language makes this straightforward: functionscan be executed in the background with Go routines, and channels have the exactsemantics described here and can be used as a concrete implementation of thestartSignal parameter.3.6 Dealing with FailuresThe possibility of failure is one of the reasons that make writing correct distributedsystems challenging. In most cases, the system needs to detect when a failurehappens and perform some recovery procedure to continue making progress. Inaddition, different systems can choose to support different failure models: for in-stance, a protocol may be designed to accommodate crash-stop failures, but notByzantine failures [30].Systems compiled by PGo are as fault-tolerant as the specification itself: in par-ticular, if the system uses abstractions that model the possibility of failure and thesystem is designed to tolerate them, the generated implementation should be ableto present the same behavior, provided the archetype resource implementationsexhibit the same semantics as the abstraction. Consider Listing 3.1 and supposethe user is interested in writing a property that states that every job pushed by theproducer is eventually processed by the consumer in the correct way. While thisproperty may hold for the specification in Modular PlusCal, it would not hold ina concrete implementation if the consumer node were to crash, for example; notethat if a similar event happened in the specification, the liveness property statedbefore would be violated.Providing language-level support for fault-tolerance is currently future work inthis project. However, the proposed design and execution model leaves a few op-tions for users that intend to design fault-tolerant systems. We discuss two possibil-ities to handle failures in the current design: dealing with failures when interactingwith the environment; and recovering from crash-stop failures.273.6.1 Recovering from Errors in the EnvironmentAs described in section 3.3, the functions used to interact with an archetype canreturn errors; when these indicate an error situation that is not part of the abstractionin the specification, the error is returned to the programâs main function, which ismanually written by the user.Consider the definition of the Producer archetype in Listing 3.1, and supposethat the implementation of the queue passed to it issues a network call to push jobsto a replicated object store. A user could recover from failures of this remotestore by inspecting any errors returned by the corresponding function, choosing adifferent replica when a failure is detected, and restarting the function. Listing 3.6illustrates how this could be achieved in Go.1 queueObj := RemoteQueueAt(master)2 jobStream := NewJobStream()34 // queue.Producer should run indefinitely unless an error occurs5 for {6 err = queue.Producer(queueObj, jobStream)7 switch err.cause.(type) {8 case *object_store.MasterTimeout:9 master = electNewMaster()10 queueObj = RemoteQueueAt(master)1112 case *job_stream.IOError:13 // deal with job stream error14 }15 }Listing 3.6: Recovering from a failure by restartingThe pattern illustrated here can be used to detect multiple kinds of errors andrecover from them appropriately, as the previous code snippet shows: a failurein the job stream can also be detected and potentially recovered from, dependingon the semantics of the implementation passed to the Producer function. Tomake this process easier, the implementation generated by PGo will make sure that,when an error that is returned to the user occurs, all resources previously acquiredare aborted before the function returns; this guarantees that no externally visiblebehavior is observed if the failure happens while executing a statement halfway inan atomic step. Despite this fact, the system should be prepared to be restarted at28arbitrary points: while this may be the case for some specifications, PGo requiresthat the user design the system for that possibility.3.6.2 Crash FailuresMany reasons could lead to a system crashing: hardware faults, power failures,bugs in the software stack (operating system, programming language runtime,an archetype resource implementation), among others. While entirely supportingcrash recovery in a system requires the specification to be aware of the fact thatapplications may stop at arbitrary points in time, the user is capable of performingrecovery under certain circumstances using the application design proposed in thiswork.One way to add fail-stop tolerance to a specification that does not model crashesis to hide their occurrence completely. If the crashed process can be restarted in adifferent machine where it left off, the failure can become invisible to the other pro-cesses in the system. To illustrate this mechanism, consider how a user may specifytheir system to capture local state (Listing 3.7) and allow it to be recovered.1 archetype Producer(ref queue, jobs, ref context)2 variable nextJob;3 {4 producerLoop:5 while (TRUE) {6 readJob:7 if (context.action = "readJob") {8 nextJob := jobs;9 context := [action |-> "processJob", job |-> nextJob];10 }11 processJob:12 if (context.action = "processJob") {13 (* process job in âcontext.jobâ *)14 }15 }16 }Listing 3.7: Capturing local state in a context object in order to make it ac-cessible in the event of a crash.By having execution be dictated by a context, the user is able to start computa-tion at arbitrary steps in the definition of the Producer archetype. Specifically,if the implementation of the context object passed to the producer updates the state29in a persistent store, an external monitor process can detect failures in the producernode and start another instance of the same function. Since the context is stored ina different source, it can be read by the new instance, and execution may resume.Note that while the approach above is sufficient to handle fail-stop failures inmost circumstances, it still requires careful, manual error handling from the devel-oper. In particular, if the crash happens during the process of releasing resources,the system could be left with a partial state change leading to behavior that isnot part of the model-checked specification. In this scenario, the programmer isrequired to correct these inconsistencies before attempting a restart. While theexecution runtime could help in the recovery process by providing stronger trans-action semantics with a write-ahead log implementation [33], this is currently notsupported.30Chapter 4Execution RuntimeIn this chapter, we discuss the runtime support provided by PGo to applicationsthat were compiled from Modular PlusCal specifications. In section 4.1, we de-scribe the protocol used to make sure all components of the system are connectedand start execution at the same time. PGo also provides some implementations ofcommonly used resources in distributed applications: distributed global state canbe easily used as a resource (section 4.2); and direct communication channels arealso provided as a convenience to applications based on message-passing (section4.3). Finally, section 4.4 provides an overview of other resources provided by thePGo runtime and how they can be used by system designers when compiling theirspecifications into executable implementations.4.1 Synchronized StartWhen a Modular PlusCal specification is compiled to TLA+ and model-checked,all enabled states are scheduled infinitely often if they remain enabled (assuming aweak fairness model; for a longer discussion of fairness in TLA+, see [26]). In aneffort to replicate this behavior in the context of a distributed system, we providetools for the developer to enforce a distributed barrier, allowing all componentsof the system to start at the same time. For example, in the context of the queuespecified in Listing 3.1, synchronization could enforce that the producer does notinundate the queue with jobs before consumers are ready to process them.31PGo provides an implementation of a distributed barrier that also makes surethat every component is connected to each other. Figure 4.1 shows one executionof the protocol to illustrate how it works.Figure 4.1: Synchronization protocol provided by the PGo runtime to allowapplications to optionally coordinate their start.32As used here, a process loosely corresponds to a component in the systembeing designed. Since archetypes define the API that developers use to interactwith the system, there is no one-to-one correspondence between their definitionsand processes: there could be multiple archetypes associated with the same com-ponent, likely executing in the same host when deployed. Processes are, in gen-eral, deployed on different hosts, although that is not a requirement of the model.In the context of the queue specification of Listing 3.1, processes P1, P2 andP3 in the diagram of Figure 4.1 could be Consumer(0), Consumer(1) andProducer(2), respectively (numbers in parentheses are the process identifiers;the implicit self variable in PlusCal specifications).One arbitrary process in the system is assigned the role of coordinator of thesynchronization protocol. The coordinator process does not need to be the firstprocess to be executed: in Figure 4.1, for example, process P2 is chosen to be thecoordinator, but P1 is the one that comes online first. When it tries to reach thecoordinator, the call fails; processes keep trying to reach the coordinator until theyeventually succeed. Once every process reported that they have connected to everyother node in the system, the coordinator is responsible for informing them thatthey may start execution of their respective functions.The messages exchanged during the synchronization protocol are briefly de-scribed below:DIAL. When processes are created, they attempt to send a DIAL message to thecoordinator, including the network address where they are deployed. As de-scribed previously, a failure in this process causes processes to keep tryingto contact the coordinator until they finally succeed. The coordinator ac-knowledges DIAL messages, and processes then wait for a message fromthe coordinator.{ P1, ..., Pn }. As soon as the coordinator receives DIAL messages fromevery process, it sends a list of network addresses where every other processin the system active. This list is aggregated from the DIAL messages thatthe coordinator received from every process.CONNNECTED. When a process receives the list of other processes in the system33from the coordinator, it establishes a connection with them. When that iscompleted, a CONNECTED message is sent to the coordinator to indicatethat the process is ready to start execution any time.START. When the coordinator received CONNECTED messages from every pro-cess, it is then responsible for informing the processes that they may startexecution of their functions in the system. The coordinator sends a STARTmessage to every process to express that intent.4.2 Distributed Global StateAs described in section 2.4, communication between processes in PlusCal happensvia updates on global state; while Modular PlusCal makes it easier to use differentcommunication abstractions, relying on global state can be more convenient forsome applications. For this reason, PGo provides an implementation of distributed,shared state that developers can use as archetype resources in implementations.This component can be especially useful if the system has already been specifiedin PlusCal, where communication is achieved via updates on global state, but thesystem designer wishes to translate it to a Modular PlusCal specification in order tomore clearly separate implementation-specific concerns from protocol definition.The implementation of global state in PGo assigns an owner to every objectstored; however, object ownership is a dynamic property. Nodes may become own-ers of objects they use (if, for example, a series of operations will be performed onthem over a short period of time) and ownership can be controlled via application-specific policies. The design and implementation is similar to, and inspired by,previous work in distributed object systems and programming languages [19, 33].4.2.1 Data StoreGlobal state in the system is stored in each nodeâs data store. A nodeâs data storerepresents the global state information that each node knows about at an arbitrarypoint in time. In particular, it includes the name associated with a portion of thestate; the believed owner of that variable: i.e., the node that knows its current value;and the value of the variable. Figure 4.2 illustrates a snapshot of the data stores in34(a) P1(b) P2 (c) P3Figure 4.2: State of the data stores in every node in a system at a certain pointin time. A value is only associated with a global variable if the nodeowns the data. Ownership information may be outdated: for instance,P3 believes that history is owned by P1 when it is, in fact, owned by P2at this moment.a system with three processes and three global variables.The most important aspects of how the data store is managed are summarizedbelow:A process is aware of the data it owns. There is always at most one process thatbelieves to own a variable of the global state. More specifically, for everyvariable in the global state, there is either exactly one process where theowner column of the corresponding data store entry points to itself; or own-ership is being transferred to another node. In the period it takes for theownership transfer message to reach the new owner, no node owns the data.No data is kept for state that is not owned. If a node does not own a variable inthe global state, it keeps no value associated with it (even if it owned thevalue before), avoiding inconsistency and unnecessary memory use. If anoperation on an object that is not owned is required, the caller needs to obtaina reference from the owner before the operation can be performed.Ownership information may be outdated. When the ownership of an object ismoved from one process to another, the update is not visible to other pro-cesses that were not involved in the exchange. For this reason, ownershipinformation in the data store may be outdated; in particular, processes thatreceive requests for a reference to variables that they no longer own respondwith the node that is believed to own the variable at that moment (that is,35their current owner entry for the variable in their data store). The requesterthen updates its own data store and repeats the process until it finally gets areference to the object.Global state can hold data of arbitrary types. The types of the values associ-ated with each variable in the global state are not maintained by the datastore. Instead, these values are serialized and need to be converted to theirappropriate types by the caller (if they wish to perform operations on them).In practice, the implementation relies on the gob1 serialization format, andsupports the same sets of types and values.Migration can be controlled via application-specific policies. When a request fora reference to a variable reaches the process that owns that state, it can chooseto move ownership to the caller. Applications can provide their own policiesto determine when moving should be allowed by implementing a simple in-terface (see Listing 4.1). The PGo runtime provides two simple migrationpolicies, allowing processes to always (or never) migrate the data to the re-quester.1 type MigrationStrategy interface {2 // ShouldMigrate is called when a process ârequesterâ is attempting3 // to get a reference to a varible of the given ânameâ.4 ShouldMigrate(name, requester string) bool5 }Listing 4.1: Applications can provide a custom migration policy in the formof a definition of a ShouldMigrate function, defined when the user cre-ates the global state resource.4.2.2 ProtocolThis section describes the underlying protocol that implements the semantics ofthe data store and object ownership described in 4.2.1. One of the key ideas be-hind the protocol is that references are obtained in lexicographical order of their1https://golang.org/pkg/encoding/gob/36names. This notion is similar to acquiring archetype resources in consistent orderas described in section 3.2 and avoids deadlocks under concurrent execution.When a reference to a variable is obtained by a process, it causes subsequentrequests for the same variable (from the same or other processes) to block untilthe reference is released. In other words, only one process in the system can haveaccess to shared state at a time.We discuss the protocol by overviewing three examples of its execution in in-creasing levels of complexity. In the diagrams that follow, arrows represent net-work calls performed from one process to another; straight vertical lines representprocess execution over time.Scenario 1: Borrowing a Single Variable (Figure 4.3) In this scenario, node P1wants to grab a reference to (borrow) variable a, which is believed to beowned by node P2. P2 turns out to actually have the ownership of a, so itreturns a reference to it back to P1. The green line in P1 indicates the timeduring which it has exclusive access to a and runs application specific logic.In the meantime, a third node, P3, wishes to get access to a too. However,since that variable is currently borrowed to P1 (the entry in the data store islocked), the call is blocked (red line on P3). When P1 is done using variablea, it sends a RELEASE message to P2. At that point, the entry for variable ais unlocked, and P2 can now borrow variable a to P3, which had been waitingfor it.Scenario 2: Multiple Variables and Outdated Ownership (Figure 4.4) This sce-nario illustrates how a node may combine requests for references to differentvariables in the same message. P1 wants to borrow variables a and b, whichit believes are owned by node P2. When P2 receives the request, it noticesthat it indeed owns variable a, but not variable b â it was previously movedto node P3. Therefore, P2 returns a reference to variable a (allowing P1 touse it) and indicates that b has moved to process P3. When receiving the re-sponse, P1 updates its data store to indicate that b is owned by P3 and moveson to request access to b from it. P3 grants it access, and P1 is able to use aand b exclusively (green line in the diagram). Once P1 has used a and b, itcan release the references that it borrowed â first to P2 (for variable a) and37Figure 4.3: Borrowing a single variable from another process.then to P3 (for variable b).Scenario 3: Ownership Move (Figure 4.5) This scenario is more complex andinvolves a number of complicated conditions. The order of events depictedin the diagram are:â¢ Process P1 wants to have exclusive access to variables a, b and c,which it believes are owned by node P2.â¢ Node P2, when receiving the request, consults its data store and realizes38Figure 4.4: Requesting multiple references in the same message. In this ex-ample, P2 no longer owns variable b, and it informs P1 that the newowner is believed to be P3.that while it does own variables a and c, variable b was previouslymoved to P3. In addition, it decides to move ownership of variable a toP1. In the diagram, a*: OK indicates that P2 returned a reference to a,including ownership of it.â¢ Since b has moved to P3 (according to P2), a reference to c cannot bereturned to P1 at this point. Exclusive access to variables need to beacquired in lexicographical order to avoid deadlocks. Thatâs what c:SKIP in the diagram indicates.â¢ When receiving the reply from P2, P1 notices that it received a refer-ence to a that includes ownership of the variable. It updates its data39store to indicate that it now owns variable a and acknowledges P2 thatit successfully received ownership of a and is ready to handle requestsrelated to a.â¢ In the meantime, however, process P3 wishes to have exclusive accessto a, which it believes is owned by P2 (and it indeed was until momentsago, before P2 decided to move ownership of a to P1). Since P2 knowsthat an ownership move of a is currently underway, it blocks until anacknowledgment from P1 is received.â¢ P1 sends an ACK(a) message to P2, indicating that ownership move iscompleted. Once that message is received, P2 is ready to tell P3, whichhad been waiting, that a moved to P1.â¢ P1 continues its Acquire process (this interaction started with P1needing exclusive access to a, b and c). Since it already has accessto a (and owns it), it moves on to request b from P3, and eventuallyreceives a reference from it.â¢ In the meantime, P3 itself wants access to variable a, which it nowknows that itâs owned by P1. Since P1 itself is currently using a exclu-sively for its own purposes, that request is blocked (red line on P3 inthe diagram).â¢ Finally, P1 requests variable c to P2, which then returns a reference toit (without ownership this time). Since P1 has now exclusive access toa, b and c, it can now run its application logic (green line on P1 in thediagram).â¢ Once the P1âs computation is over, it has to release the references it pre-viously acquired. Variable a is now owned by it, so a local RELEASEcall is performed. As soon as that is done, a reference to variable a canbe returned to P3, who had been waiting for some time. P1 then moveson to release b (from P3) and c (from P2).40Figure 4.5: A complex interaction between processes P1, P2 and P3 whereownership is moved and concurrent access to global variables needs tobe resolved. Names in curly braces indicate which variables are ownedby the processes at different times.414.3 Communication ChannelsThe global state infrastructure provided by PGo exposes a shared-memory abstrac-tion to the resulting distributed system: every process can read state that is shared,and updates are immediately visible after the corresponding action completes. De-spite its simple semantics, distributed global state can come at a significant per-formance cost. A high contention environment, where multiple processes race toread and write shared state, can slow the system down, leading to degraded per-formance. In the context of distributed systems, however, it is common to think ofthe interactions between the components of a system in terms of the messages theyexchange. To support this common pattern, PGo provides an archetype resourceimplementation that allows processes to send messages to one another.Message-passing support in PGo aims to be an implementation of a communi-cation channel with TCP-like semantics: messages are received in the order theywere sent; no messages are lost, duplicated or corrupted. Each process communi-cates with other components in the system by posting messages to their mailbox;the idea is inspired by how actors communicate in an actor-based model [1, 18].The communication abstraction targeted by this implementation, in the form of aModular PlusCal mapping macro, is defined in Listing 4.2. Figure 4.6 illustrates asystem of three processes using the message-passing implementation described inthis section.Figure 4.6: Three processes connected to each other. Each have a local mail-box of fixed capacity; when processes want to communicate, they senda message that is appended to the receiverâs mailbox.421 mapping macro ReliableMailboxes {2 read {3 await Len($variable) > 0;4 with (msg = Head($variable)) {5 $variable := Tail($variable);6 yield msg;7 };8 }910 write {11 await Len($variable) < CAPACITY;12 yield Append($variable, $value);13 }14 }1516 variable connections = [id in NodeIds |-> << >>];1718 process (P in NodeIds) == instance SomeArchetype(connections)19 mapping connections[_] via ReliableMailboxes;Listing 4.2: Definition of the message-passing abstraction supported by thePGo runtime.The implementation of this mailbox-based resource is a simple wrapper on topof the underlying TCP stack. However, it is important to notice two importantaspects of the ReliableMailboxes abstraction as defined previously:â¢ A PlusCal process that attempts to read a message from its mailbox is not en-abled until there is at least one message to be read. To preserve these seman-tics, the implementation provided by PGo employs the following strategy: ifan attempt to read a message is made when the mailbox of the correspondingprocess is empty, the Read call fails with an AbortRetryError, causingthe action to be restarted. With enough time, the expected message shouldeventually reach the running process (as this was behavior tested in the spec-ification).â¢ Similarly, a process that attempts to send a message to another process (posta message to the targetâs mailbox) will not be enabled if the destination mail-box is full (number of queued messages is equal to CAPACITY). In practice,the mailbox capacity is set to relatively low values for model checking pur-poses (to avoid exponential state-space growth) but can be set to arbitrarily43large values in a real implementation. PGoâs strategy for this case is to havethe receiver return an error to the caller when a message cannot be receiveddue to a full mailbox The Write call on the connection, then, fails withAbortRetryError, causing the action to be restarted. Eventually, the re-ceiver has processed enough messages to allow the sending of the message.4.4 Other Common ResourcesApart from valid implementations of the archetype resource API (discussed in sec-tion 3.3) for the communication of two processes across the network, this workalso provides a number of other implementations that are useful for building realsystems. In this section, we briefly describe some of them.File System Access. Reading and writing to persistent storage is a common con-cern that is abstracted away in specifications written in Modular PlusCal.One way to reconcile these abstractions and a concrete implementation is bypassing a file system parameter to archetypes and mapping it as a function.The PGo runtime provides a FileSystemResource that implements theArchetypeResourceCollection interface (see Listing 3.4). Whengiven an arbitrary path in the system, this implementation is able to read andwrite files on behalf of the application and has the semantics expected by theresource API.Locally Shared Data. Since archetypes can be seen as defining the API used tointeract with the system, it is possible that multiple of the generated Go func-tions will be invoked in the same OS process. If they need to share data whileexecuting concurrently (for instance, in different Go routines), they need tomake sure their use of shared data is consistent with their atomic steps. PGoprovides an implementation of local, shared data that processes can use inorder to preserve Modular PlusCal execution semantics.Time. Time is another entity that is represented abstractly in Modular PlusCalspecifications. One alternative to model time is to pass an argument that isabstracted as a simple counter in the specification; however, a concrete im-44plementation can use PGoâs TimeResource object that returns the currenttime when read.45Chapter 5ImplementationIn this chapter, we briefly describe implementation details of the techniques de-scribed in previous chapters. Section 5.1 outlines the changes in the PGo compilerperformed in this work, and section 5.2 discusses updates in the execution runtime.Table 5.1 summarizes the implementation effort involved in this work.Component Language Modules LOCCompilerJavaArchetype Resource Usage Analysis 538Go Code Generation 2658Local State Snapshots 379Total 3575RuntimeGoSynchronized Start 275Distributed Global State 724Communication Channels 453Other Archetype Resources 267Total 1719Table 5.1: Lines of code (LOC), excluding comments and blank lines,changed for the components of PGo updated in this work.5.1 PGo CompilerThis work was implemented as an extension of the PGo compiler. Support for theverification of the Modular PlusCal language already existed, by translating it toPlusCal. The changes performed to support this work involved:46Static analysis of the specification. Once the Modular PlusCal model is parsed,we traverse the abstract syntax tree (AST) to determine which archetype re-sources are used in each atomic action. The compiler uses this information inorder to generate code that calls the Acquire function with the appropriateResourceAccess object (see Listing 3.4).Code generation. A new compilation pass was added to PGo that transforms theModular PlusCal AST into a Go AST. This involves: implementing the actionexecution algorithm described in Figure 3.1; acquiring (releasing) archetypeparameters on the start (end) of every action; creating a snapshot of localstate at the start of every label so that actions can be restarted; and trans-forming resource reads and writes into appropriate calls to the archetyperesource API. In addition, we also keep track of every resource mapped as afunction that is acquired in each action to avoid acquiring the same resourcetwice (since they are not statically distinguishable).5.2 Distributed RuntimeSpecifications of distributed systems compiled with PGo rely on a runtime to pre-serve the execution semantics of the specification. This work extended the PGoruntime by including the definitions of archetype resources presented in Chapter 3,as well as multiple implementations of the interface (described in Chapter 4). Allinter-process communication, necessary to provide synchronized start (4.1), globalstate (4.2) and communication channels (4.3), is built on top of Goâs RPC library1.1https://golang.org/pkg/net/rpc/47Chapter 6EvaluationIn this chapter, we provide an evaluation of the techniques and mechanisms de-scribed in the previous chapters. In particular, we are interested in answering thefollowing questions:1. Is the implementation sufficiently robust to support the compilation of com-plex specifications?2. Do systems produced by PGo have behavior that is defined by the specifica-tion?3. What is the performance of systems compiled by PGo and how does it com-pare with similar, handwritten implementations?Section 6.1 addresses the first question by describing the specifications com-piled in this work and their complexity. Section 6.2 discusses whether the resultingsystem has behaviors that are valid according to the specification. Finally, section6.3 describes performance measurements and discusses results.6.1 Specification ComplexityOur evaluation is based on two models of distributed systems written in ModularPlusCal. Table 6.1 summarizes their complexity. The behavior defined by eachmodel is described below:48Load Balancer. This model defines the interaction between three components ofa system: a set of clients, a set of servers, and a load balancer. Clients sendrequests for files to the load balancer, which in turn redirects them to one ofthe servers. The load balancer chooses the server to redirect requests to ina round-robin fashion. While simple, this specification illustrates the use ofcommunication channels across all components defined in the model; and,the use of a file system abstraction coupled with the corresponding resourceprovided by the PGo runtime allowing clients to request real files under thedirectory that the servers are running on.Replicated Key-Value Store. This model defines the behavior of a key-value storewith serializable key-value consistency semantics. It specifies a replicatedstate machine (RSM) that uses Lamport logical clocks [24] to determine or-dering and stability, as described in [36]. In summary, this setting allowsall replicas to be consistent without ever communicating with one another.Clients broadcast write (Put) operations to all replicas and send periodicclock-update messages. Clients are also allowed to disconnect: in this case,their clocks are no longer considered by the replicas when determining mes-sage stability.Specification Archetypes Abstractions #Linesload balancer 3 2 79replicated kv 5 6 291Table 6.1: Complexity of the specifications used in the evaluation. Abstrac-tions are counted based on the number of implementation-specific con-cerns that were not included in the model, each expressed as one or mul-tiple mapping macros; #Lines includes lines of Modular PlusCal, exclud-ing comments and blank lines.PGo was able to compile both specifications, generating a function for eacharchetype defined in the models. A main function was manually written for eachsystem that bootstraps the synchronized start protocol described in section 4.1 andprovides concrete implementations for the abstractions used in the models. Bothimplementations use communication channels (section 4.3) to send messages be-49tween processes. Table 6.2 summarizes the output produced by PGo, and the effortrequired to get a running system from the generated code.Specification Generated LOC Manual LOCload balancer 494 85replicated kv 3395 234Table 6.2: Generating a running implementation from the models evaluated.Generated LOC indicates lines of code produced by PGo from thearchetype definitions; Manual LOC counts lines of code manually writ-ten to bootstrap the system. Both numbers exclude comments and blanklines.6.2 Semantic EquivalenceWhile a proof that the systems we generated are semantically equivalent to theModular PlusCal models is beyond the scope of this work, we were interested inhaving higher confidence that the resulting systems meet basic functional require-ments. For this reason, we wrote a set of tests that exercised different aspects ofeach system.For the load balancer, we performed a series of operations with different num-bers of clients and servers, each requesting different files. Concurrency acrossrequests was also tested. At the end of the process, we verified that: every clientreceived a response for the requests it made; the contents of the responses are asexpected (matching the underlying file system); and that each server handled thecorrect number of requests. In all cases, the resulting implementation presentedexpected behavior.The replicated key-value store was tested similarly. We wrote a test genera-tor that produces a sequence of operations to be performed by clients; keys andvalues are combinations of randomly generated bytes of configurable length. Weperformed tests with variable numbers of clients and replicas and also in highlyconcurrent environments where every operation is happening concurrently (in aseparate Go routine). We verified that: every client terminated successfully; andthat the database was consistent and identical on every replica at the end of theprocess. We found the system to behave as expected on every scenario and to be,50to the best of our knowledge, a correct implementation of the model.6.3 Performance ComparisonWe ran performance evaluations of both the load balancing system as well as thereplicated key-value store against handwritten implementations. The manual im-plementation of the load balancer was written by the author with the goal of eval-uating this work. The manual implementation of the key-value store was the bestperforming student implementation of the same system, which was a required as-signment of the graduate course on Distributed Systems at UBC, offered in thewinter term of 2019. Table 6.3 shows the effort required in the manual implemen-tation of both models.Specification LOCload balancer 156replicated kv 406Table 6.3: Effort required to implement both models evaluated in this work,in terms of the number of lines of code involved. Numbers exclude com-ments and blank lines.6.3.1 Experimental SetupAll tests described in this section were performed by deploying all system pro-cesses in the same host; this is to reduce the impact of network latency and jitterin the numbers we aggregate and focus evaluation on overheads added by the PGoruntime. The host machine features an eight-core i7 1.80GHz processor with 16GBof memory and runs Linux 4.20.7. We used Go version 1.10.3. All numbers re-ported in the following graphs are averages of ten executions.6.3.2 ResultsThe load balancer system was run in two different scenarios: single client andmulti-client. In both cases, clients performed multiple requests in sequence andwaited for a response. The load balancer redirects requests to one of three servers.The files requested were randomly selected from a collection of previously down-51Figure 6.1: Execution time for the load balancer system, with one or multipleclients performing 10 (left) or 100 (right) requests per client.Figure 6.2: Time it takes for three clients to perform 100 operations, firstsequentially (left), and then with Go routines (right).loaded web pages from popular websites. In the multi-client scenario, ten clientsmake requests concurrently to the load balancer. Figure 6.1 shows execution timefor the two scenarios for different numbers of requests performed. The systemcompiled by PGo does not scale as nicely as the handwritten implementation dueto the performance penalty incurred by the action restart mechanism described inChapter 3.The replicated key-value store was tested in an environment with two replicasand three clients. Each client performed one hundred randomly generated opera-tions. Keys were set to be 32 bytes long and values 64 bytes long. Clock updateshappened every 100ms. In addition, we tested both sequential and concurrent ex-52ecution within a client: in concurrent mode, every operation runs in a separate Goroutine. Since the Get and Put operations in the replicated key-value store requirea response from the replica, we create a new mailbox whenever a client performsone of these operations. Figure 6.2 illustrates the results obtained in this experi-ment. As can be seen, the system compiled by PGo works correctly even undera highly concurrent environemnt. Although more extensive performance tests areneeded to make conclusive claims, these preliminary results indicate that PGo hasperformance that is comparable to handwritten implementations in most cases butthat may degrade if actions need to be restarted multiple times.53Chapter 7DiscussionIn this chapter, we address limitations of the proposed design and current imple-mentation, and discuss future work.Compilation is not verified. To trust that the specification meets the correctnessproperties and that the implementation refines the specification, the follow-ing need to be trusted: the TLC model checker, the PGo compiler, the Javacompiler and runtime, the Go compiler and runtime, and the operating sys-tem. In addition, the archetype resources passed to the functions generatedby PGo need to be correct implementations of the abstractions used in thespecification. Providing stronger correctness guarantees of the compilationfrom Modular PlusCal to Go remains future work.Fault tolerance. As discussed in section 3.6, there are limited ways to deal withfailures while preserving the execution model followed in this work. How-ever, they require significant effort from the developer, who needs to adaptboth the specification and the implementation. PGo could make the pro-cess easier by providing fault-tolerance models built into the Modular Plus-Cal language: the compiler generates an abstraction of the failure modelto PlusCal, allowing the designer to verify that the system is correct underthat failure model. PGo can also provide implementations of fault-tolerantcomponents that developers can use, matching abstract failure models withresilient implementations the same way that environment abstractions are54matched with concrete implementations in this work. This remains as futurework.Unsupported TLA+ expressions. As described in Chapter 2, TLA+ is a declar-ative specification language. Some expressions are very high level and dif-ficult to translate to a concrete implementation (for example, the CHOOSEoperator that selects an element from a set that satisfies a series of condi-tions). Further work needs to be done to support a larger portion of TLA+.Performance. While systems compiled with PGo have behavior that is defined bythe specification they originated from, performance is an area that still needsfurther work. In particular, the process of aborting and retrying an atomic ac-tion is expensive, as local state needs to be reverted and recomputed. Insteadof restarting an action from scratch, PGo could leave local state unmodi-fied and just attempt to re-acquire all archetype resources used in the action.This, however, assumes that local computation is deterministic, which maynot always be the case.Fairness considerations. PlusCal processes (i.e., instances of Modular PlusCalarchetypes) can be scheduled under unfair, weak, or strong fairness levels(for discussion and definitions, see [26]). Correctness properties written bythe system designer may only hold under a specific fairness assumption. ThePGo compiler and runtime take a best-effort approach to allow actions to bescheduled infinitely often if they remain enabled. However, many schedul-ing decisions are still made by the Go runtime, which is known to favorperformance over fairness. Further work is required to enforce a more strictapproach to matching TLA+ fairness semantics with the way actions arescheduled in the implementation.55Chapter 8Related WorkPGo is closely related to a vast body of previous work that attempted to bring thepower of formal methods to the context of concurrent and distributed systems. Inthis chapter, we review some of the most closely related work previously publishedand how they compare with the approach proposed in this thesis.Proof assistants. Verifying distributed systems by writing proofs is complex, lead-ing researchers to look for ways to make the process more approachable.Verdi [37] enables developers to write proofs about the behavior of dis-tributed protocols assuming a lossless network and provides automated trans-formers that produce a verified distributed system that works under different,more realistic network semantics. IronFleet [17] provides tools that allowdevelopers to prove that realistic implementations refine a high-level speci-fication based on the Dafny language [31]. The verification process supportsboth safety and liveness properties, although in a limited way.The work presented in this thesis differs from this category by relying onmodel checking of specifications rather than formal proofs of correctness.While model checking by state-space exploration does not prove systemsto be correct, it requires significantly less effort from the developer of thesystem. More specifically, PGo enables developers to reason about theirsystem abstractly and have sufficient confidence (but no guarantee) in itscorrectness, while at the same time freeing developers from the arduous task56of writing proofs, a process that is known to require a significant amount ofeffort, expertise and time [22].Domain-Specific Languages and Compilers. DSLs have been extensively usedin the past to provide a higher-level, more expressive way to build distributedsystems. Previous work has demonstrated that generating source code fromsuch alternative representations can be beneficial and is similar to our ap-proach. Mace [20, 21] is a C++ language extension and compiler that gen-erates a distributed system implementation from a state-machine represen-tation. The approach taken by Mace is similar to the one we used in ourwork; however, PGo better supports the evolution of such systems by pro-viding a clear boundary between protocol specification and implementationdetails due to its modular approach. P [4] is a domain-specific language forasynchronous, event-driven programs. It was used successfully to build theUSB stack on Microsoft Windows 8. P and Modular PlusCal share the goalof isolating implementation details that are not relevant for the model be-ing checked. P# [7] is an evolution of that work: it supports modeling andsystematic testing of distributed systems. P# has been used in production atMicrosoft [8]; however, the developer needs to provide both an implemen-tation and an abstract model of the components of the system that are notunder test to avoid state-space explosion.Model Checking Implementations. Previous work has applied the idea of state-space exploration directly to implementations of systems, as opposed to ab-stractions of their behavior. VeriSoft [14] is a model checker for arbitrary Cprograms that uses a stateless exploration algorithm combined with partial-order reduction techniques to reduce the state space. MODIST [16, 38] ex-tends the idea and is able to model check the implementation of distributedsystems. While both of these systems have the advantage of verifying ac-tual implementations, the approach is subject to the state-space explosionproblem. PGo aims to allow model checking to remain efficient while stillproviding many of the advantages that make checking implementations at-tractive by automating the transition from an abstract model to a concreteimplementation.57Chapter 9ConclusionIn this thesis, we have proposed a technique to automatically generate implementa-tions of distributed systems from models of their behavior in the Modular PlusCalspecification language. The process is built on the idea of matching componentsdefined abstractly in a model with concrete implementations that present the samebehavior. We also discussed how to preserve execution semantics of Modular Plus-Cal; in particular, how to provide behavior equivalent to the atomic steps of TLA+while allowing as much concurrency as possible, for performance reasons. Ourevaluation has shown that the current implementation is able to handle complexspecifications and generate implementations that satisfy the correctness propertiespreviously model-checked.We are still working to make PGo a viable option for the development of prac-tical distributed systems. In particular, we hope to provide better support for theconstruction of fault-tolerant systems and to optimize the generated code and exe-cution runtime to have performance closer to that of handwritten implementations.58Bibliography[1] G. Agha. An Overview of Actor Languages. In Proceedings of the 1986SIGPLAN Workshop on Object-oriented Programming, OOPWORK â86,pages 58â67, New York, NY, USA, 1986. ACM. ISBN 0-89791-205-5.doi:10.1145/323779.323743. URLhttp://doi.acm.org/10.1145/323779.323743. â page 42[2] B. Alpern and F. B. Schneider. Recognizing safety and liveness. DistributedComputing, 2(3):117â126, Sep 1987. ISSN 1432-0452.doi:10.1007/BF01782772. URL https://doi.org/10.1007/BF01782772. âpage 6[3] Amazon. Amazon S3 Availability Event, 2008. URLhttps://status.aws.amazon.com/s3-20080720.html. â page 1[4] V. and Gupta, E. Jackson, , and S. a. Rajamani. P: Safe AsynchronousEvent-Driven Programming. Technical report, November 2012. URLhttps://www.microsoft.com/en-us/research/publication/p-safe-asynchronous-event-driven-programming/. â page 57[5] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic Model CheckingWithout BDDs. In Proceedings of the 5th International Conference on Toolsand Algorithms for Construction and Analysis of Systems, TACAS â99,pages 193â207, Berlin, Heidelberg, 1999. Springer-Verlag. ISBN3-540-65703-7. URL http://dl.acm.org/citation.cfm?id=646483.691738. âpage 7[6] T. D. Chandra, R. Griesemer, and J. Redstone. Paxos Made Live: AnEngineering Perspective. In Proceedings of the Twenty-sixth Annual ACMSymposium on Principles of Distributed Computing, PODC â07, pages398â407, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-616-5.doi:10.1145/1281100.1281103. URL59http://doi.acm.org.ezproxy.library.ubc.ca/10.1145/1281100.1281103. âpage 1[7] P. Deligiannis, A. F. Donaldson, J. Ketema, A. Lal, and P. Thomson.Asynchronous Programming, Analysis and Testing with State Machines.SIGPLAN Not., 50(6):154â164, June 2015. ISSN 0362-1340.doi:10.1145/2813885.2737996. URLhttp://doi.acm.org/10.1145/2813885.2737996. â page 57[8] P. Deligiannis, M. McCutchen, P. Thomson, S. Chen, A. F. Donaldson,J. Erickson, C. Huang, A. Lal, R. Mudduluru, S. Qadeer, and W. Schulte.Uncovering Bugs in Distributed Storage Systems During Testing (Not inProduction!). In Proceedings of the 14th Usenix Conference on File andStorage Technologies, FASTâ16, pages 249â262, Berkeley, CA, USA, 2016.USENIX Association. ISBN 978-1-931971-28-7. URLhttp://dl.acm.org/citation.cfm?id=2930583.2930602. â page 57[9] M. Demirbas. TLA+ Specifications of the Consistency Guarantees Providedby Cosmos DB. Microsoft Research talk, Nov. 2018. â page 7[10] C. Flanagan and P. Godefroid. Dynamic Partial-order Reduction for ModelChecking Software. In Proceedings of the 32Nd ACM SIGPLAN-SIGACTSymposium on Principles of Programming Languages, POPL â05, pages110â121, New York, NY, USA, 2005. ACM. ISBN 1-58113-830-X.doi:10.1145/1040305.1040315. URLhttp://doi.acm.org/10.1145/1040305.1040315. â page 7[11] GitHub. October 21 post-incident analysis, 2018. URLhttps://github.blog/2018-10-30-oct21-post-incident-analysis. â page 1[12] GitLab. Postmortem of database outage of January 31, 2017. URLhttps://about.gitlab.com/2017/02/10/postmortem-of-database-outage-of-january-31/. â page 1[13] P. Godefroid. Partial-Order Methods for the Verification of ConcurrentSystems: An Approach to the State-Explosion Problem. Springer-Verlag,Berlin, Heidelberg, 1996. ISBN 3540607617. â page 7[14] P. Godefroid. Model Checking for Programming Languages Using VeriSoft.In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium onPrinciples of Programming Languages, POPL â97, pages 174â186, NewYork, NY, USA, 1997. ACM. ISBN 0-89791-853-3.60doi:10.1145/263699.263717. URLhttp://doi.acm.org/10.1145/263699.263717. â page 57[15] Google. Google Compute Engine Incident 17003, 2018. URLhttps://status.cloud.google.com/incident/compute/17003. â page 1[16] H. Guo, , L. Zhou, G. Hu, J. Yang, and L. Zhang. Practical software modelchecking via dynamic interface reduction. Symposium on OperatingSystems Principles (SOSP), October 2011. URLhttps://www.microsoft.com/en-us/research/publication/practical-software-model-checking-via-dynamic-interface-reduction/. âpage 57[17] C. Hawblitzel, , , J. Lorch, , M. L. Roberts, S. Setty, and B. Zill. IronFleet:Proving Practical Distributed Systems Correct. In Proceedings of the ACMSymposium on Operating Systems Principles (SOSP). ACM - Associationfor Computing Machinery, October 2015. URLhttps://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/. â pages 18, 56[18] C. Hewitt, P. Bishop, and R. Steiger. A Universal Modular ACTORFormalism for Artificial Intelligence. In Proceedings of the 3rdInternational Joint Conference on Artificial Intelligence, IJCAIâ73, pages235â245, San Francisco, CA, USA, 1973. Morgan Kaufmann PublishersInc. URL http://dl.acm.org/citation.cfm?id=1624775.1624804. â page 42[19] E. Jul, H. Levy, N. Hutchinson, and A. Black. Fine-grained Mobility in theEmerald System. ACM Trans. Comput. Syst., 6(1):109â133, Feb. 1988.ISSN 0734-2071. doi:10.1145/35037.42182. URLhttp://doi.acm.org/10.1145/35037.42182. â page 34[20] C. Killian, J. W. Anderson, R. Jhala, and A. Vahdat. Life, Death, and theCritical Transition: Finding Liveness Bugs in Systems Code. In Proceedingsof the 4th USENIX Conference on Networked Systems Design &Implementation, NSDIâ07, pages 18â18, Berkeley, CA, USA, 2007.USENIX Association. URLhttp://dl.acm.org/citation.cfm?id=1973430.1973448. â pages 2, 57[21] C. E. Killian, J. W. Anderson, R. Braud, R. Jhala, and A. M. Vahdat. Mace:Language Support for Building Distributed Systems. SIGPLAN Not., 42(6):179â188, June 2007. ISSN 0362-1340. doi:10.1145/1273442.1250755.URL http://doi.acm.org/10.1145/1273442.1250755. â page 5761[22] 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. InProceedings of the ACM SIGOPS 22Nd Symposium on Operating SystemsPrinciples, SOSP â09, pages 207â220, New York, NY, USA, 2009. ACM.ISBN 978-1-60558-752-3. doi:10.1145/1629575.1629596. URLhttp://doi.acm.org/10.1145/1629575.1629596. â page 57[23] L. Lamport. Proving the Correctness of Multiprocess Programs. IEEETrans. Softw. Eng., 3(2):125â143, Mar. 1977. ISSN 0098-5589.doi:10.1109/TSE.1977.229904. URLhttps://doi.org/10.1109/TSE.1977.229904. â page 6[24] L. Lamport. Time, Clocks, and the Ordering of Events in a DistributedSystem. Commun. ACM, 21(7):558â565, July 1978. ISSN 0001-0782.doi:10.1145/359545.359563. URLhttp://doi.acm.org/10.1145/359545.359563. â page 49[25] L. Lamport. The Temporal Logic of Actions. ACM Trans. Program. Lang.Syst., 16(3):872â923, May 1994. ISSN 0164-0925.doi:10.1145/177492.177726. URLhttp://doi.acm.org/10.1145/177492.177726. â page 7[26] L. Lamport. Specifying Systems: The TLA+ Language and Tools forHardware and Software Engineers. Addison-Wesley Longman PublishingCo., Inc., Boston, MA, USA, 2002. ISBN 032114306X. â pages2, 7, 15, 31, 55[27] 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., January 2009.URL https://www.microsoft.com/en-us/research/publication/pluscal-algorithm-language/. â pages 2, 15[28] 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., January 2009.URL https://www.microsoft.com/en-us/research/publication/pluscal-algorithm-language/. â page 9[29] L. Lamport. A PlusCalâs User Manual. Online material, Aug. 2018. â page1562[30] L. Lamport, R. Shostak, and M. Pease. The Byzantine Generals Problem.ACM Trans. Program. Lang. Syst., 4(3):382â401, July 1982. ISSN0164-0925. doi:10.1145/357172.357176. URLhttp://doi.acm.org/10.1145/357172.357176. â page 27[31] K. R. M. 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 56[32] R. J. Lipton. Reduction: A New Method of Proving Properties of Systems ofProcesses. In Proceedings of the 2Nd ACM SIGACT-SIGPLAN Symposiumon Principles of Programming Languages, POPL â75, pages 78â86, NewYork, NY, USA, 1975. ACM. doi:10.1145/512976.512985. URLhttp://doi.acm.org/10.1145/512976.512985. â page 18[33] B. Liskov. Distributed Programming in Argus. Commun. ACM, 31(3):300â312, Mar. 1988. ISSN 0001-0782. doi:10.1145/42392.42399. URLhttp://doi.acm.org.ezproxy.library.ubc.ca/10.1145/42392.42399. â pages30, 34[34] 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. ISSN 0001-0782. doi:10.1145/2699417.URL http://doi.acm.org/10.1145/2699417. â page 7[35] A. Pnueli. The Temporal Logic of Programs. In Proceedings of the 18thAnnual Symposium on Foundations of Computer Science, SFCS â77, pages46â57, Washington, DC, USA, 1977. IEEE Computer Society.doi:10.1109/SFCS.1977.32. URL https://doi.org/10.1109/SFCS.1977.32.â page 7[36] F. B. Schneider. Implementing Fault-tolerant Services Using the StateMachine Approach: A Tutorial. ACM Comput. Surv., 22(4):299â319, Dec.1990. ISSN 0360-0300. doi:10.1145/98163.98167. URLhttp://doi.acm.org/10.1145/98163.98167. â page 49[37] J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D. Ernst, andT. Anderson. Verdi: A Framework for Implementing and Formally VerifyingDistributed Systems. SIGPLAN Not., 50(6):357â368, June 2015. ISSN0362-1340. doi:10.1145/2813885.2737958. URLhttp://doi.acm.org/10.1145/2813885.2737958. â page 5663[38] J. Yang, , , Z. Xu, , H. Lin, M. Yang, F. Long, L. Zhang, and L. Zhou.MODIST: Transparent Model Checking of Unmodified Distributed Systems.In Proceedings of the 6th Symposium on Networked Systems Design andImplementation (NSDI â09), pages 213â228. USENIX, April 2009. URLhttps://www.microsoft.com/en-us/research/publication/modist-transparent-model-checking-of-unmodified-distributed-systems/. âpage 57[39] B. Zhang. PGo: Corresponding a High-Level Formal Specification with ItsImplementation. SOSP SRC, 2016. â pages 3, 1264
Thesis/Dissertation
eng
Computer Science
Vancouver : University of British Columbia Library
Attribution-NoDerivatives 4.0 International
Graduate
Compiling distributed system specifications into implementations
Text