Skip to content

TLAConf 2019 Demo

Jump to bottom
Finn Hackett edited this page Sep 6, 2019 · 5 revisions

This demo showcases load_balancer.tla, a basic round-robin load balancer that can be found in examples/mpcal/ in the PGo repository. A setup very similar to this demo is part of our automated integration tests.

We verify correctness by translating the MPCal to PlusCal then model-checking this simple property: every client request must receive a response.

We then generate modular Go code and show how that can be used to specialise the generic MPCal archetypes into a file server.

Setup

This demo assumes you have at least one Ubuntu machine, and your username is tlaconf.

You will need to install Go, along with some dependencies for pgo.distsys:

apt install golang
go get github.com/coreos/etcd github.com/mitchellh/hashstructure

Note: the etcd dependency is for another etcd-based mode PGo's runtime supports. Our plain fileserver only uses RPC.

For the model checking portion, you'll need a copy of the tla2tools.jar, which you can get here. Our demo places this in ~/toolbox/.

We also need a copy of PGo, which we can clone from the public Github:

git clone https://github.com/UBC-NSS/pgo.git
git checkout tlaconf-demo

The TLAConf branch is almost the same as master, but the root directory contains files relevant to the demo for easy access along with a couple of demo-friendly edits.

Before you start, make sure you build PGo:

ant build

If you don't have Ant installed, try this:

apt install ant

If you want nice Vim syntax highlighting for the TLA+ / PlusCal shown in the demo, you can also check out these third-party syntax files into your ~/.vim/: https://github.com/hwayne/tla.vim.

Model checking

To simplify the demo, we’ll be using the command-line approach to invoking TLC. Anything done here can also be done as usual with the toolbox.

Everything in this part of the demo is done in the ~/pgo folder:

cd pgo

First, take a look at load_balancer.tla:

vim load_balancer.tla
:95

You'll see elaborations of the archetypes in the slides, along with one new archetype: AClient. As the name suggests, it models a client for the servers/load balancer. In a sense, this client is a puppet. Since client actions are situation-specific, the client takes a sequence of requests instream as input and provides a sequence of server responses as outstream the output. These can either be model checking stand-ins or actual requests for the implementation.

To model check this code, first we compile the Modular PlusCal to PlusCal:

./pgo.sh --mpcalCompile load_balancer.tla

The above ensures the MPCal is compiled to PlusCal, at which point the normal TLA Toolbox can be used.

Then, you compile the PlusCal to TLA+:

java -cp ../toolbox/tla2tools.jar pcal.trans load_balancer.tla

Once we have actual TLA+, we can model-check it. So our model checking time is demo-friendly, we choose a simple set of constants, similar to the setup we’ll be using for the compiled code.

To illustrate:

$ cat load_balancer.cfg
CONSTANT defaultInitValue = defaultInitValue
\* Add statements after this line.
SPECIFICATION Spec
CONSTANT GET_PAGE = "get_page"
CONSTANT NUM_CLIENTS = 1
CONSTANT NUM_SERVERS = 2
CONSTANT BUFFER_SIZE = 1
CONSTANT LoadBalancerId = 0
CONSTANT WEB_PAGE = "web_page"
INVARIANT BuffersOk
PROPERTY ClientsOk

To mimic our live demo setup later, we'll model check a load balancer with 2 servers and 1 client, and a buffer size of 1.

The property we’ll be checking is ClientsOk:

vim load_balancer.tla
:569

ReceivesPage(client) == pc[client] = "clientReceive" ~> pc[client] = "clientRequest"
ClientsOk == \A client \in (NUM_SERVERS+1)..(NUM_SERVERS+NUM_CLIENTS) : ReceivesPage(client)

Essentially, this checks that every client request receives a response the same way you would check for PlusCal.

To run this model checking scenario, we invoke TLC:

java -XX:+UseParallelGC -jar ../toolbox/tla2tools.jar load_balancer.tla

This succeeds, so for these settings our model satisfies our properties.

Show system running

We will compile the model with PGo, then show it running on a network, serving files from a real filesystem. We'll be running the load balancer with 2 servers and one client.

We assume 4 servers, set up as described above (replace these with your own setup):

ssh tlaconf@tlaconf-aloadbalancer0.eastus.cloudapp.azure.com
ssh tlaconf@tlaconf-aserver1.eastus.cloudapp.azure.com
ssh tlaconf@tlaconf-aserver2.eastus.cloudapp.azure.com
ssh tlaconf@tlaconf-aclient3.eastus.cloudapp.azure.com

PGo, when used to generate Go code, takes a JSON configuration file as input:

$ cat load_balancer.json
{
  "build": {
    "output_dir": "/home/tlaconf/go/",
    "dest_package": "load_balancer"
  },
  "constants": {
    "NUM_CLIENTS": "1",
    "LoadBalancerId": "0",
    "GET_PAGE": "200",
    "NUM_SERVERS": "2"
  }
}

This asks PGo to write the resulting Go module (and all supporting libraries) to our local GOPATH. We also specify values for TLA+ constants here.

You can run PGo in this mode like so:

./pgo.sh -c load_balancer.json load_balancer.tla

At this point we have a generic library called load_balancer. It is somewhat longer than the Modular PlusCal code, but generally corresponds to it.

$ wc -l ~/go/src/load_balancer/load_balancer.tla
538 go/src/load_balancer/load_balancer.go

vim ~/go/src/load_balancer/load_balancer.go

Aside from some boilerplate, the library contains functions representing each archetype defined in the Modular PlusCal. Looking at the function bodies, you can see Go code matching the general shape of a while(TRUE) and some labels matching those from the MPCal.

We are however missing a main function, which is needed to provide a concrete environment in which to run these archetypes:

vim main.go
:111

As you can see, all we’re doing is instantiating the appropriate archetype resources. Running a compiled archetype is just a function call, which we do in a goroutine for our purposes. When we run the client, we are free to pipe in client requests whenever we want. In this case, we wait one second between requests to show what's happening. Without the sleep call, the demo completes instantaneously.

Here are the commands to run the complete demo, one block per machine:

go run main.go 'ALoadBalancer(0)' tlaconf-aloadbalancer0:2222

go run main.go 'AServer(1)' tlaconf-aserver1:3333 pages/

go run main.go 'AServer(2)' tlaconf-aserver2:4444 pages/

go run main.go 'AClient(3)' tlaconf-aclient3:5555

Our main files needs generally 2 arguments: the archetype name and process ID (in the PlusCal sense), and the host:port to bind to. The servers also take the root folder to serve.

Clone this wiki locally