## 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](https://github.com/amnore/PolySIHistories.git).

There are three kinds of histories PolySI can accept:

1. Histories generated by [Cobra](https://github.com/DBCobra/CobraBench)

    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](https://github.com/amnore/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>`.
