Output

The tool performs a systematic analysis on the application specification given as input. The first part of this analysis is optional and only checks the correctness of the specification. The remaining parts are used to infer which is the correct coordination that should be applied to the application.
If the specification fails any of the specification correction tests the tool stops its analysis as the tests related to consistency can only be executed on correct specifications.

Finally, after the tests are executed, the tool outputs a token model that defines the correct coordination to be applied to the application.

Note: You should always make sure that the input specification passes the correction tests. If it doesn't the results of the consistency tests may not be valid.

Specification Correction Tests

For each test executed the output is a line that specifies the type of test, followed by "PASSED" or "FAILED", and bellow it's printed the output of the execution of the corresponding, automatically generated, Boogie specification used in the test.

For instance:

IMPORTS TEST: (PASSED)
Boogie program verifier finished with 0 verified, 0 errors

These tests are divided into Base Verification tests and Logic Verification tests.

Base Verification

• Imports Test: Verifies the correctness of the imports declared in the input specification.

• Initializer Test: Verifies the correctness of the initializer present in the input specification.

• Variables Test: Verifies the correctness of the variable declarations present the input specification.

• Invariant Test: Verifies the correctness of the invariant present the input specification.

• Operation Tests: Verifies the correctness of operations specifications present in the input specification.

• Full Test: Verifies the correctness of the entire specification at once.

Logic Verification

• Safety Tests: Verifies if all operations in the input specification are safe. An operation is unsafe if it's non-concurrent execution can violate the application's invariant, otherwise it's safe. All operations must be safe for the specification to be correct.

• Absurd Tests: Verifies if any of the operations in the input specification are absurd. An operation is absurd if any of the statements that comprise it are contradictory. No operation can be absurd for the specification to be correct. As an example, an operation with the following effect: a==true && a==falseis absurd.

• Completeness Tests: Verifies if all the operations specifications in the input specification are complete. A operation specification is complete if all variables declared in the input specification have defined values after its execution. All operation specifications must be complete for the specification to be correct. As an example, if the input specification declares a Boogie map as a global variable and an operation states in its modifies field that it modifies said map, then the effects of that operation must fully specify the values of the entire map, for all possible executions.

Consistency Tests

• Opposition Tests: Verifies which pairs of operations have opposing preconditions. If this tests fails for a pair, that pair has opposing preconditions and, therefore, cannot execute concurrently by definition. For pairs that cannot execute currently no coordination is required and, because of this, the following two tests are not executed. As an example, a pair of operations with the following preconditions a==true and a==false, fails this test.

• Stability Tests: Verifies which pairs of operations are stable. Only pairs of operations that are stable can execute concurrently without coordination. The concept of stability is defined HERE TODO: ADD LINK. If a pair fails this tests we already know that it requires coordination and, because of this, the commutativity test is not executed.

• Commutativity Tests: Verifies which pairs of operations are commutative. Only commutative pairs of operations can execute concurrently without coordination.

Coordination Generation

By executing the previous three tests it is already known which pairs of operations need coordination. However, the tool provides a more fine grained approach to coordination then operation based coordination and generates, if possible, parameter based coordination to substitute the operation based coordination already inferred.

Take as an example the operation withdraw(client, amount) from the specification specifications/applications/basic_bank.json present in the repository, which removes a specified amount from a clients bank account.

You can verify that the operation withdraw is not stable when executed with itself by running the tool with this specification as input:

withdraw withdraw STABILITY TEST: (FAILED)

This happens because the tool detects that the invariant of the specification, that all bank accounts must have a credit above of equal to zero, might be violated when two concurrent withdraw operations happen.

But the pair of operations (withdraw, withdraw) is stable if we are sure that the clients both operations are modifying are different. This is what the tool infers and outputs.

withdraw(c1: Client, a1: int) withdraw(c1: Client, a1: int) INEQUALITY SOLVER: (PASSED)
Solutions:
( @1 != @3 )

Here the tool proposes that the first parameter of the first operation (denoted as @1) must be different from the first parameter of the second operation (denoted as @3) for the pair to be able to execute concurrently (@1 is c1 of the first operation, @2 is a1 of the first operation, @3 is c1of the second operation and @4 is a1 of the second operation).

If, during these tests, the tool outputs "FAILED" for a pair of operations it's because the tool wasn't able to find a relationship between the parameters that, when enforced, would stop the conflict.

Finally, this relationships are represented trough a Token Model using two sets:

• Tokens per operations: which tokens are assigned to which operations.
• Token conflicts: for each token, which tokens are in conflict with it.

Note: If you need to enforce multiple restrictions between parameters, the tool will output a line formatted like ( @x != @x && @x != @x ). If you can enforce one restriction or other, the tool will output multiple lines formatted like (@x != @x) , each line being one option.