PGo <img src="piggo.svg" alt="PGo logo" style="width: 1em; height: 1em; vertical-align: middle" />

PGo is a source to source compiler that translates Modular PlusCal specifications (which use a superset of PlusCal) into Go programs.

In addition to the PGo compiler, this source tree includes:

the distsys support library, which is used by PGo's generated Go code, available in the distsys/ folder.
systems built using PGo in the systems/ folder, including a Raft-based key-value store.
syntax highlighting modes for Visual Studio Code and pygments, available in the syntax/ folder.
the TraceLink utility, for validating MPCal models against implementation execution traces.

You can read more about the research aspects of our work in our ASPLOS'23 paper, a copy of which is included in this repository. Our evaluation of PGo distinguished artifact award at that conference 🏆.

We also have a couple of videos you can watch:

Purpose and motivation

PlusCal is a language for specifying/modeling concurrent systems. It was designed to make it easier to write TLA+. In particular, PlusCal can be compiled into TLA+, which can be checked against useful system properties (using the TLC model checker). For example, here is a repository of PlusCal formulations of solutions to the mutual exclusion problem.

Go is a C based language developed by Google for building distributed systems. It has built in support for concurrency with channels, and goroutines, which makes it great for developing distributed systems.

Currently there are no tools that correspond a PlusCal/TLA+ spec with an implementation of the spec. PGo is a tool that aims to connect the specification with the implementation by generating Go code based on a specification written in Modular PlusCal. The "Modular" prefix comes from the need to distinguish the description of a system from the model of its environment, which is needed for model checking. PGo enables the translation of a Modular PlusCal description of a distributed system to verifiable PlusCal, as well as to a semantically equivalent Go program.

Current status

Actively under development. PGo supports compilation of all PlusCal control flow constructs. PGo also supports a vast majority of the value-level TLA+ supported by TLC. See the pull requests and issues for documentation of ongoing work.

In its active-development state, we do not provide stable releases, but as an experiment, a recent snapshot of PGo is available from Maven as com.fhackett::pgo:0.1.0 link.

To run PGo, the best way is to clone the repository, and, on the main branch, run it via the bundled mill build tool:

./mill pgo.runMain pgo.PGo --help

We also provide a helper script ./pgo.sh, which acts like a development-local PGo executable.

To make your own local build, run the following:

./mill pgo.assembly

You can then find an executable file out/pgo/assembly.dest/out.jar, which is usable as a portable PGo executable.

To use PGo as a dependency in another application, here are instructions using the mill build system:

move the PGo jar under your package directory inside the lib directory. Note that lib directory is not in your project root, i.e., where the build.mill lives.

my-project-root/
 ├── build.mill
 ├── my-package/
 │   ├── lib/
 |        ├── dep1.jar
 |        ├── dep2.jar
 |        ├── ...
 |   ├── src/
 |        ├── Main.scala
 |   ├── test/src
 |        ├── MainTests.scala
 └── out/

include this snippet in your build.mill to include jars under <package>/lib as "unmanaged" dependencies. See mill's documentation

// mill version is 0.12.14
def lib = Task.Source("lib")
def unmanagedClasspath = Task {
 if (!os.exists(lib().path)) Agg()
 else Agg.from(os.list(lib().path).map(PathRef(_)))
}

See the usage notes below for what arguments the program accepts.

Usage

To learn how to use PGo during verification, see the PGo usage page (WARNING: this information needs updating).

For the tool's compilation modes and flags at a high level, see below.

The PGo tool's help text reads (with subcommand parts moved into each relevant section):

PGo compiler
  -n, --no-multiple-writes   whether to allow multiple assignments to the same
                             variable within the same critical section. PCal
                             does not. defaults to false.
  -h, --help                 Show help message

Subcommand: gogen
  ...
Subcommand: pcalgen
  ...
Subcommand: tracegen
  ...
Subcommand: tlc
  ...

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.

  -o, --out-file  <arg>       the output .go file to write to.
  -p, --package-name  <arg>   the package name within the generated .go file.
                              defaults to a normalization of the MPCal block
                              name.
  -h, --help                  Show help message

 trailing arguments:
  spec-file (required)   the .tla specification to operate on.

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. It requires the path to the spec file, which will be rewritten.

  -h, --help   Show help message

 trailing arguments:
  spec-file (required)   the .tla specification to operate on.

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.

tracegen

Generate a tracing setup. The requires arguments are the TLA+ specification and a directory, which is both where .log files generated by an instrumented PGo implementation live, and where the auxiliary TLA+ files for trace validation will be generated.

You can customize whether TLC should follow all paths or just one, a .cfg file including manual TLC configuration, whether to generate progress-inv ("sidestep" in the paper), and whether to prune paths by reasoning about physical time.

  -a, --all-paths                    explore all paths (as opposed to just one);
                                     default = true
      --noall-paths
  -c, --cfg-file  <arg>              config file fragment to include in
                                     *Validate.cfg
      --cfg-fragment-suffix  <arg>   suffix to add to
                                     {model_name}Validate{suffix}.cfg, when
                                     looking for a manual config file
  -l, --logs-dir  <arg>              directory containing log files to use
      --physical-clocks              rule out interleavings by reasoning about
                                     wall-clock time; default = false
      --nophysical-clocks
  -p, --progress-inv                 assert vector clock progress is always
                                     possible; default = true
      --noprogress-inv
  -h, --help                         Show help message

 trailing arguments:
  spec-file (required)   the specification file from which to infer parameters
  dest-dir (required)    directory into which code should be generated

harvest-traces

Utility that helps re-run a PGo-generated system in order to gather unique sets of traces. It should be invoked with tool-specific options, then -- prog invocation, a bit like the time command. Note: it currently only works from the repository root, as it automatically splices a dependency on the local the distsys checkout into any go.mod files used by the target system.

It uses environment variables to configure the running Go code, and you can use any command-line invocation that runs the intended code once.

When collecting traces, it will stream them into the folder you specify, and then delete them if they turn out to be identical to another set that is present.

Additional options include how many unique traces you need, and the average disruption time to apply to the system. Beware that, for very simple systems, requesting many traces might cause an endless loop due to a limited set of traces being possible.

  -d, --disruption-time  <arg>     average time for disruptions
      --traces-needed  <arg>       how many unique traces to discover
  -t, --traces-sub-folder  <arg>   subfolder to store generated traces
  -h, --help                       Show help message

 trailing arguments:
  folder (required)       folder where the system to trace lives
  victim-cmd (required)   command to launch the implementation code, specify
                          after -- (will be launched repeatedly)

tlc

This is a helper to streamlin

Pgo

Install / Use

README