Tsunaou/PolySI

Build

PolySI is tested on Ubuntu 22.04 LTS. Follow the instructions below to build it.

$ sudo apt update
$ sudo apt install g++ openjdk-11-jdk cmake libgmp-dev zlib1g-dev
$ git clone --recurse-submodules https://github.com/amnore/PolySI
$ cd PolySI
$ ./gradlew jar

Usage

After building, there should be a jar file in the build/libs directory. Use this file to run the program.

To verify histories, use the audit command:

$ java -jar PolySI/build/libs/PolySI-1.0.0-SNAPSHOT.jar audit --help
Usage: verifier audit [-hV] [--no-coalescing] [--no-pruning] [-t=<type>] <path>
      <path>            history path
  -h, --help            Show this help message and exit.
      --no-coalescing   disable coalescing
      --no-pruning      disable pruning
  -t, --type=<type>     history type: COBRA, DBCOP, TEXT
  -V, --version         Print version information and exit.

Histories to reproduce the results are in PolySIHistories.

There are three kinds of histories PolySI can accept:

1. Histories generated by Cobra

   This kind of histories contains files like T*.log in a directory. To verify them, pass --type=cobra to this program:

   $ java -jar PolySI/build/libs/PolySI-1.0.0-SNAPSHOT.jar audit --type=cobra PolySIHistories/fig8_9_10/rubis-10000/hist-00000
   

2. Histories generated by DBCop

   These histories are stored in a single file named history.bincode. Use --type=dbcop with the audit command:

   $ java -jar PolySI/build/libs/PolySI-1.0.0-SNAPSHOT.jar audit --type=dbcop PolySIHistories/fig8_9_10/25_400_8_10000_0.3_uniform/hist-00000/history.bincode
   

3. Text format

   These histories are stored in a text file. Each operation occupies one line, with the following format:

   # r means read, w means write
   <r/w>(<key>,<value>,<session_id>,<transaction_id>)
   

   Use --type=text with this kind of histories:

   $ java -jar PolySI/build/libs/PolySI-1.0.0-SNAPSHOT.jar audit --type=text PolySIHistories/violations/galera/galera.txt
   

Program Output

Using PolySIHistories/violations/galera/galera.txt as an example:

...
Conflicts:
Edge: (<(2, 8) -> (1, 3)>,[(RW, 0)])
Edge: (<(1, 3) -> (2, 8)>,[(RW, 0)])
Constraint: SIConstraint((1, 3), (2, 8), [((1, 3) -> (2, 8), WW, 0), ((1, 4) -> (2, 8), RW, 0), ((1, 4) -> (2, 8), RW, 0)], [((2, 8) -> (1, 3), WW, 0)], 17)
Related transactions:
sessionid: 1, id: 4
ops:
READ 0 = 5
...
ENTIRE_EXPERIMENT: 146ms
ONESHOT_CONS: 16ms
...
SI_PRUNE: 20ms
...
SI_SOLVER_GEN: 11ms
...
SI_SOLVER_SOLVE: 0ms
[[[[ REJECT ]]]]

The last line shows whether this program has found a violation in the history. In this case, this history is rejected because a violation is found.

The time used in different steps of verification is printed above. Those corresponding to the numbers in figures are:

Step	Name in figures
ENTIRE_EXPERIMENT	total time
ONESHOT_CONS	constructing
SI_PRUNE	pruning
SI_SOLVER_GEN	encoding
SI_SOLVER_SOLVE	solving

In case of finding a violation, the conflicting transactions are also printed.

Each transaction is printed as (<sesssion id>, <txn id>).

Edge means a known edge <from txn> -> <to txn>, [(<edge type>, <key>) ...].

Constraint means a constraint derived from the history <txn1>, <txn2>, [<new edges if txn1 -ww-> txn2> ...], [<new edges if txn2 -ww-> txn1> ...].

The operations in related transactions are printed as <READ/WRITE> <key> = <value>.