Fork me on GitHub

PGo logo PGo

Outline

In PGo’s active-development state, we do not provide stable releases. To run PGo, the best way is to clone the repository, and, on the master branch, run it via the sbt build tool:

$ sbt
> run [command-line arguments]

See the usage notes below for what arguments the program accepts. Note: if you run it on one line, then you must quote the arguments, as in sbt run "[command-line arguments]".

Usage

The PGo tool’s help text reads:

PGo compiler
  -h, --help   Show help message

Subcommand: gogen
  -o, --out-file  <arg>
  -p, --package-name  <arg>
  -s, --spec-file  <arg>
  -h, --help                  Show help message

Subcommand: pcalgen
  -s, --spec-file  <arg>
  -h, --help               Show help message

It has two subcommands: gogen and pcalgen.

gogen

The gogen subcommand requests that PGo generate a Go file from an MPCal-containing TLA+ module. Most customisation of this stage should be done by choosing specific parameters when calling the generated Go code, so there are only a few options to consider.

pcalgen

The pcalgen subcommand requests that PGo rewrite its MPCal-containing TLA+ input file, such that it contains a PlusCal translation of the MPCal algorithm. The only option, --spec-file, is the path to the spec file, which will be rewritten.

To insert the PlusCal translation, PGo will look for comments like, give or take whitespace:

\* BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
\* END PLUSCAL TRANSLATION

If it cannot find one of both of these comments in that order, it will give up with an error message describing the problem, and will not write any output.

How it works

PGo is a source to source compiler written in Scala. It compiles specifications written in an extension of PlusCal, called Modular PlusCal (see the Modular PlusCal page for more details), to Go programs.

How to build (for development)

PGo’s Scala code builds via an sbt project, with its dependencies managed by Maven. PGo additionally provides a runtime support library for its generated Go code, which lives in the distsys/ subfolder. This Go code is a standard Go module, which can be imported via the URL https://github.com/DistCompiler/pgo/distsys.

The main build script is the top-level build.sbt. To build from terminal, run sbt in the root directory and use the standard commands provided by the sbt console. These include run <command-line args> to (re-)compile and run PGo, and test to run all tests, including Go tests.

The sbt build can also be auto-imported by the IntelliJ Scala plugin, as well as likely any other IDE with Scala support.

PGo’s Scala code has managed dependencies on a small set of utility libraries:

PGo’s test suites additionally depend on:

PGo’s Go runtime library depends on:

PGo is tested using OpenJDK 1.11 through 1.16, and Go 1.18. OpenJDK 1.11+ is needed because of standard API usage. Go >=1.18 is needed because of generics.

Example verification workflow

In this section, we’ll go over how to verify a load balancer. We’ll get PGo’s example load balancer specification, compile it to PlusCal using PGo, compile the resulting PlusCal to TLA+ using the TLA+ toolbox, and then verify some invariants and properties of the specification in the toolbox.

  1. Download PGo’s example load balancer specification.

  2. Compile the specification to PlusCal (output in the same file) using PGo with the following command, replacing the example paths with appropriate paths.

    sbt run pcalgen --spec-file systems/loadbalancer/load_balancer.tla
  3. Open the load balancer specification in the TLA+ toolbox (by going to File > Open Spec > Add New Spec… > Browse…).

    Add New Spec...
    Add New Spec...
    Browse...
    Browse...
  4. Press Ctrl-t to compile PlusCal to TLA+ (output in the same file).

  5. On the left pane, right click on models, select New Models…, and name the new model. The created model is opened on the right pane.

    New model...
    New model...
    New model dialog...
    New model dialog...
  6. In “What is the model?” on the lower right side, double click on each item and fill in the following values.

    ItemValue
    GET_PAGE1
    NUM_CLIENTS1
    NUM_SERVERS1
    BUFFER_SIZE1
    WEB_PAGE1

    You can vary the values as you see fit.

    Value filling...
    Value filling...
    What is the model?
    What is the model?
  7. Scroll down and expand out Invariants and Properties on the lower left side.

    What to check?
    What to check?
  8. In Invariants, click Add, type in BuffersOk, and click Finish. BuffersOk (found on line 501) states that the buffer must not underflow nor overflow.

    Invariants...
    Invariants...
  9. In Properties, click Add, type in ClientsOk, and click Finish. ClientsOk (found on line 515) states that the client requesting a web page eventually receives that web page.

    Properties...
    Properties...

    What to check? should now look like the following.

    What to check?
    What to check?
  10. Click Run TLC on the model. (the green circle with a white triangle that looks like a play button)

    Run TLC on the model...
    Run TLC on the model...

    Below is an example output.

    Results
    Results

    The output shows that TLC ran for 6 seconds in breath-first search mode. It found 3033 states, out of which 1274 states are distinct (visited states are not rechecked). The specification satisfies the invariant BuffersOk and property ClientsOk so TLC output No errors.

Example invariant violation

In this section, we’ll modify the example load balancer to see an example violation of desired invariant BuffersOk.

  1. Open the load balancer specification in the TLA+ toolbox.

  2. Comment out line 234, which instructs the client to wait until the buffer is not full before sending a message. Press Ctrl-s to save.

    Where to comment
    Where to comment
  3. Recompile the file using PGo.

  4. Reload the file when asked to do so in the toolbox.

    Reload...
    Reload...
  5. Press Ctrl-t to recompile to TLA+.

  6. Open the created model and run it.

    Run TLC on the model...
    Run TLC on the model...

    TLC shows that invariant BuffersOk is violated.

    Violation
    Violation

    The Error-Trace pane shows how BuffersOk is violated. In this case, the client sent two messages to the server, which overflows the network buffer of size one.

    Error trace
    Error trace