Skip to content

VeyMont

Jump to bottom
Robert Mensing edited this page Aug 14, 2024 · 62 revisions

VeyMont is a tool for verification of concurrent message passing programs, also called choreographies. It is implemented as an extension of VerCors. VeyMont generates an implementation from a choreography using the endpoint projection. In this implementation, each endpoint is executed as a thread, and is responsible for a part of the choreography. When these threads are all executed in parallel, the behaviour follows the choreography. Essentially, this projection preserves functional correctness, which is proven with VerCors on the choreography, and guarantees deadlock-freedom. In addition, contracts written in proper form are preserved and projected to the proper endpoint. This allows re-verification of the generated implementation, decreasing the need to trust the implementation of VeyMont, as well as allowing modifications to the generated implementation.

We will introduce the syntax of choreographies through a simple example. Then we will show how to verify it using the permission generation capabilities of VeyMont. Finally, we will introduce the syntax for choreography contracts & permissions, and channel invariants. Using these, we will verify a property of the example. We will assume the reader is familiar with PVL concepts such as permissions, the separating conjunction, contracts and classes. At the end of this section we will give some further directions for reading, as well as an overview of all syntax that VeyMont supports.

Choreography syntax

Choreographies are defined using the choreography keyword. They have a name, arguments, and a body. For example, the next code snippet defines a choreography named Example, and has two parameters, the integers x and y.

choreography Example(int x, int y) {
  // Empty body
}

The body of a choreography consists of endpoint definitions and a single run definition. Endpoint definitions have a name, a class type, and arguments. For example, we can add a Store class with two integer fields. We then define two endpoints using the Store class. We initialize the endpoints with the x and y parameters from the main arguments of the choreography.

class Store {
  int v;
  int temp;

  constructor(int init) {
    v = init;
  }
}

choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);
}

The Store class is a regular PVL class, for more information we refer the reader to the PVL documentation here. It is sometimes omitted in this documentation, but it should be included when verifying the choreography, as otherwise the program cannot be typechecked.

The run definition of a choreography contains the logic of the choreography, and determines the interactions between the endpoints. It is defined using the run keyword and a block of choreographic statements. The next example exchanges the two values using choreographic statements. First, each endpoint sends their v value to the temp field of the other endpoint using the communicate statement. Then, each endpoint copies the value in their temp fields to their v fields using :=, the choreographic assignment operator. The difference between choreographic assignment and regular assignment, is that a choreographic assignment may only read and write to memory that is owned by the endpoint being assigned to.

choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  run {
    communicate alex.v -> bobby.temp;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

Using VeyMont: choreographic verification & permission generation

This example lacks contracts and permissions. However, it can still be verified, and an implementation can also be generated. This can be done using the following command:

$ vercors --veymont example.pvl --generate-permissions --veymont-output example_output.pvl
[INFO] Start: VeyMont (at 10:52:56)
[INFO] Choreography verified successfully (duration: 00:00:10)
[INFO] Writing unknown.pvl to example_output.pvl
[INFO] Implementation generated successfully
[INFO] Implementation verified successfully (duration: 00:00:07)
[INFO] Done: VeyMont (at 10:53:14, duration: 00:00:17

This command executes several steps:

  • Permissions are generated according to the single-owner policy. This means that each endpoint owns its own fields, and is not allowed to read or write fields of other endpoints.
  • The choreography is verified. This succeeds, as the program is memory safe: each endpoint only reads and writes its own fields.
  • An implementation is generated using the endpoint projection. All generated permissions are projected to the endpoint that contains the field referenced in the permissions. As the --veymont-output is also present, the implementation is also written to the path given.
  • The generated implementation is verified. This again verifies, as expected for this simple example, because the choreography verified as well. This is not always the case, as we will show in a later section.

If you want to use only one of these steps, you can use the --choreography, --generate, and --implementation flags, respectively, to make veymont skip the other steps.

Choreographic contracts

Channel invariants & choreographic contracts can be used to specify & verify functional correctness and memory safety. Using choreographic contracts, we can manually specify the permissions that VeyMont generated for us with the --generate-permissions flag:

class Store {
  int v;
  int temp;

  ensures Perm(v, 1) ** v == init;
  ensures Perm(temp, 1);
  constructor(int init) {
    v = init;
  }
}

choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  requires (\endpoint alex;
    Perm(alex.v, 1) **
    Perm(alex.temp, 1));
  requires (\endpoint bobby;
    Perm(bobby.v, 1) **
    Perm(bobby.temp, 1));
  run {
    communicate alex.v -> bobby.temp;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

Specifically, we add permissions to the constructor of Store, and permissions to the precondition of run. We use the \endpoint expression to indicate the endpoint for which the expressions is relevant. The endpoint projection uses this information to decide which endpoint to project an expression to. VeyMont knows a very simple inference rule, which allows us to omit the \endpoint expressions in some cases. Essentially, whenever the endpoint context is directly inferrable from the expression, VeyMont tries to do so. In this case, this shortens the contract to the following:

choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  requires Perm(alex.v, 1) ** Perm(alex.temp, 1);
  requires Perm(bobby.v, 1) ** Perm(bobby.temp, 1);
  run {
    communicate alex.v -> bobby.temp;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

VeyMont verifies the above two examples successfully.

Channel invariants & functional correctness

We will now go one step further and specify functional correctness of the above example. Specifically, we will verify that, if x and y are positive and negative respectively, the fields bobby.v and alex.v will also be positive and negative, respectively, after executing the choreography. We do this by adding a contract to the main choreography, to constrain x and y. We also enhance the contract of run by adding this requirement. This results in the following choreography:

requires x > 0 && y < 0;
choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  requires Perm(alex.v, 1) ** Perm(alex.temp, 1) ** alex.v > 0;
  requires Perm(bobby.v, 1) ** Perm(bobby.temp, 1) ** bobby.v < 0;
  ensures Perm(alex.v, 1) ** alex.v < 0;
  ensures Perm(bobby.v, 1) ** bobby.v > 0;
  run {
    communicate alex.v -> bobby.temp;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

This version does not yet verify. VeyMont reports an error on the postcondition of the above choreograpy, reporting that alex.v and bob.v might not be negative and positive, respectively. Note that this error is discovered only after the choreography is verified! This shows an interesting aspect of VeyMont: at the choreography level, properties over the transferred values are included in the reasoning of VeyMont. While this is only matters for primitive values like integers, it is ocasionally useful for verifying choreographies. Note that, while the generated implementation would not verify, it is not because of a bug: there are simply some annotations missing.

In deductive program verification terms, there is a modularity boundary at the communicate statement, in the sense of modular verification. When verifying the choreography, this modularity boundary is transparent. When verifying the implementation, this modularity boundary is opaque. The decision of when and where to draw the modularity boundary is a topic of ongoing research, and might change in future versions of VeyMont.

We will now finish verifying the implementation by adding a property over the message that is sent. This type of property is specified using a channel invariant. Channel invariants are defined using the channel_invariant keyword, followed by an expression. Channel invariants must directly precede the communicate statement they apply to. Within a channel invariant, the special expressions \msg, \sender and \receiver are available. They refer to the message being sent, the sending and the receiving endpoint, respectively. Within a channel invariant, there can be no endpoint ownership expressions, as the owners are implictly determined by the sending and receiving endpoint.

Adding the constraints as channel invariants results in the following choreography:

requires x > 0 && y < 0;
choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  requires Perm(alex.v, 1) ** Perm(alex.temp, 1) ** alex.v > 0;
  requires Perm(bobby.v, 1) ** Perm(bobby.temp, 1) ** bobby.v < 0;
  ensures Perm(alex.v, 1) ** alex.v < 0;
  ensures Perm(bobby.v, 1) ** bobby.v > 0;
  run {
    channel_invariant \msg > 0;
    communicate alex.v -> bobby.temp;
    channel_invariant \msg < 0;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

The generated implementation of this final version of the choreography verifies.

What next?

More choreographies can be found in the test suite of VeyMont, as well as in the tool papers.

Publications

VeyMont syntax overview

Choreography declarations

  • [contract] choreography Name(parameters...) { choreographic declarations... }

    Defines a choreography named "Name", with zero or more parameters and a body of choreographic declarations. The choreography declaration may be preceded with a contract, which can be used to constrain the arguments.

  • endpoint a = ClassType(args...);

    Defines an endpoint named a of type ClassType. When a is initialized, the constructor of ClassType will be called with arguments args....

  • [contract] run { choreographic statements... }

    The run declaration defines the interactions between endpoints. It contains zero or more choreographic statements.

Choreographic contract expressions

  • (\endpoint a; expr)

    Specifies that expression expr belongs to endpoint a. This means that expression expr will be evaluated in the context of a, using memory only available to a. The endpoint projection also uses this to decide where to project an expression to.

  • (\chor expr)

    Specifies that expression expr belongs to no endpoint in particular. It will be included when verifying the choreography, but when generating an implementation this expression is discarded and replaced with true. This means that the generated implementation might not verify. Essentially, \chor is a debugging construct, similar to the assume statement. It is useful to verify properties at the choreographic while they cannot be verified at the generated implementation level yet.

  • Perm[a](obj.f, p)

    This is shorthand syntax for (\endpoint a; Perm(obj.f, p)).

Choreographic statements

  • channel_invariant expr;

    Specifies a property over a message being sent. Must directly precede a communicate statement.

  • communicate a.f -> b.f;

    Indicates that a message is exchanged between endpoint a and b, the value being the f field of a, the destination being the f field of b.

  • communicate a: message -> b: target;

    Extended form of the communicate statement, with a and b being endpoints, message being the expression of the message to be sent, and target an assignable memory location for which b has write permission.

  • a.f := expr;

    Assigns expr to a.f, in the context of endpoint a. This means VeyMont will report an error if expr tries to read memory that a does not own.

  • a: target := expr;

    Assigns expr to target in the context of endpoint a. Used as a fallback when VeyMont cannot infer the endpoint context directly from target.

Channel invariant expressions

  • \msg

    Refers to the message being sent.

  • \sender, \receiver

    Refer to the sender and receiver of the communicate statement.

Home

Tutorial

Developing for VerCors

Clone this wiki locally