Science, Faculty of
Computer Science, Department of
DSpace
UBCV
Do, Minh Nhat
Master of Science - MSc
University of British Columbia
As the need for computing resources grows, providers are increasingly relying on distributed systems to render their services. However, distributed systems are hard to design and implement. As an aid for design and implementation, formal verifica- tion has seen a growing interest in industry. For example, Amazon uses Temporal Logic of Actions plus (TLAâº) and PlusCal specification languages and tool chain to formally verify manually created specifications of their web services [8]. Nevertheless, there is currently no tool to automatically establish a correspon- dence between a PlusCal specification with a concrete implementation. Further- more, PlusCal was not designed with modularity in mind, so a large PlusCal spec- ification cannot be decomposed into smaller ones for ease of modification. This thesis proposes an extension to PlusCal, named Modular PlusCal, as well as a compiler, named PGo, which compiles Modular PlusCal and PlusCal specifications into Go programs. Modular PlusCal introduces new constructs, such as archetypes and mapping macros, to provide isolation and, as a result, modularity. By auto- matically compiling PlusCal and Modular PlusCal specifications into distributed system implementations, PGo reduces the burden on programmers trying to ensure the correctness of their distributed systems.
Corresponding formal specificationswith distributed systemsbyMinh Nhat DoB. Eng, Nanyang Technological University, 2014A 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©Minh Nhat Do, 2019The following individuals certify that they have read, and recommend to the Fac-ulty of Graduate and Postdoctoral Studies for acceptance, the thesis entitled:Corresponding formal specificationswith distributed systemssubmitted by Minh Nhat Do in partial fulfillment of the requirements for the de-gree of Master of Science in Computer Science.Examining Committee:Ivan Beschastnikh, Computer ScienceSupervisorWilliam Bowman, Computer ScienceSupervisory Committee MemberiiAbstractAs the need for computing resources grows, providers are increasingly relying ondistributed systems to render their services. However, distributed systems are hardto design and implement. As an aid for design and implementation, formal verifica-tion has seen a growing interest in industry. For example, Amazon uses TemporalLogic of Actions plus (TLA+) and PlusCal specification languages and tool chainto formally verify manually created specifications of their web services [8].Nevertheless, there is currently no tool to automatically establish a correspon-dence between a PlusCal specification with a concrete implementation. Further-more, PlusCal was not designed with modularity in mind, so a large PlusCal spec-ification cannot be decomposed into smaller ones for ease of modification. Thisthesis proposes an extension to PlusCal, named Modular PlusCal, as well as acompiler, named PGo, which compiles Modular PlusCal and PlusCal specificationsinto Go programs. Modular PlusCal introduces new constructs, such as archetypesand mapping macros, to provide isolation and, as a result, modularity. By auto-matically compiling PlusCal and Modular PlusCal specifications into distributedsystem implementations, PGo reduces the burden on programmers trying to ensurethe correctness of their distributed systems.iiiLay SummaryDistributed software systems are notoriously hard to build correctly due to theirsheer scale and complexity. Several approaches have been proposed to ensure thecorrectness of these systems, such as various forms of testing, monitoring, and for-mal verification. In formal verification, the programmer typically has to build thesystem twice, once as a formally verified specification and again as a real imple-mentation.This thesis proposes a compiler to convert a formally verified specification intoa real implementation, easing the burden on programmers.ivPrefaceThe work presented in this thesis was conducted by the author in collaborationwith Finn Hackett, Renato Costa, Brendan Zhang, and Adam Geller, under thesupervision of Dr. Ivan Beschastnikh.The design of Modular PlusCal (Chapter 3) was joint work by Finn Hackett,Renato Costa, and the author. The design and implementation of the parsing passand PGoâs internal representation of (Modular) PlusCal and TLA+ were joint workby Finn Hackett and the author (Section 4.1.1). The design and implementation ofthe configuration parsing pass were joint work by Finn Hackett and Renato Costa(Section 4.2.1). The design and implementation of the macro expansion pass wereperformed by Finn Hackett (Section 4.1.2). The design and implementation of thevalidation pass were performed by Renato Costa (Section 4.1.4). The design andimplementation of the scoping pass were joint work by Finn Hackett and the author(Section 4.1.5). The design and implementation of the Modular PlusCal to Gocode generation were performed by Renato Costa. The design and implementationof the PlusCal/TLA+ to Go code generation were joint work by Finn Hackett andthe author (Section 4.2.4). The design and implementation of the run-time systemwere joint work by Finn Hackett, Renato Costa, and the author. The type inference(Section 4.2.2) and atomicity inference (Section 4.2.3) stages were designed andimplemented by the author.vTable of ContentsAbstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iiiLay Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ivPreface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vTable of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . viList of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . viiiList of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ixGlossary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiAcknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xii1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42.1 TLA+ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42.2 PlusCal algorithm language . . . . . . . . . . . . . . . . . . . . . 53 Modular PlusCal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83.2 Archetypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113.3 Mapping macros . . . . . . . . . . . . . . . . . . . . . . . . . . 123.4 Instances . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14vi4 Compilation with PGo . . . . . . . . . . . . . . . . . . . . . . . . . . 174.1 The Modular PlusCal to PlusCal pipeline . . . . . . . . . . . . . 194.1.1 Parsing . . . . . . . . . . . . . . . . . . . . . . . . . . . 194.1.2 Macro expansion . . . . . . . . . . . . . . . . . . . . . . 244.1.3 Desugaring . . . . . . . . . . . . . . . . . . . . . . . . . 254.1.4 Validation . . . . . . . . . . . . . . . . . . . . . . . . . . 254.1.5 Scoping . . . . . . . . . . . . . . . . . . . . . . . . . . . 264.1.6 Post-scoping validation . . . . . . . . . . . . . . . . . . . 274.1.7 PlusCal code generation . . . . . . . . . . . . . . . . . . 284.2 The PlusCal to Go pipeline . . . . . . . . . . . . . . . . . . . . . 354.2.1 Configuration parsing . . . . . . . . . . . . . . . . . . . 364.2.2 Type inference . . . . . . . . . . . . . . . . . . . . . . . 374.2.3 Atomicity inference . . . . . . . . . . . . . . . . . . . . 414.2.4 Go code generation . . . . . . . . . . . . . . . . . . . . . 415 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 555.1 How effective is the compiled PlusCal output for model checking? 555.2 How complex a specification can PGo compile? . . . . . . . . . . 595.2.1 Walkthrough of the queens specification and its compiledsingle-threaded implementation . . . . . . . . . . . . . . 615.2.2 Walkthrough of round robin specification and its compileddistributed sytem implementation . . . . . . . . . . . . . 686 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 716.1 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 716.2 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 727 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 738 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77viiList of TablesTable 4.1 PGo support for PlusCal constructs . . . . . . . . . . . . . . . 46Table 4.2 PGo support for TLA+ constructs . . . . . . . . . . . . . . . . 52Table 5.1 Model checking results for distributed queue . . . . . . . . . . 57Table 5.2 Model checking results for load balancer . . . . . . . . . . . . 58Table 5.3 Sizes of single-process specifications and their outputs . . . . . 60Table 5.4 Sizes of multi-process specifications and their outputs . . . . . 61viiiList of FiguresFigure 2.1 Eulerâs greatest common denominator algorithm in TLA+ . . . 5Figure 2.2 Eulerâs greatest common denominator algorithm in PlusCal . . 6Figure 2.3 Compiled TLA+ output . . . . . . . . . . . . . . . . . . . . . 7Figure 3.1 Add server and client specification in PlusCal . . . . . . . . . 9Figure 3.2 PlusCal procedures specifying a TCP connection . . . . . . . 10Figure 3.3 PlusCal macros specifying a TCP connection . . . . . . . . . 11Figure 3.4 Grammar for archetypes . . . . . . . . . . . . . . . . . . . . 12Figure 3.5 Specification for add server in Modular PlusCal . . . . . . . . 12Figure 3.6 Grammar for mapping macros . . . . . . . . . . . . . . . . . 13Figure 3.7 Specification for a TCP connection in Modular PlusCal . . . . 14Figure 3.8 Grammar for instances . . . . . . . . . . . . . . . . . . . . . 14Figure 3.9 Examples of Modular PlusCal instances . . . . . . . . . . . . 15Figure 3.10 Add server and client in Modular PlusCal . . . . . . . . . . . 16Figure 4.1 Sharing between Modular PlusCal to Go and PlusCal to Gopipelines in PGo . . . . . . . . . . . . . . . . . . . . . . . . 18Figure 4.2 PGo compiler pipeline from Modular PlusCal to PlusCal . . . 19Figure 4.3 Grammar for simple arithmetic expressions . . . . . . . . . . 20Figure 4.4 Abstract syntax for arithmetic expressions . . . . . . . . . . . 21Figure 4.5 Implementation for ãunitã . . . . . . . . . . . . . . . . . . . 21Figure 4.6 Implementation for ãfactorã and ãexpressionã . . . . . . . . . 23Figure 4.7 A simple macro . . . . . . . . . . . . . . . . . . . . . . . . . 25Figure 4.8 Simple desugaring . . . . . . . . . . . . . . . . . . . . . . . 25ixFigure 4.9 A simple Modular PlusCal specification . . . . . . . . . . . . 29Figure 4.10 Compiled PlusCal output . . . . . . . . . . . . . . . . . . . . 30Figure 4.11 Example local and global temporary variable outputs . . . . . 32Figure 4.12 State spaces of specifications in Figure 4.11 . . . . . . . . . . 33Figure 4.13 PGo compiler pipeline from PlusCal to Go . . . . . . . . . . 35Figure 4.14 PGoâs accepted command line arguments . . . . . . . . . . . 36Figure 4.15 Configuration file for PGo . . . . . . . . . . . . . . . . . . . 36Figure 4.16 PGoâs types . . . . . . . . . . . . . . . . . . . . . . . . . . . 38Figure 4.17 Example pseudocode output of while loop . . . . . . . . . . . 54Figure 5.1 Queens specification . . . . . . . . . . . . . . . . . . . . . . 63Figure 5.2 Compiled queens specification - preamble . . . . . . . . . . . 64Figure 5.3 Compiled queens specification - while condition . . . . . . . 64Figure 5.4 Compiled queens specification - queens, nxtQ, and cols . . . . 65Figure 5.5 Compiled queens specification - exts . . . . . . . . . . . . . 66Figure 5.6 Compiled queens specification - update todo when solutionsare found . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67Figure 5.7 Compiled queens specification - update sols when solutionsare found . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68Figure 5.8 Round robin specification . . . . . . . . . . . . . . . . . . . 69Figure 5.9 Compiled distributed system for round robin specification . . 70xGlossaryAPI application programming interfaceDSL domain-specific languageIR intermediate representationTLA+ Temporal Logic of Actions plus (see http://lamport.azurewebsites.net/tla/high-level-view.html)TLAPS TLA+ Proof SystemTLC Temporal Logic CheckerxiAcknowledgmentsThis research was funded by the Natural Science and Engineering Research Coun-cil of Canada (NSERC) Discovery Grant.I would like to thank my supervisor, Dr. Ivan Bestchasnikh, for his guidancethroughout my master program and his support for my pursuit of academic inter-ests. Iâd like to thank Renato Costa for all the discussions about the project and lifein general that kept me sane. Iâd like to thank Finn Hackett, and Brendan Zhang,who put so much work into the project. Finally, Iâd like to thank my wife, mymom, and NSS lab-mates for their support throughout my program.xiiChapter 1IntroductionDistributed systems are hard to reason about due to the asynchronous interactionsamong their constituent components. An obscure series of interactions among thecomponents may lead to subtle yet catastrophic bugs. For example, Amazonâs Ela-sic Compute Cloud (EC2) hit a rare race condition which caused serious downtimefor the service and took down major sites on the Internet [1].Formal verification is one approach to help programmers ensure correctnessof distributed systems. In formal verification, the programmer has to provide amodel and specification of the system alongside its implementation. A model ofthe system is a tractable representation of the implementation. A specificationconsists of some properties and invariants which formally establish what it meansfor the model to be correct. The specification and model of the system are written ina formal verification language, of which Temporal Logic of Actions plus (TLA+)1is an example. According to TLA+ documentation by Lamport [5, 17], a TLA+specification and model are together referred to as a TLA+ specification, while aTLA+ model is an instance of the specification with all constants instantiated withfinite values. Thus, this thesis follows this convention.Once a TLA+ specification of a system is available, the programmer can use theTemporal Logic Checker (TLC), a model checker bundled in the TLA+ tool box,to check for violations of important system properties. For TLA+ specificationswith very large state spaces, the programmer can run TLC on a group of virtual1https://lamport.azurewebsites.net/tla/tla.html1machines using cloud-based distributed TLC [4] to reduce model checking time.Alternatively, the programmer can use the TLA+ Proof System (TLAPS) [3] to pro-vide proofs of the systemâs correctness.Beside accepting TLA+ specifications as inputs, the TLA+ tool box also supportsspecifications written in the algorithm language PlusCal2. PlusCal is designed asa replacement for pseudocode so its syntax is closer to popular imperative lan-guages than TLA+âs syntax. In addition, PlusCal also has constructs for specifyingnondeterminism and synchronization between asynchronous system components.Specifications written in PlusCal are compiled to TLA+ so they enjoy the same sup-port from the tool box. Thanks to these useful features, PlusCal has been adoptedby large software development companies like Amazon and Microsoft [1, 2].PlusCal allows the programmer to structure the distributed system as a collec-tion of cooperating processes. Within one process, the programmers are free tostructure the single-process computation however they choose. This is in contrastto approaches such as Mace [14, 15], and P# [9], where the specification must bestructured as a state machine, complete with explicit states and state transitions.We discuss more about these languages, and other approaches in Chapter 7.Although PlusCal has many useful features, it suffers from the lack of compos-ability: the programmer cannot reuse concepts defined in one PlusCal specificationin another PlusCal specification. This thesis proposes Modular PlusCal, an exten-sion of PlusCal, to address this problem.With this approach, the programmer essentially has to write the system twice:once as a specification, and again as a real implementation. Beside the duplicationof effort, the real implementation may deviate from the model, violating correct-ness properties which are checked of the specification.To mitigate these shortcomings, this thesis also contributes PGo, a compilerfrom Modular PlusCal, or PlusCal, specifications to distributed Go programs. Byautomating the conversion, PGo removes the duplication of effort and reduces theburden on programmers.In summary, this thesis makes the following two contributions.â¢ Modular PlusCal is an extension of PlusCal with features for composing2https://lamport.azurewebsites.net/tla/high-level-view.html2specifications (Chapter 3).â¢ PGo is a compiler from a Modular PlusCal or PlusCal specification to adistributed Go program (Chapter 4).3Chapter 2BackgroundThis chapter is an overview of TLA+, PlusCal, and the TLA+ tool box.2.1 TLA+TLA+ is a formal specification language, designed for verification of concurrentsystems. A TLA+ specification is composed of expressions and operators with theoccasional constant/variable declarations and module extension. Figure 2.1 showsa specification of Eulerâs greatest common denominator algorithm in TLA+.A TLA+ specification starts with the name of the module, surrounded by dashes(line 1 of Figure 2.1). The TLA+ standard library includes some built-in modules,of which Integers is one. Integers includes the definitions of the less-than (<) andminus (-) operators. EXTENDS Integers (line 2 of Figure 2.1) pulls these definitionsinto scope. CONSTANTS declares constants to be used in the specification, which haveto be specified when model checking. VARIABLES, as the name suggests, declaresvariables to be used in the following expressions or declarations. Nullary operatordeclaration (line 8, 11, and 20 of Figure 2.1) starts with the operator name, followedby double equals (==), and ends with the body of the operator, which is a TLA+expression. A TLA+ conjunction can be written either as an infix operator, e.g.TRUE / TRUE, or as a prefix operator, as shown on lines 8 to 18 of Figure 2.1.When written as prefix operators, they have to align at the same column in the text.The same rules apply for disjunctions (/).41 ----------- MODULE GCD -----------2 EXTENDS Integers34 CONSTANTS N, M56 VARIABLES n, m78 Init == / n = N9 / m = M1011 Next == / / n < m12 / mâ = m - n13 / nâ = n14 / / m < n15 / nâ = n - m16 / mâ = m17 / / nâ = n18 / mâ = m1920 Spec == Init / [][Next]_<<n, m>>21 ==================================Figure 2.1: Eulerâs greatest common denominator algorithm in TLA+Init, Next, and Spec are default names for predicates that constitute a specifi-cation in TLA+. The initial predicate, called Init in Figure 2.1, sets the variablesto their initial values. The next-state relation, called Next in Figure 2.1, relates thecurrent value of a variable with its next value, for all variables, by putting an equal-ity constraint on the variable, e.g., n, and its primed version, nâ. Finally, Spec is aconjunction of the initial predicate Init and the next-state relation Next. The syntax[][Next]_<<n, m>> says that each state transition is either described by Next or thevalues of n and m are unchanged. Spec sets up the state space of the specfication,which can be thought of as a (possibly infinite) directed graph of states, consistingof variable-value pairs, reachable from the initial state.For the detailed grammar of TLA+, see Lamportâs Specifying Systems book [16].2.2 PlusCal algorithm languageThe PlusCal algorithm language is a pseudocode-like language whose goal is tolower the learning curve for using the TLA+ tool box. Figure 2.2 shows a PlusCalspecification for Eulerâs greatest common denominator algorithm. As seen in Fig-ure 2.2, PlusCalâs syntax resembles those of imperative programming languages.51 ----- MODULE GCDPlusCal -----2 EXTENDS Integers34 CONSTANTS N, M56 (*7 --algorithm GCDPlusCal {8 variables n = N, m = M;9 {10 l:11 while (TRUE) {12 if (n < m) {13 m := m - n;14 } else if (m < n) {15 n := n - m;16 }17 }18 }19 }20 *)21 =============================Figure 2.2: Eulerâs greatest common denominator algorithm in PlusCalA PlusCal specification is written in an algorithm block inside a TLA+ com-ment, denoted using (* ... *). All PlusCal statements beside declarations mustbe part of a label. In Figure 2.2, the specification consists of a single infinite whileloop inside the label l. Statements within one label are executed atomically, i.e.,either they all succeed or the label is not executed at all.PlusCal has support for familiar constructs such as if statements, while state-ments, local binding via with blocks, as well as procedures and macros. Proceduresin PlusCal can take a number of arguments, can have their own local variables, andcan modify global variables, but have no return value. Macros in PlusCal have thesame textual expansion behavior as C pre-processing macros.To use a PlusCal specification for model checking, the programmer must com-pile it to TLA+ using the TLA+ tool box. Figure 2.3 shows the output of compilingthe PlusCal specification in Figure 2.2 to TLA+. Except for the slight syntacticdifference, the compiled output in Figure 2.3 is equivalent to the specification inFigure 2.1.For the detailed grammar of PlusCal, see Lamportâs manual1.1https://lamport.azurewebsites.net/tla/c-manual.pdf61 VARIABLES n, m23 vars == << n, m >>45 Init == (* Global variables *)6 / n = N7 / m = M89 Next == IF n < m10 THEN / mâ = m - n11 / nâ = n12 ELSE / IF m < n13 THEN / nâ = n - m14 ELSE / TRUE15 / nâ = n16 / mâ = m1718 Spec == Init / [][Next]_varsFigure 2.3: Compiled TLA+ output7Chapter 3Modular PlusCalThis chapter describes Modular PlusCal, an extension of PlusCal, which providesmodularity and isolation between system specification and environment specifica-tion.3.1 MotivationConsider a simple specification for a server and client in Figure 3.1. The specifica-tion describes simple interactions between an add server and a client, over a TCPconnection. The server waits for the client to send two numbers over the networkconnection and sends back the sum of those two numbers to the client. The client,on the other hand, sends two numbers to the server, gets the result from the server,and prints the result.There are two problems with the specification. Firstly, there is code duplica-tion. The code blocks labeled readA, readB, and readResult differ only in the vari-able being assigned to, a, b, and result, respectively. Similarly, the code blockslabeled writeResult, writeA, and writeB share a lot in common. Secondly, thereis no clear separation between system functionality specification and environmentspecification. The main functionality of the system, namely adding numbers on theserver and printing results on the client, is mixed with the specification of the TCPconnection between the client and the server, which is part of the environment.81 ----------------- MODULE AddServerClientPlusCal -----------------2 EXTENDS Integers, Sequences, TLC34 CONSTANTS A, B, BufferSize, ClientId, ServerId56 (*7 --algorithm AddServerClientPlusCal {8 variables network = [i in {ServerId, ClientId} |-> <<>>];910 process (S = ServerId)11 variables a, b;12 {13 ls:14 while (TRUE) {15 readA:16 await Len(network[self]) > 0;17 a := Head(network[self]);18 network[ServerId] := Tail(network[self]);19 readB:20 await Len(network[self]) > 0;21 b := Head(network[self]);22 network[ServerId] := Tail(network[self]);23 writeResult:24 await Len(network[ClientId]) < BufferSize;25 network[ClientId] := Append(network[ClientId], a + b);26 }27 }2829 process (C = ClientId)30 variables result;31 {32 lc:33 while (TRUE) {34 writeA:35 await Len(network[ServerId]) < BufferSize;36 network[ServerId] := Append(network[ServerId], A);37 writeB:38 await Len(network[ServerId]) < BufferSize;39 network[ServerId] := Append(network[ServerId], B);40 readResult:41 await Len(network[self]) > 0;42 result := Head(network[self]);43 network[self] := Tail(network[self]);44 printResult:45 print result;46 }47 }48 }49 *)50 =================================================================Figure 3.1: Add server and client specification in PlusCal91 * global variables2 variables network = [i in {ServerId, ClientId} |-> <<>>],3 serverPkt, clientPkt;45 procedure TCPRead(which)6 {7 lr:8 await Len(network[which]) > 0;9 if (which = ServerId) {10 * TCP read for server11 serverPkt := Head(network[which]);12 } else {13 * TCP read for client14 clientPkt := Head(network[which]);15 }16 network[which] := Tail(network[which]);17 }1819 procedure TCPWrite(which, pkt)20 {21 lw:22 await Len(network[which]) < BufferSize;23 network[which] := Append(network[which], pkt);24 }Figure 3.2: PlusCal procedures specifying a TCP connectionThe two PlusCal syntactical constructs that are offered as solutions for reuseare procedures and macros. However, they cannot effectively address the aboveproblems.PlusCal procedures can modify global variables, so they can modify the networkglobal variable but cannot return the packet read from the network without in-troducing a new global variable to store it (as shown in Figure 3.2). To use theprocedure TCPRead, the programmer has to introduce two new global variables,namely serverPkt and clientPkt. Furthermore, the definition of TCPRead containsthe knowledge that there are only two processes interacting with each other. This isnot desirable because it reduces reusability of the specification as well as the com-piled output of PGo. For example, this procedure cannot be used in a specificationwhere there are more than two kinds of processes interacting with each other.PlusCal macros, on the other hand, do not require new global variables, buthave implicit behaviors, which are non-obvious (as shown in Figure 3.3). Forexample, after the macro call TCPRead(ServerId, a), the value read from the TCPconnection is stored in a, but this fact is hidden in the TCPRead definition. Both the101 macro TCPRead(which, pkt)2 {3 await Len(network[which]) > 0;4 pkt := Head(network[which]);5 network[which] := Tail(network[which]);6 }78 macro TCPWrite(which, pkt)9 {10 await Len(network[which]) < BufferSize;11 network[which] := Append(network[which], pkt);12 }Figure 3.3: PlusCal macros specifying a TCP connectionprogrammer and the compiler have to tease this fact out from its definition, whichsignificantly hinders comprehension and compilation.To cleanly address the problems of reuse and modularity, this thesis introducesModular PlusCal, which extends PlusCal by adding archetypes (Section 3.2), in-stances (Section 3.4), and mapping macros (Section 3.3).3.2 ArchetypesA PlusCal process is a unit of execution. Each process can define local variables,and can make modifications to global variables.A Modular PlusCal archetype is a blueprint for a process, or a group of pro-cesses. Unlike processes, they can only access global variables which are passedin as arguments. In addition, they can only interact with their arguments through awell-defined interface. Archetypes are used for specifying system behaviors. Therestrictions imposed on archetypes provide the desired isolation between systemspecification and environment specification. Figure 3.4 shows the grammar forarchetypes.Besides the inability to access global variables, archetypes have the same se-mantics as processes. They can declare their own local variables, which behaveidentically to local variables in PlusCal processes. Labeled blocks in their bodiesare also executed atomically. They have the same labeling restrictions (see Sec-tion 4.1.4) in their bodies.Figure 3.5 shows the specification of the add server as an archetype in Modular11ãarchetypeã |= archetype ãidentifierã(ãparameter-listã)ãlocal-variablesããbodyããparameter-listã |= ε | ãparameterã | ãparameterã,ãparameter-listããparameterã |= ãidentifierã | ref ãidentiferããlocal-variablesã |= ε | variables ãdeclaration-listã;ãdeclaration-listã |= ãvariable-declarationã | ãvariable-declarationã,ãdeclaration-listããbodyã |= {ãlabeled-statement-listã}Figure 3.4: Grammar for archetypes1 archetype AddServer(ref network)2 variables a, b;3 {4 ls:5 while (TRUE) {6 readA:7 a := network[self];8 readB:9 b := network[self];10 writeResult:11 network[ClientId] := a + b;12 }13 }Figure 3.5: Specification for add server in Modular PlusCalPlusCal. The ref keyword in ref network means that network may be modified inthe archetype body, i.e., it may be assigned to in the body. It may seem that a isalways assigned to the value of network[self], as shown on line 7; however, a isactually assigned to whatever value is pulled out of the environment modeled bythe archetype argument network. In this case, a is a number read from a networkconnection. Similarly, line 11 actually specifies that the sum a + b is sent to theclient via the network.3.3 Mapping macrosMapping macros complement of archetypes by specifying the environment. Map-ping macros define both the interface, which consists of reading and writing, andthe model checking behaviors used to model the environment. A mapping macro12ãmapping-macroã |= mapping macro ãidentifierã{read ãmacro-bodyã write ãmacro-bodyã}ãmacro-bodyã |= {ãstatement-listã}Figure 3.6: Grammar for mapping macroshas two parts, one for reading (captured in the read block), and the other for writ-ing (captured in the write block). Just like the body of a PlusCal macro, the readand write blocks of a mapping macro cannot contain any labels. In other words, thestatements in each block can only be a part of an atomic step in a specification. Theprogrammer must keep this in mind to write code that accurately models the envi-ronment. Specifically, each block should not perform too much work. Figure 3.6shows the grammar for mapping macros.The read block of a mapping macro specifies how to pull a value out of theenvironment. Inside a read block of a mapping macro, the programmer can usethe $variable special variable to refer to the global variable being used to storestate for modeling a part of the environment. The write block of a mapping macrospecifies how to incorporate some value into the global environment. Inside awrite block, in addition to the $variable special variable, the programmer alsohave access to the $value special variable to refer to the value being incorporatedinto the environmentâs state. Finally, in both read and write blocks, the programmeruses a yield statement to specify either what value is pulled out of the environment(for a read operation) or to what value the environment modeling state is updated(for a write operation).Figure 3.7 shows how a TCP connection can be modeled with a mappingmacro. In this case, the global variable used to model a TCP connection shouldbe initialized as a TLA+ sequence. The read block specifies that a read operationperformed on a TCP connection blocks until a packet has arrived (using the Plus-Cal await statement). A packet is then extracted from the connection and returnedto the calling code using the with statement and the yield statement, respectively.The write block specifies that a write operation blocks until there is enough bufferto hold the packet. The packet is then sent by Appending it to the connection.131 mapping macro TCPConnection {2 read {3 await Len($variable) > 0;4 with (msg = Head($variable)) {5 $variable := Tail($variable);6 yield msg;7 }8 }9 write {10 await Len($variable) < BufferSize;11 yield Append($variable, $value);12 }13 }Figure 3.7: Specification for a TCP connection in Modular PlusCalãinstanceã |= process (ãvariable-declarationã) == ãarchetype-instantiationããarchetype-instantiationã |= instance ãidentifierã(ãargument-listã)ãmapping-clause-listããargument-listã |= ε | ãargumentã | ãargumentã,ãargument-listããargumentã |= ãexpressionã | ref ãidentifierããmapping-clause-listã |= ε | ãmapping-clauseã | ãmapping-clauseããmapping-clause-listããmapping-clauseã |= mapping ãmapped-variableã via ãidentifierããmapped-variableã |= @ãintegerã | ãidentifierãFigure 3.8: Grammar for instances3.4 InstancesSince the system specification is modeled using archetypes and the environmentspecification is modeled using mapping macros, the programmer can develop themindependently, allowing for higher level of reuse. For verification purposes, thesystem specification has to be composed with the environment specification. In-stances are the compositional glue relating the two halves. Figure 3.8 shows thegrammar for instances.An instance statement instantiates a process or a group of processes using thespecified archetype. Any ref parameter must be instantiated with a ref globalvariable, indicating that the global variable may be modified in the body of thearchetype with an assignment, or an expression, indicating that the argument is141 process (S = ServerId) == instance AddServer(ref conns)2 mapping conns[_] via TCPConnection;34 process (C = ClientId) == instance AddClient(ref conns)5 mapping conns[_] via TCPConnection;Figure 3.9: Examples of Modular PlusCal instanceslocal to the archetype. All non-ref parameters must not be instantiated with aref global variable. Each argument may also be mapped by a mapping macro,indicating that any read and write operation to the argument must be expandedwith the corresponding read or write block of the mapping macro.In Figure 3.9, process S is instantiated by the AddServer archetype, while pro-cess C is instanticated by the AddClient archetype. Their network parameters areinstantiated with the global variable conns, which is also macro-mapped via theTCPConnection mapping macro. The [_] notation following conns indicates thatread and write operations to elements of conns are expanded with the correspond-ing read and write blocks of the TCPConnection mapping macro; and conns is said tobe function-mapped. A mapping clause without a [_] notation is called variable-mapped; and read and write operations are expanded using the variable directly.Figure 3.10 shows a specification of an add server and client in Modular Plus-Cal which is equivalent to the PlusCal specification in Figure 3.1. Having writtenthe specification this way, the programmer can easily swap the TCPConnection map-ping macro for a different UDPConnection mapping macro. Furthermore, TCPConnectioncan be reused in other specifications to model the network.151 -------------- MODULE AddServerClientModularPlusCal --------------2 EXTENDS Integers, Sequences, TLC34 CONSTANTS A, B, BufferSize, ClientId, ServerId56 (*7 --mpcal AddServerClientModularPlusCal {8 variables conns = [i in {ServerId, ClientId} |-> <<>>];910 mapping macro TCPConnection {11 read {12 await Len($variable) > 0;13 with (msg = Head($variable)) {14 $variable := Tail($variable);15 yield msg;16 }17 }18 write {19 await Len($variable) < BufferSize;20 yield Append($variable, $value);21 }22 }2324 archetype AddServer(ref network)25 variables a, b;26 {27 ls:28 while (TRUE) {29 readA:30 a := network[self];31 readB:32 b := network[self];33 writeResult:34 network[ClientId] := a + b;35 }36 }3738 archetype AddClient(ref network)39 variables result;40 {41 lc:42 while (TRUE) {43 writeA:44 network[ServerId] := A;45 writeB:46 network[ServerId] := B;47 readResult:48 result := network[self];49 printResult:50 print result;51 }52 }5354 process (S = ServerId) == instance AddServer(ref conns)55 mapping conns[_] via TCPConnection;5657 process (C = ClientId) == instance AddClient(ref conns)58 mapping conns[_] via TCPConnection;59 }60 *)61 ==================================================================Figure 3.10: Add server and client in Modular PlusCal16Chapter 4Compilation with PGoIn this chapter, we explain the internals of PGo, primarily to document the currentstate and design of the compiler.There are three pipelines in PGoâs architecture, namely Modular PlusCal toPlusCal (Figure 4.2), PlusCal to Go (Figure 4.13), and Modular PlusCal to Go.This thesis describes the first two pipelines.Since compilation from Modular PlusCal to PlusCal expands all accesses ofarchetype parameters using mapping macros, the clear boundary between systemspecification and environment specification is erased. Therefore, it is not appro-priate to compile a Modular PlusCal to PlusCal, and then compiling the resultingPlusCal to Go. Instead, PGo compiles Modular PlusCal specifications directly toGo. However, the compilation from Modular PlusCal to Go is not described in thisthesis.Figure 4.1 shows which stages are shared between the Modular PlusCal to Goand PlusCal to Go pipelines, from parsing to type inference. In addition, config-uration parsing and validation are also shared. Only atomicity inference and codegeneration are distinct for each pipeline.17Parsing(Section 4.1.1)Macro expansion(Section 4.1.2)Validation(Section 4.1.4)Scoping(Section 4.1.5)Post-scoping validation(Section 4.1.6)Type inference(Section 4.2.2)Modular PlusCalatomicity inferenceModular PlusCal to Gocode generationPlusCalatomicity inference(Section 4.2.3)PlusCal to Gocode generation(Section 4.2.4)Figure 4.1: Sharing between Modular PlusCal to Go and PlusCal to Gopipelines in PGoPGo relies on the TLA+ tool box for specification verification. Since TLC onlyaccepts TLA+ specifications as input, a Modular PlusCal specification has to becompiled to TLA+ for verification. PGo accomplishes this by compiling the Mod-ular PlusCal specification to PlusCal, and then relies on the TLA+ tool box forcompilation from the resulting PlusCal to TLA+. This pipeline is described next.18Modular PlusCal specificationParsing(Section 4.1.1)Macro expansion(Section 4.1.2)Desugaring(Section 4.1.3)Validation(Section 4.1.4)Scoping(Section 4.1.5)Post-scoping validation(Section 4.1.6)PlusCal code generation(Section 4.1.7)PlusCal specificationFigure 4.2: PGo compiler pipeline from Modular PlusCal to PlusCal4.1 The Modular PlusCal to PlusCal pipeline4.1.1 ParsingPGo has a rich library for constructing and consuming grammars. It is developedby necessity due to the complexity of the TLA+ and PlusCal grammars: oper-ators have precedence ranges and PlusCal has C and P-syntaxes. Since PGoâsGrammar objects are constructed in ordinary Java code, complicated constructs such19ãexpressionã |= ãfactorã | ãexpressionã+ãfactorã | ãexpressionã-ãfactorããfactorã |= ãunitã | ãfactorã*ãunitã | ãfactorã/ãunitããunitã |= ãnumberã | (ãexpressionã)Figure 4.3: Grammar for simple arithmetic expressionsas precedence ranges for TLA+ operators can be handled outside of the grammaralgorithmically in plain Java, greatly reducing grammar development effort.Grammar constructionPGoâs parser facility provides an application programming interface (API) for piece-meal construction of grammars. The API supports string matching, regular expres-sion pattern matching, alternative choice, and mapping. To showcase how to writedown a grammar using this API, we will implement a simple arithmetic expressiongrammar whose grammar is shown in Figure 4.3. Note that this grammar is usedonly for illustration and is not part of the TLA+ grammar.The arithmetic expression grammar in Figure 4.3 supports four operators, namelyaddition, subtraction, multiplication, and division. Addition and subtraction havethe same precedence, which is lower than the precedence of multiplication anddivision. Multiplication and division has the same precedence. The precedenceof operators is encoded into the grammar as the productions of ãexpressionã andãfactorã, which makes multiplication and division bind more tightly than additionand subtraction. All operators are left associative, which is encoded as left recur-sion in the grammar.Figure 4.4 shows the abstract syntax for the arithmetic expressions. The ab-stract syntax consists of binary operations and numbers, both of which are sub-classes of expressions. Since PGoâs parser also provides source location informa-tion for parsed result, all abstract syntax classes must subclass SourceLocatable(line 1).Figure 4.5 shows how the ãunitã production can be implemented using facil-ities provided by PGoâs parsing utility. A unit is either a number or a parenthe-201 abstract class Expression extends SourceLocatable {}23 class BinOp extends Expression {4 enum Operator {5 Add,6 Sub,7 Mul,8 Div,9 }10 final Operator operator;11 final Expression lhs;12 final Expression rhs;13 BinOp(Operator operator, Expression lhs, Expression rhs) {14 this.operator = operator;15 this.lhs = lhs;16 this.rhs = rhs;17 }18 }1920 class Number extends Expression {21 final int value;22 Number(int value) {23 this.value = value;24 }25 }Figure 4.4: Abstract syntax for arithmetic expressions1 static Grammar<Expression> number =2 matchPattern(Pattern.compile("[1-9][0-9]*"))3 .map(m -> new Number(Integer.parseInt(m.getValue().group())));45 static ReferenceGrammar<Expression> expression = new ReferenceGrammar<>();67 static Grammar<Expression> unit =8 parseOneOf(9 number,10 emptySequence()11 .drop(matchString("("))12 .part(expression)13 .drop(matchString(")"))14 .map(seq -> seq.getValue().getFirst()));Figure 4.5: Implementation for ãunitã21sized expression, so the grammar for it is constructed with a choice grammar usingparseOneOf() (line 8). The grammar for numbers is implemented by a regular ex-pression matcher with pattern [1-9][0-9]*, which says that a number is a seriesof digits not starting with 0 (line 2). The matched string is then converted to aNumber object using the map() transformer on the grammar (line 3). In the case ofparenthesized expressions, the grammar must match a sequence of tokens, namelythe open parenthesis token ((), a series of tokens for expressions, and the closeparenthesis token ()). A sequence grammar starts with an empty sequence (line10), and then is built upon using various sequence constructing methods such aspart() (line 12) and drop() (lines 10 and 12), each accepting a grammar. A dropsequence grammar tells the parser to parse the grammar but drops the result. Anyfailure while parsing a dropped constituent grammar still results in a parse failureoverall. Drop sequence grammars are useful in cases where tokens in the input textdetermine the structure of the resulting abstract syntax tree, but not the nodes in it,or cases where the token does not have a representation in the abstract syntax. Theresult of a sequence grammar is a heterogeneous list, where each node has its owntype. Hence, a map() transformation is needed to extract the parsed expression (line14). Finally, a reference grammar (line 5) acts as a pre-declaration, which allowsfor self-referential (e.g., the definitions of ãfactorã and ãexpressionã) or mutuallyrecursive grammars (e.g., the definitions of ãunitã and ãexpressionã).Figure 4.6 shows how the ãfactorã and ãexpressionã productions can be imple-mented. Since ãfactorã is self-referential, it is declared as a reference grammar.Since ãexpressionã is both self-referential and mutually recursive (with ãunitã), itis also declared as a reference grammar. Lines 24 to 26 and 47 to 49 in Figure 4.6shows how each nodes in the resulting heterogeneous list can be accessed. Thenodes are in the reverse order of construction. A Located object is a simple stand-in for cases where a temporary result of a constituent part of a grammar is needed.In the case of ãfactorã, the operator may be a multiplication or a division, rep-resented as enum values, which cannot be a subclass of SourceLocatable (a Javarestriction). Hence, it is saved into a Located object.221 static ReferenceGrammar<Expression> factor = new ReferenceGrammar<>();23 static {4 factor.setReferencedGrammar(5 parseOneOf(6 unit,7 emptySequence()8 .part(factor)9 .part(parseOneOf(10 emptySequence()11 .part(matchString("*"))12 .map(seq ->13 new Located<>(14 seq.getLocation(),15 BinOp.Operator.Mul)),16 emptySequence()17 .part(matchString("/"))18 .map(seq ->19 new Located<>(20 seq.getLocation(),21 BinOp.Operator.Div))))22 .part(unit)23 .map(seq -> new BinOp(24 seq.getValue().getRest().getFirst().getValue(),25 seq.getValue().getRest().getRest().getFirst(),26 seq.getValue().getFirst()))));2728 expression.setReferencedGrammar(29 parseOneOf(30 factor,31 emptySequence()32 .part(expression)33 .part(parseOneOf(34 emptySequence()35 .part(matchString("+"))36 .map(seq ->37 new Located<>(38 seq.getLocation(),39 BinOp.Operator.Add)),40 emptySequence()41 .part(matchString("-"))42 .map(seq -> new Located<>(43 seq.getLocation(),44 BinOp.Operator.Sub))))45 .part(factor)46 .map(seq -> new BinOp(47 seq.getValue().getRest().getFirst().getValue(),48 seq.getValue().getRest().getRest().getFirst(),49 seq.getValue().getFirst()))));50 }Figure 4.6: Implementation for ãfactorã and ãexpressionã23PGoâs parserPGoâs parser is a recursive descent parser with backtracking and memoization. Itconsumes Grammar objects defined by the programmer, together with a string input,and produces all possible abstract syntax trees resulting from that grammar.Since TLA+ has many constructs with the same prefix, e.g., a tuple <<e>>, anda required action, <<e1>>_e2, memoization is heavily employed to keep parsingtime manageable. The parser relies on the programmer to annotate which grammarshould be memoized via a memoize() call, which creates a memoized grammar fromany grammar. The memoization key is the identity of the memoized grammar andthe state of the parser when it encounters that grammar. Upon the first encounter,the parser proceeds normally with the inner grammar and the result is saved intoa memoization table. When there is a parse failure and the memoized grammar isretried, the memoized result is used instead of reparsing.Internal representationPGo has separate abstract syntax classes for TLA+, PlusCal, and Modular PlusCalconstructs. Each abstract syntax node has its own unique identifier, which is usedas keys in constructed tables of information regarding that node. This means thattheir classes need not be modified to add fields for new pieces of information aboutthe objects, which reduces churn in the code base. The class DefinitionRegistryin the code base acts as a centralized database for all tables of information aboutnodes in the abstract syntax tree.The design of the abstract syntax classes follows the visitor pattern, whichallows addition of operations on the classes without modification to them, furtherreducing churn.4.1.2 Macro expansionMacros in PlusCal and Modular PlusCal are named code fragments. They areexpanded structurally during compilation. As such, they do not suffer from pitfallsof textual expansion, such operator precedence problems, which is demonstratednext. A call such as Macro(c, 1 + 2), whose definition is shown in Figure 4.7,is expanded correctly to c := (1 + 2) * 2 by PGo. This is in contrast to textual241 macro Macro(a, b) {2 a := b * 2;3 }Figure 4.7: A simple macro1 lb: while (f(a)) {2 body3 };4 stmt1 lb: if (f(a)) {2 body3 goto lb;4 } else {5 stmt6 };Figure 4.8: Simple desugaringmacro expansion, where the same call is expanded incorrectly to c := 1 + 2 * 2.There are restrictions on macros such as macros must not be recursive or mu-tually recursive, and their bodies must not contain any labels.4.1.3 DesugaringSince a PlusCal while loop must appear at the start of a labeled code block, a whileloop in Modular PlusCal are desugared into an if and a goto. This is necessary dueto the possibility that the condition of the while loop may contain an archetype pa-rameter read, which may be expanded in the code generation stage (Section 4.1.7)to multiple statements. Figure 4.8 shows how this translation is performed in thesimplest case. Note that desugaring is only performed in the Modular PlusCal toPlusCal pipeline.However, blindly inserting a goto may result in invalid code since control flowmay have terminated before the inserted goto. For example, the last statement of awhile loop may be a goto statement. Inserting a new goto after that goto results indead code, which is forbidden by the TLA+ tool box. Therefore, desugaring has toinsert goto strategically based on control flow.4.1.4 ValidationThe validation stage checks the input specificationâs compliance with labeling rules.Modular PlusCal inherits all labeling rules from PlusCal. These rules dictate where25a label must, must not, and may be present. Below are some example labeling rules.â¢ The first statement in the body of a process, a procedure, or a uniprocessalgorithm must be labeled.â¢ A while statement must be labeled.â¢ A statement S in a statement sequence must be labeled if it is preceded inthat sequence by any of the following:â A call statement, if S is not a return or a goto.â A return statement.â A goto statement.â An if or either statement that contains a labeled statement, a goto, acall, or a return anywhere within it.â¢ A macro body and a with body cannot contain any labeled statements.â¢ In any control path, a label must come between an assignment to a variablex and any other statement that assigns a value to x. A local variable or pa-rameter of a procedure P is set by a call P(...) or return statement in P.The above rules are taken from section 3.7 of the PlusCalâs manual1.4.1.5 ScopingModular PlusCal, and PlusCal have static scoping, i.e., identifiers must be declaredbefore use. TLA+, on the other hand, does not allow redefinition of an identifier, sothe problem of scoping becomes moot for the language.The scoping stage builds a table matching uses of an identifier to its declara-tion. It does so using one ChainMap per lexical scope. A ChainMap has mappingsfrom variable names to variable declarations, and a parent map. To find a variabledeclaration, it first looks up the variable name in its own mappings. If the name isnot found, the ChainMap delegates the lookup to its parent map.1https://lamport.azurewebsites.net/tla/c-manual.pdf26In addition, the scoping stage also loads additional modules as instructed byTLA+ EXTENDS and INSTANCE statements in the specification. An EXTENDS statementpulls all definitions in a TLA+ module into scope. An INSTANCE statement pulls alldefinitions in a TLA+ module into scope, and also replaces some constant defini-tions with user-provided values.Beside normal variables, which are declared before use, there are some specialvariables which are implicitly declared. For example, each process and archetypebody has an implicit self variable, which refers to the process identifier of theprocess or archetype, is immutable, and is in scope for the whole body. A pro-cedure also has an implicit self variable which refers to the calling process orarchetypeâs identifier; however, PGo does not support this at the moment but onlysupports procedures which do not use self. Other special variables are $variableand $value. The $variable special variable is available in both read and writeblocks of a mapping macro and it refers to the name of the variable being mapped(see Section 4.1.7). The $value special variable is available only in the write blockof a mapping macro and it refers to the value being assigned to the mapped variable(see Section 4.1.7).4.1.6 Post-scoping validationIn addition to the labeling rules, Modular PlusCal also imposes some restrictionswhich are checked in the post-scoping validation stage. Below are the restrictionschecked in this stage.â¢ Only ref parameters or local variables can be assigned to inside an archetypebody.â¢ Parameters which are function-mapped can only be used as functions (asopposed to being used as variables).â¢ Parameters which are variable-mapped can only be used as variables (as op-posed to being used as functions).â¢ A variable can only be mapped once in a Modular PlusCal instance state-ment.27â¢ Parameters must be mapped consistently across different instances of thesame archetype, i.e., a parameter of an archetype cannot be function-mappedin one instance but variable-mapped in another instance.These restrictions ensure that the Modular PlusCal to Go code generation stage(not described in this thesis) can generate meaningful code.4.1.7 PlusCal code generationA Modular PlusCal specification is compiled into a PlusCal specification by remov-ing the mapping macros, the archetypes, and compiling instances into processes.An instance is compiled into a process, or a group of processes, by expanding readsand writes to archetype parameters with their corresponding mapping macro readand write blocks. In other words, archetype definitions are inlined and mappingmacros are expanded for instances.For example, consider the specification in Figure 4.9. The archetype A writes0 to the network (line 29), modeled as conn, reads from the network into a localvariable r (line 30), and if r is positive (line 31), writes r + 1 into its database atkey "k" (line 32), and finally, prints out the value associated with the key "k" in itsdatabase (line 34). It does all of the above in one atomic step labeled l. A singleprocess P (line 39), assigned an identifier of 0 (which is the value of self within itsbody), is instantiated from archetype A, with a TCP connection (lines 39 and 40),and a local database initialized to have the key "k" maps to 0 (lines 39 and 41).Figure 4.10 shows the compiled PlusCal output for this specification with addedcomments for clarity.As seen in Figure 4.10, read and write expansions use temporary variables.Any write to network is saved into a temporary variable (e.g., connWrite on line11 and connWrite0 on line 16) because PlusCal only permits one modification pervariable in a label. Any read from network is also saved into a temporary variable(e.g., connRead on line 17) to maintain a small code size. If there are multiple labels,the temporary variables are reused in each label.281 --mpcal Spec {2 mapping macro TCPConnection {3 read {4 await Len($variable) > 0;5 with (msg = Head($variable)) {6 $variable := Tail($variable);7 yield msg;8 }9 }10 write {11 await Len($variable) < BufferSize;12 yield Append($variable, $value);13 }14 }1516 mapping macro DB {17 read {18 yield $variable;19 }20 write {21 yield $value;22 }23 }2425 archetype A(ref conn, ref db)26 variables r;27 {28 l:29 conn := 0;30 r := conn;31 if (r > 0) {32 db["k"] := r + 1;33 };34 print db["k"];35 }3637 variables network = <<>>;3839 process (P = 0) == instance A(ref network, [k in {"k"} |-> 0])40 mapping network via TCPConnection41 mapping @2[_] via DB;42 }Figure 4.9: A simple Modular PlusCal specification291 --algorithm Spec {2 variables network = <<>>,3 * temporaries4 connWrite, connRead, connWrite0, dbWrite, dbWrite0, dbRead;5 process (P = 0)6 variables dbLocal = [k in {"k"} |-> 0], r;7 {8 l:9 * expanded write to conn10 await (Len(network)) < (BufferSize);11 connWrite := Append(network, 0);1213 * expanded read from conn14 await (Len(connWrite)) > (0);15 with (msg0 = Head(connWrite)) {16 connWrite0 := Tail(connWrite);17 connRead := msg0;18 };19 r := connRead;2021 if (r > 0) {22 * expanded write to db23 dbWrite := [dbLocal EXCEPT !["k"] = (r) + (1)];2425 * join write26 dbWrite0 := dbWrite;27 } else {28 * join write29 dbWrite0 := dbLocal;30 };31 * expanded read from db["k"]32 dbRead := dbWrite0["k"];3334 * print uses temporary35 print dbRead;3637 * write-backs38 network := connWrite0;39 dbLocal := dbWrite0;40 }41 }Figure 4.10: Compiled PlusCal output30Write-backsModular PlusCal, just like PlusCal, allows the programmer to put multiple readsand a single write to the same archetype parameter into a labeled atomic step. How-ever, both read and write blocks of a mapping macro may modify the underlyingvariable (e.g., TCPConnection mapping macro in Figure 4.9). Therefore, PGo mustgenerate temporary write variables to save intermediary modifications to the un-derlying variable. The last temporary write variable is written to the underlyingvariable at the end of the label.Join writesWhen control flow forks into multiple execution paths (e.g., if and either state-ments), each path may write a different number of times to an underlying variable.This is a problem because when the execution paths merge back after the statement,there may not be a single temporary variable that can be used for further modifica-tion. For example, in Figure 4.9, db is only modified when r is positive (line 32).Therefore, join writes are inserted (lines 26 and 28 of Figure 4.10) so that there is asingle valid temporary variable to be used after the statement, regardless of whichexecution path was taken.Temporary variables as global variablesTemporary variables capture unnecessary intermediary states. The intermediarystates are distinct from each other due to differences in the values of the temporaryvariables. This leads to an exponential increase in the number of states that TLChas to check.Originally, temporary variables are declared as local variables in compiledPlusCal processes. This further exacerbates the problem of state explosion dueto how local variables in processes are compiled to TLA+. Local variables in Plus-Cal processes are compiled as TLA+ global variables whose values are functionsmapping process identifiers to the local value of that variable in TLA+.To illustrate the problem, consider two example PlusCal outputs of the ModularPlusCal to PlusCal pipeline, shown in Figure 4.11. In Figure 4.11, temp serves asa PGo generated temporary variable for var. The only difference between the two311 --algorithm Spec {2 variables var = [3 i in {1, 2} |-> 04 ];56 process (P in {1, 2})7 variables temp;8 {9 lb:10 temp := [11 var EXCEPT ![self] = self12 ];13 var := temp;14 }15 }1 --algorithm Spec {2 variables3 temp,4 var = [5 i in {1, 2} |-> 06 ];78 process (P in {1, 2}) {9 lb:10 temp := [11 var EXCEPT ![self] = self12 ];13 var := temp;14 }15 }Figure 4.11: Example local and global temporary variable outputsLeft: Local temporary variable PlusCal output.Right: Global temporary variable PlusCal output.specifications is whether temp is a local variable or a global variable.Local variables in PlusCal processes are compiled as TLA+ global functionsmapping process identifiers to the local value of that variable in TLA+ due to thepossibility that the programmer may want to write properties and invariants involv-ing local state of processes. Thus, lines 10 to 12 of the local temporary variableoutput in Figure 4.11 is actually compiled to the following nested function substi-tution 2 in TLA+.tempâ = [temp EXCEPT ![self] = [var EXCEPT ![self] = self]]In other words, temp is actually a nested function. Furthermore, process 1 canonly ever read from or write to temp[1] in the compiled TLA+. Similarly, process 2can only read from and write to temp[2] in the compiled TLA+.The state spaces for the two specifications in Figure 4.11 are shown in Fig-ure 4.12. Below are the states of the local temporary variable specification. Notethat lb is an atomic block for both processes 1 and 2.2A function substitution [func EXCEPT ![x] = y] results in a new function with the samecontent as func, except that key x is mapped to value y in the new function.32Initial stateProcess 1has performed lbProcess 1had performed lbbefore process 2performed lbProcess 2has performed lbProcess 2had performed lbbefore process 1performed lbInitial stateProcess 1has performed lbProcess 2has performed lbBoth processes 1 and 2have performed lbFigure 4.12: State spaces of specifications in Figure 4.11Left: State space for local temporary variable specification.Right: State space for global temporary variable specification.â¢ Initial statetemp = [1 |-> defaultInitValue, 2 |-> defaultInitValue]var = [1 |-> 0, 2 |-> 0]â¢ Process 1 has performed lbtemp = [1 |-> [1 |-> 1, 2 |-> 0], 2 |-> defaultInitValue]var = [1 |-> 1, 2 |-> 0]â¢ Process 1 had performed lb before process 2 performed lbtemp = [1 |-> [1 |-> 1, 2 |-> 0], 2 |-> [1 |-> 1, 2 |-> 2]]var = [1 |-> 1, 2 |-> 2]â¢ Process 2 has performed lbtemp = [1 |-> defaultInitValue, 2 |-> [1 |-> 0, 2 |-> 2]]var = [1 |-> 0, 2 |-> 2]â¢ Process 2 had performed lb before process 1 performed lbtemp = [1 |-> [1 |-> 1, 2 |-> 2], 2 |-> [1 |-> 0, 2 |-> 2]]var = [1 |-> 1, 2 |-> 2]Contrast the state space of the global temporary variable specification and thatof the local temporary variable specification in Figure 4.12. The state space nowhas only four states, which are listed below.33â¢ Initial statetemp = defaultInitValuevar = [1 |-> 0, 2 |-> 0]â¢ Process 1 has performed lbtemp = [1 |-> 1, 2 |-> 0]var = [1 |-> 1, 2 |-> 0]â¢ Process 2 has performed lbtemp = [1 |-> 0, 2 |-> 2]var = [1 |-> 0, 2 |-> 2]â¢ Process 2 had performed lb before process 1 performed lbtemp = [1 |-> 1, 2 |-> 2]var = [1 |-> 1, 2 |-> 2]As discussed above, promoting temporary variables to global variable reducesstate explosion.34PlusCal specificationParsing(Section 4.1.1)ConfigurationConfiguration parsing(Section 4.2.1)Configuration validation(Section 4.2.1)Macro expansion(Section 4.1.2)Validation(Section 4.1.4)Scoping(Section 4.1.5)Post-scoping validation(Section 4.1.6)Type inference(Section 4.2.2)Atomicity inference(Section 4.2.3)Go code generation(Section 4.2.4)Go programFigure 4.13: PGo compiler pipeline from PlusCal to Go4.2 The PlusCal to Go pipelineThe PlusCal to Go pipeline takes a PlusCal specification, as well as a configurationfile, as input and produces a Go program as output (see Figure 4.13).351 Usage: pgo [options] spec2 --version=<boolean> - Version [default false]3 -h --help=<boolean> - Print usage information [default false]4 -q --logLvlQuiet=<boolean> - Reduce printing during execution [default false]5 -v --logLvlVerbose=<boolean> - Print detailed information during execution6 [default false]7 -m --mpcalCompile=<boolean> - Compile a Modular PlusCal spec to vanilla PlusCal8 [default false]9 -c --configFilePath=<string> - path to the configuration file, if anyFigure 4.14: PGoâs accepted command line arguments1 {2 "build": {3 "output_dir": "/path/to/output/dir",4 "dest_file": "file.go",5 "dest_package": "package_name"6 },7 "networking": {8 "enabled": false,9 "state": {10 "strategy": "state-server",11 "endpoints": [],12 "peers": [],13 "timeout": 314 }15 },16 "constants": {17 "CONST": "\
"18 }19 }Figure 4.15: Configuration file for PGo4.2.1 Configuration parsingThe configuration parsing stage parses command line arguments and the configu-ration file. Figure 4.14 shows the command line arguments accepted by PGo. Ifthe programmer turns on compilation from Modular PlusCal to PlusCal, the pathto the configuration file is not required. The configuration file is expected to be avalid JSON object with attributes shown in Figure 4.15. We now overview each ofthe configuration parameters, starting with build.BuildThe build object is required. The output_dir attribute is required and must bean existing path. The programmer must provide either dest_file or dest_package36attribute; if both are provided, dest_package takes precedence. The dest_file at-tributes specifies the name of the output file. The dest_package attribute specifiesthe name of the output Go package.NetworkingThe networking object is optional. If it is not specified, PGo produces a multi-threaded Go program as output. The optional enabled attribute specifies whethernetworking is enabled. The state attribute specifies the configuration for the net-worked state strategy. If the state object is present, enabled is overridden to be true.The strategy attribute specifies which state strategy to use. PGo currently sup-ports state-server and etcd, with state-server being the default. The endpointsattribute specifies the etcd endpoints to connect to. The endpoints attribute is re-quired if strategy is etcd. The peers attribute specifies the peer endpoints to con-nect to. The optional timeout attribute specifies the network timeout in seconds,which defaults to three seconds.ConstantsThe constants object is optional. It contains key-value pairs whose key is the nameof the constant, encoded as a JSON string, and whose value is a TLA+ expression,also encoded as a JSON string.4.2.2 Type inferenceSince Go, the target language, is a statically typed language, PGo introduces a typesystem for effective compilation. The type inference stage is the last stage sharedbetween the Modular PlusCal to Go and the PlusCal to Go pipelines.TypesPGoâs types are defined inductively, as shown in Figure 4.16. The~Ï notation indi-cates a sequence of types, e.g., Tuple[Bool,Tuple[Int]] is a valid type. The âââx : Ïindicates a sequence of fields and types, e.g., Record[dst : String,src : String]is a valid type.37Ï ::=Bool | Int | Real | String | Interface| Set[Ï] | NonEnumerableSet[Ï] | Slice[Ï]| Tuple[~Ï] | Map[Ï1]Ï2 | Record[âââx : Ï]| Function(~Ï)Ï2 | Procedure(~Ï)| AR[read(Ï1);write(Ï2)] | ARC[Ï1][read(Ï2);write(Ï3)]Figure 4.16: PGoâs typesThe type NonEnumerableSet[Ï] is reserved for sets that are not finitely enu-merable, such as built-in constructs like Nat and Integers, which represent thesets of natural numbers and integers, respectively. An example record type isRecord[dst : String,data : String], which is inferred for the TLA+ expression[dst |-> "1.1.1.1", data |-> "payload"]. PlusCal processes and procedures, aswell as Modular PlusCal archetypes and instances, have type Procedure(~Ï).The type AR[read(Ï1);write(Ï2)] is read as archetype resource with read typeÏ1 and write type Ï2. Similarly, the type ARC[Ï1][read(Ï2);write(Ï3)] is read asarchetype resource collection with key type Ï1, read type Ï2, and write type Ï3.These two types are the types of archetype parameters.Type constraintsA typing judgement has the form Î ` t : T | C, which is read as âterm t has typeT under assumptions Î whenever constraints C are satisfiedâ. Below are someexample type rules in PGoâs type system.n â {FALSE,TRUE}CT-BoolÎ ` n : Bool | /0n â {. . . ,-1,0,1, . . .}CT-IntÎ ` n : Int | /0x : T â Î CT-VarÎ ` x : T | /0n â {. . . ,-0.1, . . . ,0, . . . ,0.1, . . .}CT-RealÎ ` n : Real | /0n â {"","a", . . .}CT-StringÎ ` n : String | /038Î ` x : T1 |C1 Î ` y : T2 |C2boolOp â {â§,â¨,â,â¡}C =C1âªC2âª{T1 = Bool,T2 = Bool}CT-BoolOpÎ ` x boolOp y : Bool |CÎ ` x : T1 |C1 Î ` y : T2 |C2setMemberOp â {â, /â}C =C1âªC2âª{T2 = Set[T1]}CT-SetMemberOpÎ ` x setMemberOp y : Bool |CThe typing rules are implemented in multiple classes in PGoâs code base. Forexample, typing rules for built-in TLA+ operators are implemented in the TLABuiltinsclass.The most common type constraints in PGoâs type system are equality type con-straints, as shown in the example typing rules. An equality type constraint statesthat a type T1 must be structurally equal to another type T2. In other words, all con-stituent types within T1, if there are any, must be structurally equal to constituenttypes within T2, recursively.In addition to type equality constraints, PGo also supports has-field constraints.A has-field constraint states that a type T must be a Record and it must have afield f with type T f . This type constraint is necessary since definition and usage ofrecords may span multiple processes or archetypes.Type equality constraints and has-field constraints comprise basic type con-straints. These basic type constraints are then wrapped in monomorphic type con-straints or polymorphic type constraints. A monomorphic type constraint is just asimple wrapper for a basic type constraint. A polymorphic type constraint wrapsmultiple basic constraints, which are considered alternatives. Since a collection oftype constraints encodes the conjunction of them, a polymorphic type constraintallows encoding of disjunctions of basic constraints.Type inference algorithmThe type inference stage has two phases: type constraint collection, and type solv-ing. After type constraints are collected, they are solved by the TypeSolver. The re-sulting solution is a mapping between type variables (stand-ins for unknown typesduring type constraint collection) to concrete types. If a type variable is not mapped39to any concrete type, which happens when there are not enough constraints onit, it is mapped to an Interface. PGoâs Interface type is translated to Goâsinterface{} type in code generation.The TypeSolver works by going through the constraints one by one. If thecurrent constraint is a monomorphic constraint, the solver extracts out the basicconstraint. If the current constraint is a polymorphic constraint, the solver sets upa backtracking point by taking a snapshot of its own state, and pushes the snapshotonto a state stack. It then extracts the first basic constraint from the polymorphicconstraint, and proceeds to solve it. When thereâs a need to backtrack, the solverpops a snapshot from the state stack, reloads its state from the snapshot, and ex-tracts the next basic constraint to be solved. If thereâs no basic constraint left, itreturns an error via the issue context.After extracting a basic type constraint, the TypeSolver proceeds to solve it. Ifthe extracted basic constraint is a has-field constraint, the solver looks up the recordin its record groups to constrain that record if itâs present; otherwise, it adds a newentry for that record. If the extracted basic constraint is not a has-field constraint,it must be a type equality constraint. The solver checks if the left-hand side orthe right-hand side of the equality constraint is a type variable. If so, it looks upthe type variable in its variable groups. If both are type variables, the two groupsto which they belong are merged, and the types to which the two groups map areadded as a type equality constraint to be solved. The left hand side and right handside are then substituted to gain further structural knowledge of their types. Theresulting types are checked to see if they are the same type and their constituenttypes are added as constraints to be solved.The above process repeats until there are no constraints left, at which point thesolver constructs and returns a substitution as the result. In other words, the solverreturns the first solution it can find.Another point of note is that since TLA+ expressions are ambiguous (e.g.,<<1, 2>> can be a tuple or a sequence initialized with two elements), PGo prefersconstraints which give the most amount of information. For example, the TLA+function call a[b] is constrained with (a : Slice[T]â§ b : Int)â¨ (a : Map[T1]T2â§ b :T1)â¨ (a : Function(T1)T2â§ b : T1). The order of basic constraints in the disjunc-tion matters, since TypeSolver returns the first found solution. For example, if40selecting a : Slice[T]â§ b : Int leads to a solution, TypeSolver does not considerthe other constraints.4.2.3 Atomicity inferenceThe atomicity inference stage is the first stage where Modular PlusCal and PlusCalcompilation to Go diverge. This thesis describes only the PlusCal to Go pipeline.PlusCal requires that a statement be part of a label. A block of statements in alabel is executed atomically, i.e., they all succeed or are not executed. Therefore,PGo has to determine if a global variable needs synchronization to maintain thesesemantics in the generated Go code.Global variables that need synchronization are grouped into collections that arecalled lock groups. The lock groups are computed by traversing labeled blocks inprocedures and processes, putting all global variables accessed within a labeledblock into the same group, and merging groups with a common global variable.4.2.4 Go code generationPlusCal has many language constructs that are translated to Go in non-trivial ways.These constructs and their translations are described in this section, starting withan overview of supported PlusCal and TLA+ constructs.PlusCal supportPGo supports both the C and P-syntaxes of PlusCal. PlusCalâs P-syntax denotescode blocks with keywords like begin and end, while its C-syntax denotes codeblocks with curly braces. Note that unused labels are removed from the Go outputand that fresh variable names and labels are generated to avoid name capture.PlusCal feature PGo supportLine comment* line commentSupported; removed from output41PlusCal feature PGo supportBlock comment(* block comment *)Supported; removed from outputLabeled statementslabel:stmt1;stmt2;* ...Compiled with a mutex or a dis-tributed mutex around the statementsAssignmentx := exp;Supported; compiled as expectedMultiple variable assignmentx := y || y := x + y;Supported; compiled as multiple as-signment in GoWhile loopwhile (condition) {body;}Compiled asfor {if !condition {break}body}42PlusCal feature PGo supportIf statementif (condition) {thenPart;} else {elsePart;}Supported; compiled as expectedReturn statementreturn;Supported; compiled as expectedSkip statementskip;Supported; removed from outputCall statementcall proc(arg1, arg2);Supported; compiled as expectedMacro callmacro1(arg1, arg2);Supported; expanded during compi-lation43PlusCal feature PGo supportEither statementeither { stmt1; stmt2; }or { stmt3; stmt4; }or { stmt5; stmt6; }* ...Compiled ascase0:stmt1stmt2goto endEithercase1:stmt3stmt4goto endEithercase2:stmt5stmt6goto endEither// ...endEither:Each case is tried deterministicallyfrom top to bottom (i.e., case0 istried before case1, etc.). Case N istried only after case 0 to N-1 havefailed because await conditions inthose cases are not met.With statementwith (x = exp1,y in exp2) {body;}Supported; compiled as variable as-signment with fresh names. In theexample code, y is assigned the firstelement of exp2.Print statementprint exp;Compiled asfmt.Printf("%v", exp)44PlusCal feature PGo supportAssert statementassert condition;Compiled asif !condition {panic("condition");}Await statementawait condition;Compiled asawaitLabel:if !condition {goto awaitLabel}Goto statementgoto label;Supported; compiled as expectedSingle process algorithm--algorithm Algo {variables x = exp1,y in exp2;{body;}}Supported; compiled as a single-threaded single-process Go program45PlusCal feature PGo supportMultiprocess algorithm--algorithm Algo {variables x = exp1,y = exp2;process (P in exp3)variables local = exp4;{body;}}Supported; compiled with variousstrategies configured by the userTable 4.1: PGo support for PlusCal constructs46TLA+ supportBelow are the TLA+ constructs. Note that PGo makes liberal use of temporaryvariables to compile complex TLA+ constructs.TLA+ feature PGo supportFunction callx[exp1]* orx[exp1, exp2, exp3]* orx[<<exp1, exp2, exp3>>]* orx[[field1 |-> e1,field2 |-> e2]]Supported; compiled code dependenton the type of x (the function). Forexample, when x is a Slice[Ï], thefunction call x[i] is compiled to asimple slice indexing.Binary operator callx / y = z + 1Supported; compiled as expectedRecords[field1 |-> exp1,field2 |-> exp2]Compiled as Go mapsmap[string]interface{}{"field1": exp1,"field2": exp2,}Function set[Nat -> Nat]* or[Nat -> 1..3]* or[1..3 -> 1..3]Unsupported47TLA+ feature PGo supportFunction substitution[f EXCEPT ![exp1] = exp2]* or[f EXCEPT !.field = exp]UnsupportedIf expressionif conditionthen thenExpelse elseExpCompiled asvar result type;if condition {result = thenExp} else {result = elseExp}// result is used in place// of the expression// hereafterTuple (as slice)<<exp1, exp2, exp3>>Compiled as slice when all its con-tents are of the same type[]type{exp1, exp2, exp3}Tuple (as struct)<<exp1, exp2, exp3>>Compiled as a struct when at leastone element is of a different typefrom the othersâ types.struct {e0 typee1 typee2 type}{exp1, exp2, exp3}48TLA+ feature PGo supportCase expressionCASE x -> y[] z -> p[] OTHER -> otherCompiled asvar result type;if x {result = ygoto matched}if z {result = pgoto matched}result = othermatched:// result is used in place// of the expression// hereafterExistentalE a, b, c : exp* orEE a, b, c : expUnsupportable; TLC throws an errorwhen given this expressionUniversalA a, b, c : exp* orAA a, b, c : expUnsupportable; TLC throws an errorwhen given this expressionLet expressionLET op(a, b, c) == exp1fn[d in D] == exp2e == exp3IN expUnsupported49TLA+ feature PGo supportAssumptionASSUME exp* orASSUMPTION exp* orAXIOM expUnsupportedTheoremTHEOREM expUnsupportedMaybe action[exp1]_exp2UnsupportedRequired action<<exp1>>_exp2UnsupportedOperatorOp(arg1, arg2) = expCompiled as a Go functionOperator callOp(exp1, exp2)Supported; compiled as a functioncall50TLA+ feature PGo supportQuantified existentialE a in exp1,b in exp2 : exp3Compiled asexists := falsefor _, a := range exp1 {for _, b := range exp2 {if exp3 {exists = truegoto yes}}}yes:// exists is used in place// of the expression// hereafterQuantified universalA a in exp1,b in exp2 : exp3Compiled asforAll := truefor _, a := range exp1 {for _, b := range exp2 {if !exp3 {forAll = falsegoto no}}}no:// forAll is used in place// of the expression// hereafterSet constructor{exp1, exp2, exp3}Compiled as sorted slice[]type{exp1, exp2, exp3}51TLA+ feature PGo supportSet comprehension{exp : a in exp1,b in exp2}Compiled astmpSet := make([]type, 0)for _, a := range exp1 {for _, b := range exp2 {tmpSet = append(tmpSet,exp)}}// more code to ensure// elements in tmpSet// are unique and sorted// tmpSet is used in place// of the expression// hereafterSet refinement{a in exp1 : exp}Compiled astmpSet := make([]type, 0)for _, v := range exp1 {if exp {tmpSet = append(tmpSet,v)}}// tmpSet is used in place// of the expression// hereafterTable 4.2: PGo support for TLA+ constructsStructure of a compiled Go programA compiled Go program has the following structure: an init function, compiledprocedures, compiled user-defined operators, compiled processes (as Go func-52tions), and a main function.The init function contains initialization code for constants. It also containsinitialization code for global variables, as well as client initialization code for theglobal state backing store (etcd or state server), when compiling a multi-processspecification.When compiling a single-process specification, the main function contains thecompiled output of the single processâs body. When compiling a multi-processspecification, it only contains a âprocess switchâ, which is a switch statement se-lecting the right process based on the command line argument passed to it at run-time. When compiling a multi-process specification using the state server strategy,there are two synchronization barriers before and after the process switch. Thesesynchronization barriers ensure states are initialized correctly and processes termi-nate only when all other processes have finished their work.Critical section trackingSince PlusCal execution model requires that a statement must be part of exactly onelabel, PGo employs mutual exclusions (mutexes) to satisfy this requirement. At thestart and end of a compiled labeled block, PGo inserts mutex lock and unlock coderespectively. However, statements with differing execution paths, e.g., if, while,and either statements, pose a challenge to this simple compilation strategy, sinceeach execution path may execute different labels as well as a different number oflabels. Thus, PGo employs critical section tracking to handle this issue.In critical section tracking, PGo keeps the current active label and lock groupas part of its state. When a statement with diverging execution paths is compiled,PGo makes copies of the tracking state, and follows different paths with differentcopies. Thus, compilation interacts with labeling rules (see Section 4.1.4) in non-trivial ways. For example, Figure 4.17 shows a simple while loop whose conditioncond is in label cond_label, which is different from its bodyâs label body_label, aswell as the pseudocode for the output, where CS is short for critical section. Beforeentering the loop, PGo inserts code to enter the critical section for cond_label (line1). After testing the condition, PGo exits the critical section for cond_label (line 7),and enters the critical section for cond_body (line 8) to execute the body of the loop531 cond_label: while (cond) {2 body_label: body3 };1 enter CS for cond_label2 for {3 if !cond {4 exit CS for cond_label5 break6 }7 exit CS for cond_label8 enter CS for body_label9 body10 exit CS for body_label11 enter CS for cond_label12 }Figure 4.17: Example pseudocode output of while loop(line 9). At the end of the loop, PGo exits the critical section for body_label (line10), and enters the critical section for cond_label (line 11) so that the conditioncond can be safely tested again.54Chapter 5EvaluationAll tests in this chapter are preformed on an Intel Core i7-4720HQ CPU @ 2.60GHzwith 16GB of RAM running Fedora 29 and OpenJDK 1.8.0 201. The TLA+ tool-box version is Version 1.5.7 of 18 July 2018.5.1 How effective is the compiled PlusCal output formodel checking?Since PGo relies on TLC to model check the Modular PlusCal specifications andTLC only accepts TLA+ specifications as input, PGo has to compile Modular Plus-Cal to TLA+. PGo does this by compiling Modular PlusCal to PlusCal, and thenrelies on the TLA+ tool box to convert the resulting PlusCal to TLA+.This experiment tries to determine if there is any degradation in model check-ing performance and how much degradation is introduced by PGoâs approach tocompilation. In this experiment, three Modular PlusCal specifications, written bythe PGo development team, with varying degrees of complexity are used as inputto PGo.The source Modular PlusCal specifications are formatted to maximize com-prehension. All environment-modeling mapping macros are included in the spec-ification. Each variable declaration is put on a new line with an accompanyingcomment explaining what the variable is. Thus, the source specifications are quiteverbose.55On the other hand, the compiled PlusCal specifications are only formattedslightly with indentations by PGo. However, variable declarations are put on thesame line.â¢ Distributed queue. The distributed queue specification is the simplest of thethree specifications. The specification models a single-producer multiple-consumer queue. The producer is modeled as an archetype with two pa-rameters, namely the network connections and a task queue. The producercontinually listens for a work request from any client and then picks a taskfrom the queue to send to the requesting client. A client is modeled as anarchetype with two parameters, namely the network connections, and a taskprocessor. A client continually sends a work request to the producer, getsback a task, and works on the task by invoking the task processor. The fullModular PlusCal specification is 55 lines long. The compiled PlusCal outputhas 59 lines of code.â¢ Load balancer The load balancer specification models a load balancing sys-tem with multiple clients and multiple servers, multiplexed by a single loadbalancer. The clients send requests to the load balancer, which forwardsthem to the servers in a round-robin fashion. The specification models thefile system abstractly. The full Modular PlusCal specification is 87 lineslong. The compiled PlusCal output has 93 lines of code.â¢ Replicated key-value store The replicated key-value store specification isthe most complex of the three specifications. It models a replicated key-valuestore where the replicas only talk to the clients and state modification is onlyapplied when the network message containing the command is stable. Mes-sage stability detection is implemented via buffered messages with logicaltime stamps. The full Modular PlusCal specification is 296 lines long. Thecompiled PlusCal output has 338 lines of code.Each Modular PlusCal specification is compiled to PlusCal using PGo intotwo versions, one where the temporary variables are local to the processes, theother where the temporary variables are global variables. Additionally, the authormanually creates another PlusCal version by removing all the temporary variables,56i.e., this version is the optimal output an ideal compiler can generate. The metricscollected for model checking are time (in seconds), diameter (the length of thelongest behavior found), states found (the total number of states TLC found), anddistinct states (the number of distinct states among the states found).Parameters VersionTime(seconds)Diameter States Found Distinct States1 consumerbuffer size of 1Local 5 13 25 18Global 5 13 25 18Optimal 5 10 21 152 consumersbuffer size of 2Local 5 48 8291 3858Global 5 30 1583 758Optimal 5 30 709 3363 consumersbuffer size of 3Local 109 125 40285707 12840589Global 5 62 123723 45943Optimal 5 59 25065 86354 consumersbuffer size of 4Local timeout N/A N/A N/AGlobal 23 106 11842873 3790768Optimal 6 100 794705 2141765 consumersbuffer size of 5Local timeout N/A N/A N/AGlobal timeout N/A N/A N/AOptimal 30 153 24708973 54590696 consumersbuffer size of 6Local timeout N/A N/A N/AGlobal timeout N/A N/A N/AOptimal timeout N/A N/A N/ATable 5.1: Model checking results for distributed queueTable 5.1 shows the model checking results for the distributed queue specifi-cation. The specification has two parameters: number of consumers and buffersize. With one consumer and a buffer size of one, the global temporary variableversion does not have any model checking performance advantage compared tothe local temporary variable version. Both versions degrade model checking per-formance when compared to the optimal version. The model checking time inseconds, however, shows that model checking for the three versions terminates inthe same amount of time (five seconds). This may indicate that a significant por-tion of the time is spent in initializing TLC. With two consumers and a buffer57size of two, the local temporary variable version starts to show further degradationin model checking performance than the global temporary variable version in allcollected metrics except for running time. Although the state space of the globaltemporary variable version has the same diameter as the optimal version, it con-tains more than twice as many distinct states as the optimal version. This meansthat the state spaces for the local and global temporary variable versions are goingto grow much faster than that of the optimal version. However, the model checkingtime for the three versions are the same, and is also equal to the model checkingtime when there is only one consumer with buffer size of one. This strengthensthe hypothesis that most of the five seconds is spent in initializing TLC. Increas-ing the values of the parameters significantly increases the size of the state space.However, the global temporary variable version shows a much slower growth thanthe local temporary variable version. Nevertheless, the global temporary variableversion still shows much faster growth than the optimal version.Overall, Table 5.1 shows that even such a simple specification as the distributedqueue specification quickly runs into the state explosion problem. It also shows thatdeclaring temporary variables as global variables is a huge state space reductionwhen compared to declaring them as local variables. However, that strategy is stillnot doing enough to keep the state space as small as the version where there are notemporary variables.Parameters VersionTime(seconds)Diameter States Found Distinct States1 client1 serverbuffer size of 1Local 5 19 85 48Global 5 19 85 48Optimal 5 19 85 482 clients2 serversbuffer size of 2Local 35 62 651053 221800Global 10 53 121153 41832Optimal 5 53 16261 55923 clients3 serversbuffer size of 3Local timeout N/A N/A N/AGlobal timeout N/A N/A N/AOptimal 15 101 5316875 13385723 clients3 serversbuffer size of 3Local timeout N/A N/A N/AGlobal timeout N/A N/A N/AOptimal timeout N/A N/A N/ATable 5.2: Model checking results for load balancer58Table 5.2 tells the same story as Table 5.1: global temporary variables are ahuge help but are nowhere near enough to keep state space down.Unfortunately, the state space for the replicated key-value store is infinite, sothe programmer can only rely on bounded model checking which does not explorethe entire state space. Running TLC for bounded time or bounded number of statesdoes not show any difference among the three versions, but only shows the rate ofexploration of the state space in terms of number of explored states, which is about10 million distinct states per minute for all three versions. In addition, TLC doesnot show any other indication of progress, such as how much of the state space isexplored in terms of percentage of the overall state space. Thus, no metrics arecollected for the outputs of this specification.5.2 How complex a specification can PGo compile?This experiment tries to determine if PGo can compile various PlusCal specifica-tions. In this experiment, six PlusCal specifications, which are a mix of pre-existingand newly written specifications, are used as input to PGo. Table 5.3 shows thesizes of the single-process specifications and their outputs. Table 5.4 shows thesizes of the multi-process specifications and their outputs. Below are the descrip-tions of the specifications.â¢ Euclid. The Euclid specification is a simple single-process PlusCal imple-mentation of Euclidâs algorithm for finding the greatest common denomina-tor of two numbers. It does so by continually subtracting the smaller numberfrom the larger number, and stopping only when the the larger number is 0after subtraction. The result is printed to the screen. This specification iswritten by a PGo team member.â¢ Queens. The queens specification is a single-process PlusCal implemen-tation to solve the n-queens problem. The n-queens problem asks for allplacements of n queens on an n-by-n chessboard, such that no queen canattack another. The PlusCal implementation is a brute-force solution thattries to place the next queen such that it cannot attack any previously placed59queens, keeping only successful placements along the way. This specifica-tion is taken from the TLA+ examples repository.â¢ Counter. The counter specification has a number processes all trying toincrement a counter a number of times. This specification checks whetherglobal state management is implemented correctly, by checking if the finalvalue of the counter equals to the number of processes times the number ofiterations. This specification is written by a PGo team member.â¢ Round robin. The round robin specification is just the counter specificationwith an added twist: each process is blocked waiting for its turn at the startof each iteration. At the start of execution, all processes race to get the firstturn. This specification is written by a PGo team member.â¢ Distributed queue. The distributed queue specification models a single-producer multiple-consumer queue. The queue is modeled as a sequence oftasks. This specification is different from the one with the same name de-scribed in Section 5.1. This specification is written by a PGo team member.â¢ Dijkstraâs mutex. The Dijkstraâs mutex specification is a PlusCal imple-mentation of the first mutual exclusion algorithm by Dijkstra [11]. Thisspecification is taken from the TLA+ examples repository.SpecificationSize(lines of code)Output size(lines of code)Euclid 21 36Queens 49 203Table 5.3: Sizes of single-process specifications and their outputs60SpecificationSize(lines of code)Multi-threadedoutput size(lines of code)Distributed systemoutput size(lines of code)Counter 27 55 88Round robin 30 66 115Distributed queue 43 70 117Dijkstraâs mutex 41 173 340Table 5.4: Sizes of multi-process specifications and their outputsThe results in Table 5.3 and Table 5.4 show that PGo can handle moderate-size specifications with non-trivial TLA+ functionalities, such as set operations.PGo successfully compiles the Dijkstraâs mutex specification which is a realisticspecification from the TLA+ examples repository. For examples of the Go outputs,see Section 5.2.1 and Section 5.2.2.Since this thesis does not describe PGoâs run-time system, and discussionsabout the performance of the generated Go program is not meaningful withoutdiscussing the run-time system, no metrics on the performance of the generated Goprograms are collected. Studying the performance of PGoâs compiled Go programsare deferred to future work.To give an intuition about the Go outputs, we provide walkthroughs of twospecifications in the next two subsections.5.2.1 Walkthrough of the queens specification and its compiledsingle-threaded implementationFigure 5.1 shows the queens specification in PlusCal. Line 1 pulls arithmetic op-erators on natural numbers from Naturals, sequence operators (such as Len, Seq(sequence constructor), and Append) from Sequences, and printing operator and pro-cedure (print in PlusCal and printS in TLA+) from TLC. The constant N denotes thesize of the board (line 4), which is assumed to be positive (line 5). The Attacks op-erator (lines 7 to 10) checks if two queens on rows i and j can attack each other bychecking whether they are on the same column (line 8), on the same first diagonal(line 9), or on the same second diagonal (line 10). The IsSolution operator (lines6112 to 14) checks if a placement is a solution by making sure that all queens cannotattack one another. The Solutions operator (line 16) contains all solutions for Nqueens, which is constructed by filtering all NN placements using the IsSolutionoperator. The IsSolution and Solutions operators are not used in the PlusCal spec-ification but they are used in checking whether the PlusCal specification is correct.The sols variable (line 21) contains all solutions found so far, which is ini-tialized as an empty set. The todo variable contains the tasks to be done, whichis initialized as a set containing an empty placement (no queens are placed on theboard). Whenever there is work to be done (line 24), a placement queens is ex-tracted from todo (line 26). The next row, where the new queen is placed, nxtQ, isextracted on line 27. The cols variable (lines 28 and 29) is the set of all columnswhere the next queen can be placed. The exts variable (line 30) is the set of newplacements, constructed by extending the placement on line 26 with the columnson line 28. If the next row nxtQ is the last row to be filled (line 32), then todo isupdated by removing the placement queens, and the solution set sols is extendedwith the new solutions, now in exts (line 33). Otherwise, the placement queens isremoved from todo and new placements, exts, are added to todo. When there areno tasks left in todo, the set of solutions is printed (line 37).There are some additional invariants to check during model checking. TypeInvariant(lines 42 to 44) states that todo is a subset of the power set of the sequence 1 .. N(line 43), all placements in todo must have length less than N (line 43), sols is alsoa subset of the power set of the sequence 1 .. N (line 44), and all solutions in solsmust have length exactly N. Invariant (lines 46 to 49) states that must always bea subset of Solutions (defined on line 16), and when there is no more work (todois empty), Solutions must be a subset of sols, which, together with the previouscondition, means that Solutions and sols must be equal.The compiled single-threaded Go program has 203 lines of code. The configu-ration for this specification only contains the output path and file name, as well asthe value for N, the problem size.As show in Figure 5.2, it starts with the package name (line 1), imported pack-ages (lines 3 to 6), declaration of N as a Go variable (line 8), and the init function,which initializes N to 8, as specified in the configuration. Since only the Attacksoperator is used in the PlusCal specification, only that operator is compiled. Lines621 -------------------------- MODULE Queens -----------------------------2 EXTENDS Naturals, Sequences, TLC34 CONSTANT N ** number of queens and size of the board5 ASSUME N in Nat {0}67 Attacks(queens,i,j) ==8 / queens[i] = queens[j] ** same column9 / queens[i] - queens[j] = i - j ** first diagonal10 / queens[j] - queens[i] = i - j ** second diagonal1112 IsSolution(queens) ==13 A i in 1 .. Len(queens)-1 : A j in i+1 .. Len(queens) :14 Ë Attacks(queens,i,j)1516 Solutions == { queens in [1..N -> 1..N] : IsSolution(queens) }1718 (* --algorithm QueensPluscal19 variables20 todo = { << >> };21 sols = {};2223 begin24 nxtQ: while todo # {}25 do26 with queens in todo,27 nxtQ = Len(queens) + 1,28 cols = { c in 1..N : Ë E i in 1 .. Len(queens) :29 Attacks( Append(queens, c), i, nxtQ ) },30 exts = { Append(queens,c) : c in cols }31 do32 if (nxtQ = N)33 then todo := todo {queens}; sols := sols nion exts;34 else todo := (todo {queens}) nion exts;35 end if;36 end with;37 end while;38 print sols;39 end algorithm40 *)4142 TypeInvariant ==43 / todo in SUBSET Seq(1 .. N) / A s in todo : Len(s) < N44 / sols in SUBSET Seq(1 .. N) / A s in sols : Len(s) = N4546 Invariant ==47 / sols subseteq Solutions48 / todo = {} => Solutions subseteq sols49 =============================================================================Figure 5.1: Queens specification631 package main23 import (4 "fmt"5 "sort"6 )78 var N int910 func init() {11 N = 1112 }1314 func Attacks(queens []int, i int, j int) bool {15 return queens[i-1] == queens[j-1] ||16 queens[i-1]-queens[j-1] == i-j ||17 queens[j-1]-queens[i-1] == i-j18 }1920 func main() {21 todo := [][]int{[]int{}}22 sols := [][]int{}Figure 5.2: Compiled queens specification - preamble1 for {2 if !(len(todo) != 0) {3 break4 }Figure 5.3: Compiled queens specification - while condition14 to 18 shows the compiled output of the Attacks operator, with the expressionsplit on multiple lines to fit on the page. The operator is compiled into a Go func-tion with three parameters. PGo correctly infers the types of the parameters andthe return type of the operator, without aid from the programmer.The rest of the specification is compiled into the main function in Go, startingwith the declaration and initialization of todo and sols. The variables todo andsols are inferred to be sets of sequences of integers, and TLA+ sets are compiledas sorted slices while sequences are compiled as slices, the two variables are oftype slices of slices of integers in Go. Since todo is initialized as a set containingan empty sequence in PlusCal, it is initialized as a slice containing a single emptyslice (line 21). Since sols is initialized as an empty set, it is initialized as an emptyslice (line 22).Figure 5.3 shows how the while condition on line 24 of Figure 5.1 is compiled.641 queens := todo[0]2 nxtQ := len(queens) + 13 tmpSet := make([]int, 0)4 tmpRange := make([]int, N-1+1)5 for i := 1; i <= N; i++ {6 tmpRange[i-1] = i7 }8 for _, c := range tmpRange {9 exists := false10 tmpRange0 := make([]int, len(queens)-1+1)11 for i := 1; i <= len(queens); i++ {12 tmpRange0[i-1] = i13 }14 for _, i := range tmpRange0 {15 tmpSlice := make([]int, len(queens), len(queens)+1)16 copy(tmpSlice, queens)17 tmpSlice = append(tmpSlice, c)18 if Attacks(tmpSlice, i, nxtQ) {19 exists = true20 break21 }22 }23 if !exists {24 tmpSet = append(tmpSet, c)25 }26 }27 cols := tmpSetFigure 5.4: Compiled queens specification - queens, nxtQ, and colsSince this is a single-process output, there is no need to insert locking code. Notethat the check agains an empty collection is compiled as a length check againstzero.Figure 5.4 shows how lines 26 to 29 of Figure 5.1 are compiled. Note thatthe variable queens is assigned to the zeroth element of todo. Lines 4 to 7 showhow 1 .. N is compiled. Lines 8 to 27 show how a set refinement, which removeselements for which the check returns false, is compiled, with the Attacks check online 29 of Figure 5.1 compiled on line 18. There is no need to sort the result, sinceelement removal maintains the sortedness property.Figure 5.5 shows how line 30 of Figure 5.1, which is a set comprehension, iscompiled. It looks involved because it contains code for set element construction(lines 2 to 7), sorting the constructed elements to establish sortedness (lines 8 to19), and removal of duplicate elements to establish uniqueness (lines 20 to 40).Since the condition for the if condition on line 32 of Figure 5.1 is a simple651 tmpSet0 := make([][]int, 0)2 for _, c := range cols {3 tmpSlice := make([]int, len(queens), len(queens)+1)4 copy(tmpSlice, queens)5 tmpSlice = append(tmpSlice, c)6 tmpSet0 = append(tmpSet0, tmpSlice)7 }8 sort.Slice(tmpSet0, func(i int, j int) bool {9 less := len(tmpSet0[i]) < len(tmpSet0[j])10 if len(tmpSet0[i]) == len(tmpSet0[j]) {11 for i0 := 0; i0 < len(tmpSet0[i]); i0++ {12 less = tmpSet0[i][i0] < tmpSet0[j][i0]13 if tmpSet0[i][i0] != tmpSet0[j][i0] {14 break15 }16 }17 }18 return less19 })20 if len(tmpSet0) > 1 {21 previousValue := tmpSet0[0]22 currentIndex := 123 for _, v := range tmpSet0[1:] {24 eq := len(previousValue) == len(v)25 if eq {26 for i0 := 0; i0 < len(previousValue); i0++ {27 eq = previousValue[i0] == v[i0]28 if !eq {29 break30 }31 }32 }33 if !eq {34 tmpSet0[currentIndex] = v35 currentIndex++36 }37 previousValue = v38 }39 tmpSet0 = tmpSet0[:currentIndex]40 }41 exts := tmpSet0Figure 5.5: Compiled queens specification - exts661 tmpSet1 := make([][]int, 0, len(todo))2 for _, v := range todo {3 eq := len(v) == len(queens)4 if eq {5 for i0 := 0; i0 < len(v); i0++ {6 eq = v[i0] == queens[i0]7 if !eq {8 break9 }10 }11 }12 if !eq {13 tmpSet1 = append(tmpSet1, v)14 }15 }16 todo = tmpSet1Figure 5.6: Compiled queens specification - update todo when solutions arefoundinteger comparison, it is compiled simply as nxtQ == N. Figure 5.6 shows how theupdate to todo on line 33 of Figure 5.1, which is a set difference, is compiled.Figure 5.7 shows how the update to sols on line 33 of Figure 5.1, which is aset union, is compiled. It looks involved because sortedness and uniqueness haveto be re-established (lines 4 to 15 and lines 16 to 36, respectively).Since lines 34 of Figure 5.1 is just a combination of a set difference and a setunion, which are already shown in Figure 5.6 and Figure 5.7, its compiled outputwill not be shown.From the compiled output, the following observations can be made.â¢ Constants are compiled as Go variables. This is the case due to the possibilityof complex initialization, e.g., set refinement.â¢ PGo makes liberal use of temporary variables in its Go compiled output.â¢ PlusCal while loops are compiled as infinite loops with in-body checks. Thisis the case also due to the possibility of complex loop condition.â¢ TLA+ sets are compiled as immutable sorted slices in Go.671 tmpSet2 := make([][]int, len(sols), len(sols)+len(exts))2 copy(tmpSet2, sols)3 tmpSet2 = append(tmpSet2, exts...)4 sort.Slice(tmpSet2, func(i0 int, j0 int) bool {5 less0 := len(tmpSet2[i0]) < len(tmpSet2[j0])6 if len(tmpSet2[i0]) == len(tmpSet2[j0]) {7 for i1 := 0; i1 < len(tmpSet2[i0]); i1++ {8 less0 = tmpSet2[i0][i1] < tmpSet2[j0][i1]9 if tmpSet2[i0][i1] != tmpSet2[j0][i1] {10 break11 }12 }13 }14 return less015 })16 if len(tmpSet2) > 1 {17 previousValue := tmpSet2[0]18 currentIndex := 119 for _, v := range tmpSet2[1:] {20 eq := len(previousValue) == len(v)21 if eq {22 for i1 := 0; i1 < len(previousValue); i1++ {23 eq = previousValue[i1] == v[i1]24 if !eq {25 break26 }27 }28 }29 if !eq {30 tmpSet2[currentIndex] = v31 currentIndex++32 }33 previousValue = v34 }35 tmpSet2 = tmpSet2[:currentIndex]36 }37 sols = tmpSet2Figure 5.7: Compiled queens specification - update sols when solutions arefound5.2.2 Walkthrough of round robin specification and its compileddistributed sytem implementationFigure 5.8 shows the round robin specification.The constant procs (line 4) is the number of processes in the distributed sys-tems. The constant iters (line 4) is the number of iterations each process performs.The token (line 8) represents whose turn it is to increment the counter (line 9).At the begining of each iteration, each process waits for its turn (line 15). Itthen increments counter (line 16), passes the token to the next process (line 17),681 --------------------------- MODULE round_robin ---------------------------2 EXTENDS Integers, TLC34 CONSTANT procs, iters56 (*7 --algorithm round_robin {8 variables counter = 0,9 token = -1;1011 fair process (P in 0..procs-1)12 variables i = 0;13 {14 w: while (i < iters) {15 waitToken: await token = -1 / token = self;16 incCounter: counter := counter + 1;17 token := (self + 1) % procs;18 print counter;19 nextIter: i := i + 1;20 }21 }22 }23 *)2425 TokenWithinBounds ==26 token = -1 / token in 0..procs-12728 CounterConverges ==29 (A self in ProcSet: pc[self] = "Done") => (counter = procs * iters)30 =============================================================================Figure 5.8: Round robin specificationand prints the value of counter. Each process performs the above steps iters times(lines 14 and 19).The TokenWithinBounds invariant (lines 25 and 26) checks the value of token isnever out of bounds. The CounterConverges invariant (lines 28 and 29) states thatwhen all processes are done, the value of counter must be equal to the number ofprocesses, procs, times the number of iterations, iters.Figure 5.9 shows how line 15 of Figure 5.8 is compiled. Lines 2 to 8 obtainthe write locks on counter and token. These locks are saved into a handle namedrefs (line 2). The local values of counter and token are updated on lines 9 and 10.The PlusCal await statement is compiled as an if statement with a goto statement,whose target is the current label (waitToken), so that the condition can be testedagain.The globalState variable is a handle on the distributed state of the program.691 waitToken:2 refs, err = globalState.Acquire(&distsys.BorrowSpec{3 ReadNames: []string{},4 WriteNames: []string{"counter", "token"},5 })6 if err != nil {7 panic(err)8 }9 counter = refs.Get("counter").(int)10 token = refs.Get("token").(int)11 if !(token == -1 || token == self) {12 err = globalState.Release(refs)13 if err != nil {14 panic(err)15 }16 goto waitToken17 }18 refs.Set("counter", counter)19 refs.Set("token", token)20 err = globalState.Release(refs)21 if err != nil {22 panic(err)23 }Figure 5.9: Compiled distributed system for round robin specificationEach piece of state is a protected global variable used in the compiled program.Each process has ownership of a global variable once it has obtained a lock on thatvariable. The ownership is moved among processes during execution. When a lockon a variable is released, the ownership of that variable still stays with the processuntil another process obtains the lock on that variable.From Figure 5.9, the following observations can be made.â¢ PlusCal await statements are compiled into busy wait loops. This may hinderperformance if there are too many retries.â¢ PGoâs atomicity inference is imprecise. The counter variable is not used inthe waitToken label but it is still locked in the compiled output.70Chapter 6Discussion6.1 LimitationsModular PlusCal limits the interface of archetype parameters to only reading andwriting. This limits the kinds of systems that can be modeled using Modular Plus-Cal. For example, a programmer may find it hard to model a file system that hasan interface with three functionalities: read from, write to, and seek within a file.PGo makes liberal use of temporary variables when compiling from ModularPlusCal to PlusCal. These temporary variables capture intermediate states, whichgreatly increases the state space for TLC to explore. Currently, PGoâs PlusCaloutputs can be used during system development by setting parameter values to besmall. However, for production deployment, larger values for parameters are usedto provide higher assurance, which greatly increases model checking time. Moreeffort in eliminating these temporary variables must be invested to manage modelchecking time.PGoâs type system, while being an improvement over the previous iteration,is still limited. The lack of support for more advanced typing paradigms, suchas recursive types, coupled with poor error reporting, makes for a frustrating userexperience.PGoâs atomicity inference algorithm is prone to lumping all global variablesinto one lock group, which effectively eliminates concurrency, turning the systeminto a single-threaded program. A different approach to discovering finer grained71lock groups would mitigate this problem.6.2 Future workIn addition to being a verification tool, TLC may be used in PGoâs compilationprocess as an inference tool. For example, prefetching may be framed as an in-ference problem, where correlation among usages of variables may be encoded asa synthetic variable whose value is checked by TLC. To achieve this, PGo mustbe extended with a mechanism to manipulate generated TLA+ output, to invokeTLC on its own, and to parse the output of TLC to obtain the value of the syntheticvariable.Currently, PGo is unverified. Verifying PGo will remove it from the trustedcomputing base, increasing the programmerâs confidence in the correctness of theoutput implementation. One method to verify PGo is to formally model ModularPlusCal, PlusCal, TLA+, and Go, using various dynamic semantics, such as small-step operational semantics. With these semantics available, equivalence betweenthe source specification and the compiled output can be formally established.More effort should be invested into producing quality Go code to exact moreperformance at runtime. For example, currently, PGo outputs mostly immutabledata structures by making multiple copies of the data. Switching to in-place modi-fication may provide performance enhancement to PGo-generated programs.PGo only outputs to Go. However, due to factors such as library availabilityand team consensus, it may not always be possible to incorporate Go tools into anexisting teamâs workflow. Thus, it is desirable for PGo to output to other languages,such as Rust or Java, to promote adoption. Since Go has a simple type system andrequires explicit error handling, Go programs may not be a suitable intermediaterepresentation (IR) for code generation to other languages. On the other hand,lower-level IR, such as LLVM IR, may be too low level, which removes high leveldetails about PlusCal execution model. Instead, a new IR for PGo is recommendedfor ease of multi-target code generation.72Chapter 7Related workDomain-specific languages.There are many languages that are tailored for writing distributed systems.However, they do not provide facilities for checking the correctness of the dis-tributed system implementation. For example, the Emerald programming lan-guage [7] requires the programmer to structure the distributed system as distributedobjects. The smallest unit of execution in Emerald is an active object, which isan object with an associated process. Emerald objects expose methods that pro-vide functionalities for other objects. The Argus programming language [18] alsorequires the programmer to structure the distributed system as a collection of dis-tributed objects, called guardians. Guardians are periodically serialized to disk sothat they can be restored after crashes. In addition to guardians, Argus also in-troduces actions, which are executed atomically as composable transactions. Anaction or a group of composed actions are executed in its entirety (committed) orhave no visible effect on the whole system (failed). The Erlang programming lan-guage [6] is a functional programming language based on the actor model. Theunit of execution in Erlang is called a process, which is a green thread in modernparlance. Processes in Erlang communicate by passing messages. They are cat-egorized into workers and monitors. Workers provide the functionalities requiredfrom the system, while monitors are in charge of restarting the workers when one ofthem fails. These languages provide the programmers with tools to structure theirdistributed systems. In contrast to these languages and systems, PGo provides tools73to check for correctness via the TLA+ tool box.Correspondence using proof assistants.There have been many attempts at bridging the gap between formally verifiedspecifications and system implementations. PGo differs from these approachesby not requiring the user to write proofs for verification. Instead, PGo relies onmodel checking, using TLC for verification. For example, Verdi [20] requires theprogrammer to write the specification, the implementation, and the proof that theimplementation matches the specification in Coq [19]. The specification , andthe implementation are written against an ideal networking environment (e.g., nopacket drop, reordering, nor corruption). Verdi provides system transformers totransform the system of specification, implementation and proof into one that canhandle faults. The transformed system is then verified by the Coq theorem prover.The implementation is then extracted to an executable using Coqâs tools. Iron-Fleet [13] proposes a methodology to structure the implementation of a distributedsystem and its increasingly abstract specifications as layers to allow feasible veri-fication of practical distributed system implementations. Both Verdi and IronFleetplace a big burden of writing the proofs on the programmer. This burden is nottrivial, since it has been shown in both projects that the proof effort is at least tentimes the implementation effort in terms of lines of code. Instead of requiring for-mal proofs, PGo relies on model checking for verification. This erases the burdenof proof at the expense of verification time due to state-space explosion.Correspondence using model checkers.There are also other efforts of bridging the gap between formal specificationand system implementation using model checking. PGo differs from these projectsin that its input languages, namely PlusCal and Modular PlusCal, does not re-quire the programmer to structure the system as a state machine. For example,Mace [14, 15] is a source-to-source compiler from a highly structured domain-specific language (DSL) to C++. It requires the programmer to write distributedsystems as state machines, complete with explicit states and transitions. Thismakes the implementation amenable to model checking. P [10] provides a DSLfor asynchronous event-driven programs and a model checker to explore the statespaces for verification. Its successor, P# [9], extends P for writing distributed sys-tems, and provides a test environment for systematic exploration of the state space.74Instead of requiring the system to be written as a state machine, PGo provides morefreedom in how the specification is structured.Checking concrete implementations.Instead of checking specifications, there have been approaches to directly check-ing the implementation. PGoâs approach, on the other hand, provides efficientverification and automatic translation from abstract model to concrete implemen-tation. For example, Verisoft [12] aims to check concrete programs via statelesssearch. It employs partial-order reduction techniques and bounds on the number ofstates explored to keep checking time manageable. MODIST [21] extends this todistributed systems. Work in this category has the benefit of being a drop-in solu-tion for existing implementations. In contrast, PGoâs approach provides automatedverification and translation from abstract model to concrete implementation.75Chapter 8ConclusionThis thesis presents Modular PlusCal, an extension of PlusCal with the goal ofadding a clear distinction between system specification and environment specifi-cation, and PGo, a compiler from Modular PlusCal and PlusCal specifications toGo distributed system implementations. PGo reduces the burden of translating aspecification to an implementation, which increases programmer productivity.76Bibliography[1] Summary of the Amazon EC2 and Amazon RDS Service Disruption in theUS East Region. URL https://web.archive.org/web/20190407054157/https://aws.amazon.com/message/65648/ (Accessed on 2019-03-14). â pages1, 2[2] Azure Cosmos TLA+ specifications. Contribute to Azure/azure-cosmos-tladevelopment by creating an account on GitHub. URLhttps://web.archive.org/web/20190415013638/https://github.com/Azure/azure-cosmos-tla (Accessed on 2019-04-11). â page 2[3] TLA+ Proof System, . URLhttps://web.archive.org/web/20181127125818/http://tla.msr-inria.inria.fr/tlaps/content/Home.html (Accessed on 2019-04-11).â page 2[4] Cloud based distributed TLC, . URLhttps://web.archive.org/web/20190415013939/https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/ (Accessed on 2019-04-11). âpage 2[5] The TLA+ Hyperbook. URLhttps://web.archive.org/web/20190217125233/http://lamport.azurewebsites.net/tla/hyperbook.html (Accessed on 2019-03-14).â page 1[6] J. Armstrong. Making Reliable Distributed Systems in the Presence ofSoftware Errors. URL https://web.archive.org/web/20190405190606/http://erlang.org/download/armstrong thesis 2003.pdf (Accessed on2019-04-14). â page 73[7] A. P. Black, N. C. Hutchinson, E. Jul, and H. M. Levy. The Development ofthe Emerald Programming Language. In Proceedings of the Third ACM77SIGPLAN Conference on History of Programming Languages, HOPL III,pages 11â1â11â51. ACM. ISBN 978-1-59593-766-7.doi:10.1145/1238844.1238855. â page 73[8] F. Z. B. M. M. B. M. C. N. Deardeuff, Tim Rath. How Amazon WebServices Uses Formal Methods. URL https://web.archive.org/web/20190302044811/https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract(Accessed on 2018-05-02). â page iii[9] P. Deligiannis, A. F. Donaldson, J. Ketema, A. Lal, and P. Thomson.Asynchronous Programming, Analysis and Testing with State Machines. InProceedings of the 36th ACM SIGPLAN Conference on ProgrammingLanguage Design and Implementation, PLDI â15, pages 154â164. ACM.ISBN 978-1-4503-3468-6. doi:10.1145/2737924.2737996. â pages 2, 74[10] A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, and D. Zufferey. P:Safe Asynchronous Event-driven Programming. In Proceedings of the 34thACM SIGPLAN Conference on Programming Language Design andImplementation, PLDI â13, pages 321â332. ACM. ISBN978-1-4503-2014-6. doi:10.1145/2491956.2462184. â page 74[11] E. W. Dijkstra. Solution of a Problem in Concurrent Programming Control.8(9):569â. ISSN 0001-0782. doi:10.1145/365559.365617. â page 60[12] 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. ACM.ISBN 978-0-89791-853-4. doi:10.1145/263699.263717. â page 75[13] C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L.Roberts, S. Setty, and B. Zill. IronFleet: Proving Safety and Liveness ofPractical Distributed Systems. 60(7):83â92. ISSN 0001-0782.doi:10.1145/3068608. â page 74[14] 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. USENIX Association, . â pages2, 74[15] C. E. Killian, J. W. Anderson, R. Braud, R. Jhala, and A. M. Vahdat. Mace:Language Support for Building Distributed Systems. In Proceedings of the7828th ACM SIGPLAN Conference on Programming Language Design andImplementation, PLDI â07, pages 179â188. ACM, . ISBN978-1-59593-633-2. doi:10.1145/1250734.1250755. â pages 2, 74[16] L. Lamport. Specifying Systems: The TLA+ Language and Tools forHardware and Software Engineers. Addison-Wesley Longman PublishingCo., Inc., . ISBN 978-0-321-14306-8. â page 5[17] L. Lamport. A High-Level View of TLA+, . URLhttps://web.archive.org/web/20190415014843/https://lamport.azurewebsites.net/tla/high-level-view.html (Accessed on2019-04-11). â page 1[18] B. Liskov. Distributed Programming in Argus. 31(3):300â312. ISSN0001-0782. doi:10.1145/42392.42399. â page 73[19] T. C. D. Team. The Coq Proof Assistant, version 8.9.0. URL https://web.archive.org/web/20190415015254/https://zenodo.org/record/2554024(Accessed on 2019-04-01). â page 74[20] 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. In Proceedings of the 36th ACM SIGPLAN Conferenceon Programming Language Design and Implementation, PLDI â15, pages357â368. ACM. ISBN 978-1-4503-3468-6. doi:10.1145/2737924.2737958.â page 74[21] J. Yang, T. Chen, M. Wu, Z. Xu, X. Liu, H. Lin, M. Yang, F. Long,L. Zhang, and L. Zhou. MODIST: Transparent Model Checking ofUnmodified Distributed Systems. In Proceedings of the 6th USENIXSymposium on Networked Systems Design and Implementation, NSDIâ09,pages 213â228. USENIX Association. â page 7579
Thesis/Dissertation
eng
Computer Science
Vancouver : University of British Columbia Library
Attribution-NonCommercial-NoDerivatives 4.0 International
Graduate
Corresponding formal specifications with distributed systems
Text