Protocheck

Protocheck is an application designed to verify various correctness properties of protocols defined in the BSPL family of languages.

Installation

Protocheck may eventually be made available through the PyPI package registry, but for now install it directly from github.

Prerequisites

Protocheck requires python version 3.4 or later, because of one of its dependencies. On Windows, Python 3.6+ is recommended.

Install from source (Gitlab)

1. Download the source code from gitlab:

   $ git clone https://gitlab.com/masr/protocheck.git
       

2. Optionally create virtualenv for protocheck

   $ mkvirtualenv protocheck
       

3. Activate virtualenv (do this whenever you start a new shell session)

   $ workon protocheck
       

4. Install package in development mode

   $ pip install -e ./protocheck
       

Usage

When installed globally, protocheck provides the ‘bspl’ entrypoint, that can be used as follows:

usage: bspl [-h] [-t] [-e] [-d DEPTH] [-s] [-v] [-q] [-f FILTER]
            {projection,path-safety,path-liveness,flow,safety,enactability,liveness,atomicity,all} input [input ...]

BSPL Protocol property checker

positional arguments:
  {path-safety,path-liveness,projection,flow,safety,enactability,liveness,atomicity,all}
                        Primary action to perform
  input                 Protocol description file(s)

optional arguments:
  -h, --help            show this help message and exit
  -t, --tseytin
  -e, --exhaustive      enable heuristics (buggy)
  -d DEPTH, --depth DEPTH
                        Longest transitive relationship to generate. Only need
                        log2(max-chain) to prevent cycles. (default: 1)
  -s, --stats           Print statistics (default: False)
  -v, --verbose         Print additional details: spec, formulas, stats, etc.
                        (default: False)
  -q, --quiet           Prevent printing of violation and formula output
                        (default: False)
  -f FILTER, --filter FILTER
                        Only process protocols matching regexp (default: .*)

‘input’ is the filename of a protocol specification file.

There are some example protocol files in the ‘samples’ directory.

Common Problems

UnicodeEncodeError: ‘charmap’ codec can’t encode character ‘\u2192’ in position 5566: character maps to <undefined>

Protocheck has support for unicode arrow symbols in the protocol specifications. If your terminal does not support unicode characters, you may need to do one of the following workarounds:

Windows

Try one of the following:

1. Try Python 3.6+, which supposedly resolves the issue
2. Run set PYTHONIOENCODING=utf-8 in your shell
3. Try the following:

T:\> py -mpip install win-unicode-console
T:\> py -mrun bspl.py

Other

I haven’t run into this particular error on linux, except in older versions of python. If you still run into it, try

# export PYTHONIOENCODING="utf-8"

Notes

• There are probably still some bugs. If you find a case that doesn’t work as you expect, please record everything with ‘-v’ and submit an issue.
• For easier testing of listings used in latex papers, protocheck will automatically strip latex formatting before parsing a protocol, so they should work without modification.

Tasks

Make model objects independent of parsing pipeline

Currently, the only constructors for Protocol, Message, etc. take a ‘schema’ as input, which is the plain data format produced by the parsing system.

For easier extension and use in tools that generate protocols, it would be better if simpler constructors existed so that the objects could be constructed directly, instead of based on an intermediate data format.

Support multiple recipient roles

Currently, BSPL’s syntax only supports a single recipient role for each message. However, it’s a very simple extension semantically to support multiple recipients, and this would greatly simplify certain applications. Specifically, generating messages that provide the ‘in’ parameters of a dependent protocol for checking refinement currently requires generating one message per recipient, each of which can be interleaved anywhere in the enactment. That’s a very highly combinatorial expansion of possibilities, when they could be condensed to a single message that produces the same information at all of the endpoints. However, each message currently only has one delay parameter. Multiple recipient roles with a single delay would mean that they all observe the information at the same time.