Sreeja S Nair

Evaluation of the CEC (Correct Eventual Consistency) Tool

Keywords: Consistency, Verification, Distributed applications Évaluation cohérence, vérification, applications distribuées

Preserving invariants while designing distributed applications under weak consistency models is difficult. The CEC (Correct Eventual Consistency Tool ) is meant to aid the application designer in this task. This report presents some specifications tried out using the tool and some recommendations for its improvement based on the usage experience.

Introduction

The Correct Eventual Consistency (CEC) Tool is based on CISE logic developed by Gotsman et al. [START_REF] Gotsman | Cause I'M Strong Enough: Reasoning About Consistency Choices in Distributed Systems[END_REF]. CISE logic provides reasoning on the correctness of a distributed application operating on top of a causally consistent database. According to the logic, a distributed application is guaranteed to uphold the invariant if each operation is sequentially correct, each operation is stable under the precondition of the other and the operations commute. The assumption of CISE logic is that the application is designed on top of a database layer which ensures causal delivery of updates.

The input to the tool is a specification written in the intermediate verification language, Boogie [START_REF] Boogie | [END_REF], with some annotations required by the tool. The tool performs verification checks on the specification and provides recommendations for synchronization. This report summarizes the evaluation of the tool in terms of ease of use.

We take an example of a simple decrement counter to illustrate the usage of the tool. First we show how to write a specification for a decrement counter normally used in sequential applications. We discuss the result given by the tool in terms of the synchronization recommendations. Then we will go to a better example by designing a counter with escrow. The tool gives some recommendations here as well. As a third step we specify a bounded counter CRDT and examine the result of the tool. We also show an example of a replicated growable array specification using the tool.

The report concludes with our recommendations to enhance the usability of the tool and a discussion on the possible future research and development directions for the tool.

Correct Eventual Consistency tool

Based on the CISE logic, a tool was developed and reported by Najafzadeh et al. [START_REF] Najafzadeh | The CISE Tool: Proving Weakly-consistent Applications Correct[END_REF]. As the authors have pointed out, the CISE tool is difficult to use since the user would need to study Z3 APIs in order to use it [START_REF] Najafzadeh | The Analysis and Co-design of Weakly-Consistent Applications[END_REF]. Marcelino et al. [START_REF] Marcelino | Bringing Hybrid Consistency Closer to Programmers[END_REF] has designed the CEC tool which works on the same principle and uses Boogie [START_REF] Boogie | [END_REF] with some annotations. The language except the annotations is specified by Leino [START_REF] Leino | This is Boogie 2[END_REF]. The annotations are specific to this tool.

A specification consists of the following parts:

• Data structures and properties

• Variables

• Invariants

• Operations with pre and post conditions

The verification is done in two main steps :-specification correction and consistency verification. For each check, a boogie file is generated by the tool using the input specification. Boogie is invoked using these files and the output is examined to determine the status of the check.

The specification correction section checks whether

• each individual component of the specification is correct syntactically (syntax check )

• each operation satisfies the invariant individually (safety check )

• there is any contradictory clause in the specification (anomaly check )

• all variables which are modified by the operations have properly defined values after the execution (completeness check )

The analysis will proceed onto the consistency verification stage only if all the specification correction checks are passed. According to the event based proof rule described by Gotsman et al. [START_REF] Gotsman | Cause I'M Strong Enough: Reasoning About Consistency Choices in Distributed Systems[END_REF], this stage ensures that the consistency of the specification upholds the application invariants. In a distributed application, each operation would be propagated from the replica which it originated from(origin replica) to all other replicas. That means, now the specificatin is sequentially correct at the origin replica.

The consistency verification section checks the pair of operations to see whether

• the pair of operations have opposing preconditions (opposition check )

• the precondition of one operation holds under the other operation (stability check )

• the pair of operations commute (commutativity check )

The ones that fail the opposition check do not need to be analysed further as they will never be executed concurrently. The second and third check in the consistency verification stage deals with the safety of concurrent operations. In case these checks fail, a token generation engine is invoked to generate concurrency tokens for ensuring safety. Currently, the token generator checks whether enforcing inequality on the input parameters would make the specification safe.

Examples

This section describes several examples tried using CEC tool. Each example is provided with a brief description on the context and the specification is explained. The complete sepcification of each example along with the tokens and the output from the tool is shown in the appendix. The specification of each example is examined in four parts:

• Data structures and properties

• Variables

• Invariants

• Operations

Decrement counter

Decrement counter is a count down counter with a lower bound. It is an integer which has increment and decrement operations. The specification can be examined as per the CEC tool input format.

• Data structure and properties

The data structure is int , which is a native datatype supported by Boogie. A constant named min is defined to specify the lower bound which the counter must respect.

• Variables

There is a single variable here, named counter , which is of type int .

• Invariants

The only invariant is that the value of the counter should not be less than min .

• Operations

The operations and the pre and post conditions are as follows:

Inria

increment This function is used to increment counter by value units. The only precondition for this operation is that the value by which the counter should be incremented should be positive.

decrement This function is used to decrease the value of counter by value units. The precondition for this operations is that value should be positive and the current value of the counter is more than min + value .

When we run the CEC tool with this specification, the tool indicates that for sequential applications it works perfectly fine. For the consistency tests, the tool shows that the precondition of decrement operation is not stable under the effect of another decrement operation.

For example, consider a scenario where counter was having a value of 5. The value of min is specified as 0. This means counter cannot decrease beyond 0. Now consider an operation decrement(3) . This operation when done in a sequential program satisfies the invariant. But if the same operation with the same parameter is executed at two different replicas, when the changes are propagated, the value of counter becomes -1, which violates the invariant. So once the operation is executed with the given parameter, a second operation is not possible, because it does not fulfill the precondition. This is the output of the tool. The tool also generates a token indicating that the decrement operation needs strong coordination. The format of the token is as shown below: This also means that the increment operation can be executed without any synchronization. In short, the tool points out the functions which would require synchronization and the application designer needs to implement it.

--------------TOKEN MODEL -------------- Tokens p e
As we have seen, the decrement operation needs strong synchronization. So if a replica wants to perform a decrement , it should acquire a token which locks the counter for any decrement operation. We declare a global variable called lock of datatype ReplicaID which is to be acquired by any replica that needs to perform a decrement operation. We also specify the restriction stating that the decrement function should not originate from the same replica twice, which is based on the fact that causal delivery is ensured by the underlying database.

This leads to an application being unavailable to a user when another user needs to perform the decrement operation.

Decrement counter with escrow

In the counter described in the previous section, the locking happens for all decrement operations irrespective of the value of the counter and the value to be decremented. To overcome this drawback, the concept of escrow transactional model [START_REF] O'neil | The Escrow Transactional Method[END_REF] is used to divide the rights for decrementing the counter between replicas. Najafzadeh [START_REF] Najafzadeh | The Analysis and Co-design of Weakly-Consistent Applications[END_REF] provides a specification for this counter which we reuse here. The specification is as follows:

• Data structures and properties

We have specified two datatypes here namely Credit , of type int, and ReplicaID .

• Variables

The two variables used are localCredit for each replica and globalCredit which is a shared variable.

• Invariants

The localCredit for all replicas and globalCredit should be always non-negative.

• Operations The four operations are defined as follows:

increment This operation increases the local credits of the local replica. The parameters to this operation are the replica , which is the ReplicaID of the local replica and k , the local credits to be added. The only precondition for the operation is that k should be positive.

decrement This operation is the inverse of the increment operation. It decreases the local credits of the local replica. The parameters to this operation are replica and k , the amount of local credits consumed. The preconditions for the operation is that k should be positive and the local replica should have sufficient local credits. The operation ensures that the local credits of replica is decreased by k .

-acquireCredit This operation acquires some credit from the globalCredit and adds it to the localCredit of the replica. The parameters are similar to the previous operations. The precondition of the operation is that there should be sufficient globalCredit for the operation.

The operation ensures k credits to be acquired by the local replica from globalCredit .

-releaseCredit This operation releases the localCredit of replica to globalCredit . The parameters are the same as previous operations with the precondition that the replica has sufficient localCredit . The operation transfers credits from the replica to the globalCredit .

This specification is run against the CEC tool and the tool suggests that the precondition of the following pair of operations are not stable under another execution of the other.

• acquireCredit -acquireCredit • releaseCredit -releaseCredit • releaseCredit -decrement • decrement -decrement
The tokens generated are as follows:

- -------------TOKEN MODEL --------------Tokens p e r o p e r a t i o n s : decrement : decrement_param1 r e l e a s e C r e d i t : r e l e a s e C r e d i t _ p a r a m 1 a c q u i r e C r e d i t : a c q u i r e C r e d i t _ a l l Token c o n f l i c t s : decrement_param1 : decrement_param1 , r e l e a s e C r e d i t _ p a r a m 1 a c q u i r e C r e d i t _ a l l : a c q u i r e C r e d i t _ a l l r e l e a s e C r e d i t _ p a r a m 1 : decrement_param1 , r e l e a s e C r e d i t _ p a r a m 1

Inria

The restrictions which should be imposed here are that none of the pairs originate from the same replica. This makes sense since the CISE logic assumes causal delivery of updates.

This model requires locking only when acquireCredit function is called. We implement a lock similar to the decrement counter in the previous section and add an extra precondition to the acquireCredit function that the lock must be acquired. The tool is now run against the modified specification along with the restrictions and it shows a failure of the pair opposition test for a pair of acquireCredit operations. This makes sense as two acquireCredit operations originating from different replicas cannot run concurrently anymore. This design makes the application more available as the counter can operate seamlessly until each replica has enough local rights.

Decrement counter CRDT

The bounded counter [START_REF] Balegas | Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants[END_REF] is a conflict-free replicated datatype (CRDT) [START_REF] Shapiro | Conflict-free Replicated Data Types[END_REF] which helps to ensure numerical invariants. It is similar to the counter with escrow, but has a different implementation which takes the synchronization off the critical path. Balegas et al. [START_REF] Balegas | Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants[END_REF] specify the design of a statebased CRDT. Instead the specification which we propose below is written as an operation-based CRDT. The specification is for a counter which has a lower bound.

• Data structures and properties

The two datatypes defined are matrix2d and matrix1d for 2-dimensional and 1-dimensional matrices respectively. replicas indicate the number of replicas involved and min is the minimum value the counter should maintain. The matrices R (storing the information of the rights) and U (storing usage information) have dimensions replicas × replicas and replicas × 1 respectively. value and local_rights are computed as per the specification explained by Balegas et al. [START_REF] Balegas | Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants[END_REF].

• Invariants

The value of the counter should be always greater than or equal to the min value specified.

• Operations with pre and post conditions The three effector functions defined are as follows:

increment Increment operation takes two parameters * id -the origin replica * n -the new value of R[id ][ id ] at the origin replica

The prerequisite for the operation is simple, it has to be in a participating replica. The operation will edit the entry of R[id ][ id ] in all the other replicas. The new value will be the sum of n and the existing value of

R[id ][ id ] .
decrement Decrement operation takes the same parameters as the increment operation with the same prerequisites. The operation edits the entry of U[id] , replacing it with the sum of n and the existing value of U[id] .

transfer Transfer operation is used to transfer credit between replicas. The parameters are: * from -the replica from which the credit is transferred * to -the replica to which the credit is transferred Sreeja * n -the new value of the entry R[from][to] at the origin replica

The prerequisite for the operation is that the replica cannot transfer credit to itself and from and to are participating replicas. The operation updates the entry at R[from][to] with the sum of n and the existing value of

R[from][to] .
This specification is run against the CEC tool. The tool shows precondition instability of decrement operation with both decrement operation and transfer operation. The tool also generates the below token which shows that the operation pairs fail when they originate from the same replica.

--------------TOKEN MODEL --------------Tokens p e r o p e r a t i o n s : decrement : decrement_param1 t r a n s f e r : t r a n s f e r _ p a r a m 1 Token c o n f l i c t s : decrement_param1 : decrement_param1 , t r a n s f e r _ p a r a m 1 t r a n s f e r _ p a r a m 1 : decrement_param1

Since the CISE logic assumes causal delivery in the underlying layer of the application specification, we can impose restrictions on the pair of operations to be generated from different replicas.

Improved Decrement counter CRDT

A slight modification of the above counter can result in a design which does not require explicit specification of causal delivery. We emulate the merge function provided in the statebased specification of the bounded counter [START_REF] Balegas | Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants[END_REF]: instead of performing the addition operations on the elements of the matrix, we substitute them by the maximum of the current value and the incoming value. The parameter of the operation is the resultant of the computation performed in the local replica.

Replicated Growable Array

Replicated Growable Array(RGA) is a CRDT used in the context of collaborative editing [START_REF] Roh | Replicated Abstract Data Types: Building Blocks for Collaborative Applications[END_REF]. It proposes a replicated data type for a linked list. Previous works have formally specified RGA and a recent work proved that RGA is eventually consistent [START_REF] Gomes | Verifying Strong Eventual Consistency in Distributed Systems[END_REF]. The proof is based on modeling a network and specifying RGA on top of the model to show that given the network model, RGA eventually converges. Instead, we use the CISE logic to prove RGA correct.

• Data structures and properties ListType represents a map of nodes. A node is represented by a type Ref . The fields of a node are:

content , which contains the value of the node of type Object next , which points to the next node -clock_ins , which is used to store the timestamp for insert operations -clock_up , which stores the timestamp for update/delete operations A variable is initiated, called list , which is of the data type ListType . presence is a variable that helps in tracking the nodes added while using insert operations. Its type is

[Ref]bool .
We define a set of additional objects as follows:

Inria tombstone of type Object , indicating that the object is deleted For each of these fields and special objects, we need to specify the properties. The property of presence flag requires that if a node is present in the list, the next node which it points to must also be present in the list. This ensures that a node already inserted does not point to a node yet to be inserted to the list. For the head and tail nodes, we define the properties as below:

-head of type Ref ,
-clock_ins and clock_up are set to 0 content is set to a tombstone (indicating nothing)

presence to true to show that they will be present in the list For all nodes except the head and tail , the clock_ins and clock_up should have non-zero values. The clock_ins and clock_up are meant to have information about the origin replica and the time of the operation. Hence it is guaranteed that no two clock_ins or clock_up would be equal.

The support functions and their functionalities are describes as follows:

-create_node creates a new node and returns it. The created node will neither be a head nor the tail and the function will never return the same object if either the content or the timestamp of the object differs.

-get_actual_reference returns the exact location where the insert operation can insert a new node. The node to be inserted is to be placed to the right side of the base node but after the nodes which are inserted later at the same place. The nodes inserted later will have a greater value for the clock. Until it finds a node such that the next of the node has a clock value lesser than the current operation clock value, it goes on searching recursively.

-is_successor checks whether the parameters successor has a connection from the parameter base . This function is used to define the property of the list that the list should start from the head and end in the tail.

The property that no two nodes have the same next has been specified to avoid circles in the list and enforces the list to be linear.

• Invariants

The invariants of a linked list are only two :

-A head should be present -A tail should be present

• Operations with pre and post conditions

The four operations are insert , update , delete and read . The following shows the pre and post conditions of each operation along with the variables it modifies.

insert Insert operation takes three parameters

The preconditions for the operation are that base is not a tail and base is already present in the list . This operation modifies list by updating content of base node to obj and updating clock_up . This modification happens only when clock_up of the node is less than the operation timestamp, else it returns the same list without any modifications.

delete Delete operation takes two parameters * base -the node to be deleted * time -the number indicating the origin replica and the timestamp of the operation

The preconditions for the operation are the same as that of the update operation. The only difference between update and delete operations is that the content of the base node is updated to a tombstone .

read Read operation takes only the node of which the value is to be returned, base , as the input. The preconditions are similar to update and delete and it does not have any impact on the list.

The tool is run with the specification input. The following are the issues pointed out by the tool:

• insert -insert stability issue • delete -update commutativity issue • update -update commutativity issue

Inria

The tokens generated by the solver is as follows:

--------------TOKEN MODEL --------------Tokens p e r o p e r a t i o n s : update : update_param3 i n s e r t : insert_param3 d e l e t e : delete_param2 Token c o n f l i c t s : delete_param2 : update_param3 insert_param3 : insert_param3 update_param3 : delete_param2 , update_param3

The tokens indicated as in the same notation as we specified earlier. We know that no two timestamps for a pair of operations would be equal. When we specify this restriction, the verification succeeds.

Conclusion

The Correct Eventual Consistency (CEC) tool was used to specify some sample replicated data structures. We showed how the tool captured the behaviours of different implementations of a decrement counter and also the replicated growable array.

From the experience gained from the tool usage, we suggest the following improvements to the tool (in decreasing order of the usefulness), categorized into sections:

• Debugging support

As of now, the tool gives information on the result of the test -pass or fail, along with an error trace from boogie. For the user, who is not aware of the intermediate boogie files generated by the tool, the error traces are not useful. To support the debugging experience, we need to see how to provide useful information for each step of verification. The following are the suggestions for each step:

-Specification correction * Syntax check Boogie check provides the exact position of the syntax issue in the input file. Since the tool is reordering the format of the specification before sending it to Boogie, it would be useful to remap the error position to the position in the specification given by the user. This information is quite sufficient for identifying the issue. * Safety check A counter example can help to understand more about the issue which violates the invariant. Further to that the invariant specified by the user can be broken down and fed to the Z3 solver to narrow down what exactly caused the violation.

In some cases, strengthening the preconditions might be needed. The weakest precondition calculus can be used to derive the weakest precondition. The derived precondition needs to be a subset of the specified precondition. The precondition might need further strengthening in some cases though. * Anomaly check This is the trickiest check to debug. This test is designed in a way that the test fails if the boogie verification succeeds, thereby having no error trace and counter model generated. This leads to a situation where the user cannot get a counter example or any pointer to the failure. We have to devise an approach to find a good solution for debugging this test. * Completeness check Completeness check fails when the user doesn't specify all the components of the variables modified in the procedure. If we can point out exactly the list of components left out, it would be useful. The old and new values obtained from the counter model can be used here to point out the components whose behavior is to be specified.

-Consistency verification * Opposition check This checks whether the preconditions are disjoint sets. This is modeled in a way similar to the anomaly check and hence it is difficult to have a support in debugging.

* Stability check

The debugging support for this step can be modeled as the same in the case of the safety check.

* Commutativity check

This step can borrow the ideas from the completeness check.

• Counter example comprehension

Once the verification fails, the previous step will allow the user to identify the category of issue with the specification, like whether the individual safety test failed. Apart from this, a counter example will also help the user to understand more about the issue with the specification. For this, the feature of counter models which are generated by the SMT solve Z3, can be used. As a first level information, the parameters of the failed operation along with the values of the components in the invariant can be displayed. If the user wishes to know the state of the global variables before and after the execution of the operation, that can be provided as well. Boogie's "CaptureState" functionality can help here.

• Experimentation platform

The idea is to host the tool as a service and collect usage logs. The platform can be used as part of some coursework for the students to experiment application and/or data structure specifications. The logs can be stored and examined offline. This will help in identifying the bottlenecks in specification writing. It will also be useful later in studying the patterns in specifications.

• Token generation -The current token generation part takes a huge amount of time to suggest tokens, especially when the number of parameters are more. This needs to be optimised. The counter example generated from the previous step might be useful here to narrow down the search space of the tokens.

-The token generator only generates tokens for inequality of parameters. It can be made to handle other relations as well.

-The token generator suggests tokens by restricting the parameters. When the parameters are structured data types, this leads to a coarse locking, even if only a particular component only needs to be taken into account. This can be extended to support token generation in a finer level, considering the components of the structured data types.

Inria

• Easier specification

While writing the specification, the part which needed the most effort is the specification of properties, especially when the data types of the variables are complex data structures. If some support system is present to aid the programmers in guiding them to write the correct minimal properties, it would make the tool easier to use. Some possible approaches are:

-Generate specification (or the axioms of the specification) from the code and/or test cases -Provide a set of libraries for the usual special objects defined in the properties, such as "null".

-Identify different patterns for properties and provide reusable code snippets.

• Supporting state-based datatypes

The current version of the tool supports the specification in the form of operation-based replicated data types. This can be extended to support the verification of state-based replicated data types as well. The extended version needs to check whether -Each operation including the merge is sequentially safe -The precondition of merge is stable under itself merge is commutative

A Specification inputs to the tool and the corresponding output o p e r a t i o n 1 " : " decrement " , " o p e r a t i o n 2 " : " decrement " , " r e s t r i c t i o n s " : [ "@1 != @3" ] } ] ------------BASE VERIFICATION------------- ------------ @equals [ R e p l i c a I D ] C r e d i t @as f o r a l l r : R e p l i c a I D : : @ t h i s [ r ] == @other [ r ] ; @equals C r e d i t @as @ t h i s == @other ; @ i n v a r i a n t o p e r a t i o n 1 " : " r e l e a s e C r e d i t " , " o p e r a t i o n 2 " : " r e l e a s e C r e d i t " , " r e s t r i c t i o n s " : [ "@1 != @3" ] } , { " o p e r a t i o n 1 " : " decrement " , " o p e r a t i o n 2 " : " decrement " , " r e s t r i c t i o n s " : [ "@1 != @3" ] } , { " o p e r a t i o n 1 " : " a c q u i r e C r e d i t " , " o p e r a t i o n 2 " : " a c q u i r e C r e d i t " , " r e s t r i c t i o n s " : [ "@1 != @3" ] } , { " o p e r a t i o n 1 " : " r e l e a s e C r e d i t " , " o p e r a t i o n 2 " : " decrement " , " r e s t r i c t i o n s " : [ "@1 != @3" ] } ] ------------BASE VERIFICATION------------- --------------LOGIC VERIFICATION------------- --------------RESTRICTIONS VERIFICATION------------- ------------r --------------PAIR COMMUTATIVITY VERIFICATION-------------r e l e a s e C r e d i t r e l e a s e C r e d i t COMMUTATIVITY TEST : (PASSED) decrement decrement COMMUTATIVITY TEST : (PASSED) r e l e a s e C r e d i t decrement COMMUTATIVITY TEST : (PASSED) a c q u i r e C r e d i t r e l e a s e C r e d i t COMMUTATIVITY TEST : (PASSED) a c q u i r e C r e d i t i n c r e m e n t COMMUTATIVITY TEST : (PASSED) a c q u i r e C r e d i t decrement COMMUTATIVITY TEST : (PASSED) r e l e a s e C r e d i t i n c r e m e n t COMMUTATIVITY TEST : (PASSED) i n c r e m e n t i n c r e m e n t COMMUTATIVITY TEST : (PASSED) i n c r e m e n t decrement COMMUTATIVITY TEST : (PASSED) --------------EQUALITY SOLVER----------------------------TOKEN MODEL ------------- @import ; Inria Sreeja @ o p e r a t i o n s procedure i n c r e m e n t ( i d : int , n : i n t ) modifies R; requires n > 0 && i d >= 0 && i d < r e p l i c a s ; ensures i n c r e m e n t _ e f f e c t (R, old (R) , id , n ) ; procedure decrement ( i d : int , n : i n t ) modifies U; requires n > 0 && i d >= 0 && i d < r e p l i c a s && l o c a l _ r i g h t s ( id , R, U) >= n ; ensures d e c r e m e n t _ e f f e c t (U, old (U) , id , n ) ; procedure t r a n s f e r ( from : int , t o : int , n : i n t ) modifies R; requires n > 0 && from >= 0 && from < r e p l i c a s && t o >= 0 && t o < r e p l i c a s && from != t o && l o c a l _ r i g h t s ( from , R, U) >= n ; ensures t r a n s f e r _ e f f e c t (R, old (R) , from , to , n ) ;

Result ############## SPECIFICATION CORRECTION TESTS ############## --
--------------RESTRICTIONS VERIFICATION-------------- RESTRICTIONS WERE LOADED CORRECTLY ############## CONSISTENCY TESTS ############## --------------PAIR OPPOSITION VERIFICATION-
Result ############## SPECIFICATION CORRECTION TESTS ############## --
- RESTRICTIONS WERE LOADED CORRECTLY ############## CONSISTENCY TESTS ############## --------------PAIR OPPOSITION VERIFICATION-
Token [ { "
o p e r a t i o n 1 " : " decrement " , " o p e r a t i o n 2 " : " decrement " , " r e s t r i c t i o n s " : [ "@1 != @3" ] } , { " o p e r a t i o n 1 " : " decrement " , " o p e r a t i o n 2 " : " t r a n s f e r " , " r e s t r i c t i o n s " : ------------BASE VERIFICATION------------- --------------LOGIC VERIFICATION-------------i @import ; @ i n i t type matrix2d =[ i n t ] [ i n t ] i n t ; type matrix1d =[ i n t ] i n t ; const r e p l i c a s : i n t ; const min : i n t ;

[ "@1 != @3" ] } ] Result ############## SPECIFICATION CORRECTION TESTS ############## --
--------------RESTRICTIONS VERIFICATION-------------- Inria RESTRICTIONS WERE LOADED CORRECTLY ############## CONSISTENCY TESTS ############## --------------PAIR OPPOSITION VERIFICATION-------------- decrement decrement

Token

There are no tokens required for this specification. @equals L i s t T y p e @as f o r a l l r : Ref :

Result ############## SPECIFICATION CORRECTION TESTS ############## --------------BASE VERIFICATION------------
: @ t h i s [ r ] [ c l o c k _ i n s ] == @other [ r ] [ c l o c k _ i n s ] && @ t h i s [ r ] [ clock_up ] == @other [ r ] [ clock_up ] && @ t h i s [ r ] [ c o n t e n t ] == @other [ r ] [ c o n t e n t ] && @ t h i s [ r ] [ n e x t ] == @other [ r ]
[ n e x t ] ; @equals Fl a g @as f o r a l l r : Ref : : @ t h i s [ r ] == @other [ r ] ; @ i n v a r i a n t

  r o p e r a t i o n s : decrement : d e c r e m e n t _ a l l Token c o n f l i c t s : d e c r e m e n t _ a l l : d e c r e m e n t _ a l l

  indicating the start of the list tail of type Ref , indicating the end of the list

A. 1

 1 Decrement Counter Specification @import ; @ i n i t type R e p l i c a I D ; const min : i n t ; @ v a r i a b l e s var c o u n t e r : i n t ; var l o c k : R e p l i c a I D ; @ i n v a r i a n t c o u n t e r >= min ; @ o p e r a t i o n s procedure i n c r e m e n t ( r e p l i c a : R e p l i c a I D , v a l u e : i n t ) modifies c o u n t e r ; requires v a l u e > 0 ; ensures c o u n t e r == old ( c o u n t e r ) + v a l u e ; procedure decrement ( r e p l i c a : R e p l i c a I D , v a l u e : i n t ) modifies c o u n t e r ; requires v a l u e > 0 && ( c o u n t e r >= v a l u e + min ) && l o c k == r e p l i c a ; ensures c o u n t e r == old ( c o u n t e r ) -v a l u e ;

  -IMPORTS TEST : (PASSED) INITIALIZER TEST : (PASSED) VARIABLES TEST : (PASSED) INVARIANTS TEST : (PASSED) decrement OPERATION TEST : (PASSED) i n c r e m e n t OPERATION TEST : (PASSED) FULL TEST : (PASSED) --------------LOGIC VERIFICATION-------------decrement SAFETY TEST : (PASSED) i n c r e m e n t SAFETY TEST : (PASSED) decrement ABSURD TEST : (PASSED) i n c r e m e n t ABSURD TEST : (PASSED) RR n°9111 Sreeja decrement COMPLETENESS TEST : (PASSED) i n c r e m e n t COMPLETENESS TEST : (PASSED)

  decrement decrement OPPOSITION TEST : (FAILED) i n c r e m e n t i n c r e m e n t OPPOSITION TEST : (PASSED) i n c r e m e n t decrement OPPOSITION TEST : (PASSED) --------------PAIR STABILITY VERIFICATION-------------i n c r e m e n t i n c r e m e n t STABILITY TEST : (PASSED) i n c r e m e n t decrement STABILITY TEST : (PASSED) --------------PAIR COMMUTATIVITY VERIFICATION-------------i n c r e m e n t i n c r e m e n t COMMUTATIVITY TEST : (PASSED) i n c r e m e n t decrement COMMUTATIVITY TEST : (PASSED) --------------EQUALITY SOLVER----------------------------TOKEN MODEL --------------Tokens p e r o p e r a t i o n s : Token c o n f l i c t s : A.2 Decrement Counter with escrow Specification @import ; @ i n i t type C r e d i t = i n t ; type R e p l i c a I D ; @ v a r i a b l e s var l o c a l C r e d i t : [ R e p l i c a I D ] C r e d i t ; var g l o b a l C r e d i t : C r e d i t ; var l : R e p l i c a I D ;

  ( f o r a l l r : R e p l i c a I D : : l o c a l C r e d i t [ r ] >= 0 ) && ( g l o b a l C r e d i t >= 0 ) ; @ o p e r a t i o n s procedure a c q u i r e C r e d i t ( r e p l i c a : R e p l i c a I D , k : C r e d i t ) modifies g l o b a l C r e d i t , l o c a l C r e d i t ; requires k > 0 && g l o b a l C r e d i t >= k && l == r e p l i c a ; ensures ( f o r a l l r : R e p l i c a I D : : ( r == r e p l i c a ==> l o c a l C r e d i t [ r ] == old ( l o c a l C r e d i t ) [ r ] + k ) && ( r != r e p l i c a ==> l o c a l C r e d i t [ r ] == old ( l o c a l C r e d i t ) [ r ] ) ) && g l o b a l C r e d i t == old ( g l o b a l C r e d i t ) -k ; procedure r e l e a s e C r e d i t ( r e p l i c a : R e p l i c a I D , k : C r e d i t ) modifies g l o b a l C r e d i t , l o c a l C r e d i t ; requires k > 0 && l o c a l C r e d i t [ r e p l i c a ] >= k ; Inria ensures ( f o r a l l r : R e p l i c a I D : : ( r == r e p l i c a ==> l o c a l C r e d i t [ r ] == old ( l o c a l C r e d i t ) [ r ] -k ) && ( r != r e p l i c a ==> l o c a l C r e d i t [ r ] == old ( l o c a l C r e d i t ) [ r ] ) ) && g l o b a l C r e d i t == old ( g l o b a l C r e d i t ) + k ; procedure i n c r e m e n t ( r e p l i c a : R e p l i c a I D , k : C r e d i t ) modifies l o c a l C r e d i t ; requires k > 0 ; ensures f o r a l l r : R e p l i c a I D : : ( r == r e p l i c a ==> l o c a l C r e d i t [ r ] == old ( l o c a l C r e d i t ) [ r ] + k ) && ( r != r e p l i c a ==> l o c a l C r e d i t [ r ] == old ( l o c a l C r e d i t ) [ r ] ) ; procedure decrement ( r e p l i c a : R e p l i c a I D , k : C r e d i t ) modifies l o c a l C r e d i t ; requires k > 0 && l o c a l C r e d i t [ r e p l i c a ] >= k ; ensures f o r a l l r : R e p l i c a I D : : ( r == r e p l i c a ==> l o c a l C r e d i t [ r ] == old ( l o c a l C r e d i t ) [ r ] -k ) && ( r != r e p l i c a ==> l o c a l C r e d i t [ r ] == old ( l o c a l C r e d i t ) [ r ] ) ;

  -IMPORTS TEST : (PASSED) INITIALIZER TEST : (PASSED) VARIABLES TEST : (PASSED) INVARIANTS TEST : (PASSED) decrement OPERATION TEST : (PASSED) a c q u i r e C r e d i t OPERATION TEST : (PASSED) i n c r e m e n t OPERATION TEST : (PASSED) r e l e a s e C r e d i t OPERATION TEST : (PASSED) FULL TEST : (PASSED)

  decrement SAFETY TEST : (PASSED) a c q u i r e C r e d i t SAFETY TEST : (PASSED) i n c r e m e n t SAFETY TEST : (PASSED) r e l e a s e C r e d i t SAFETY TEST : (PASSED) RR n°9111 Sreeja decrement ABSURD TEST : (PASSED) a c q u i r e C r e d i t ABSURD TEST : (PASSED) i n c r e m e n t ABSURD TEST : (PASSED) r e l e a s e C r e d i t ABSURD TEST : (PASSED) decrement COMPLETENESS TEST : (PASSED) a c q u i r e C r e d i t COMPLETENESS TEST : (PASSED) i n c r e m e n t COMPLETENESS TEST : (PASSED) r e l e a s e C r e d i t COMPLETENESS TEST : (PASSED)

  e l e a s e C r e d i t r e l e a s e C r e d i t OPPOSITION TEST : (PASSED) decrement decrement OPPOSITION TEST : (PASSED) a c q u i r e C r e d i t a c q u i r e C r e d i t OPPOSITION TEST : (FAILED) r e l e a s e C r e d i t decrement OPPOSITION TEST : (PASSED) a c q u i r e C r e d i t r e l e a s e C r e d i t OPPOSITION TEST : (PASSED) a c q u i r e C r e d i t i n c r e m e n t OPPOSITION TEST : (PASSED) a c q u i r e C r e d i t decrement OPPOSITION TEST : (PASSED) r e l e a s e C r e d i t i n c r e m e n t OPPOSITION TEST : (PASSED) i n c r e m e n t i n c r e m e n t OPPOSITION TEST : (PASSED) i n c r e m e n t decrement OPPOSITION TEST : (PASSED) --------------PAIR STABILITY VERIFICATION-------------r e l e a s e C r e d i t r e l e a s e C r e d i t STABILITY TEST : (PASSED) decrement decrement STABILITY TEST : (PASSED) r e l e a s e C r e d i t decrement STABILITY TEST : (PASSED) a c q u i r e C r e d i t r e l e a s e C r e d i t STABILITY TEST : (PASSED) a c q u i r e C r e d i t i n c r e m e n t STABILITY TEST : (PASSED) a c q u i r e C r e d i t decrement STABILITY TEST : (PASSED) r e l e a s e C r e d i t i n c r e m e n t STABILITY TEST : (PASSED) i n c r e m e n t i n c r e m e n t STABILITY TEST : (PASSED) i n c r e m e n t decrement STABILITY TEST : (PASSED)

-

  Tokens p e r o p e r a t i o n s : Token c o n f l i c t s : A.3 Bounded Counter Specification 1

  -IMPORTS TEST : (PASSED) INITIALIZER TEST : (PASSED) VARIABLES TEST : (PASSED) INVARIANTS TEST : (PASSED) i n c r e m e n t OPERATION TEST : (PASSED) t r a n s f e r OPERATION TEST : (PASSED) decrement OPERATION TEST : (PASSED) FULL TEST : (PASSED)

  n c r e m e n t SAFETY TEST : (PASSED) t r a n s f e r SAFETY TEST : (PASSED) decrement SAFETY TEST : (PASSED) i n c r e m e n t ABSURD TEST : (PASSED) t r a n s f e r ABSURD TEST : (PASSED) decrement ABSURD TEST : (PASSED) i n c r e m e n t COMPLETENESS TEST : (PASSED) t r a n s f e r COMPLETENESS TEST : (PASSED) decrement COMPLETENESS TEST : (PASSED)

  OPPOSITION TEST : (PASSED) decrement t r a n s f e r OPPOSITION TEST : (PASSED) i n c r e m e n t i n c r e m e n t OPPOSITION TEST : (PASSED) i n c r e m e n t decrement OPPOSITION TEST : (PASSED) i n c r e m e n t t r a n s f e r OPPOSITION TEST : (PASSED) t r a n s f e r t r a n s f e r OPPOSITION TEST : (PASSED) --------------PAIR STABILITY VERIFICATION-------------decrement decrement STABILITY TEST : (PASSED) decrement t r a n s f e r STABILITY TEST : (PASSED) i n c r e m e n t i n c r e m e n t STABILITY TEST : (PASSED) i n c r e m e n t decrement STABILITY TEST : (PASSED) i n c r e m e n t t r a n s f e r STABILITY TEST : (PASSED) t r a n s f e r t r a n s f e r STABILITY TEST : (PASSED)--------------PAIR COMMUTATIVITY VERIFICATION--------------decrement decrement COMMUTATIVITY TEST : (PASSED) decrement t r a n s f e r COMMUTATIVITY TEST : (PASSED) i n c r e m e n t i n c r e m e n t COMMUTATIVITY TEST : (PASSED) i n c r e m e n t decrement COMMUTATIVITY TEST : (PASSED) i n c r e m e n t t r a n s f e r COMMUTATIVITY TEST : (PASSED) t r a n s f e r t r a n s f e r COMMUTATIVITY TEST : (PASSED)--------------EQUALITY SOLVER----------------------------TOKEN MODEL --------------Tokens p e r o p e r a t i o n s : Token c o n f l i c t s : A.4 Modified Bounded Counter Specification 1

axiom ( f o r a l l

  r : int , U: matrix1d : : r >= 0 && r < r e p l i c a s ==> U[ r ] >= 0 ) ; axiom ( f o r a l l r1 , r 2 : int , R : matrix2d : : r 1 >= 0 && r 1 < r e p l i c a s && r 2 >= 0 && r 2 < r e p l i c a s ==> R[ r 1 ] [ r 2 ] >= 0 ) ; axiom ( r e p l i c a s > 0 && r e p l i c a s < 9 9 ) ; function v a l u e (R: matrix2d , U: matrix1d ) returns ( i n t ) { min + diagonal_sum (R, 0 ) + sum (U, 0 ) } function diagonal_sum (R: matrix2d , i n d e x : i n t ) returns ( i n t ) { i f i n d e x < r e p l i c a s then (R[ i n d e x ] [ i n d e x ] + diagonal_sum (R, i n d e x + 1 ) ) e l s e ( 0 )

  --IMPORTS TEST : (PASSED) INITIALIZER TEST : (PASSED) VARIABLES TEST : (PASSED) INVARIANTS TEST : (PASSED) i n c r e m e n t OPERATION TEST : (PASSED) t r a n s f e r OPERATION TEST : (PASSED) decrement OPERATION TEST : (PASSED) FULL TEST : (PASSED)--------------LOGIC VERIFICATION-------------in c r e m e n t SAFETY TEST : (PASSED) t r a n s f e r SAFETY TEST : (PASSED) decrement SAFETY TEST : (PASSED) i n c r e m e n t ABSURD TEST : (PASSED) t r a n s f e r ABSURD TEST : (PASSED) decrement ABSURD TEST : (PASSED) i n c r e m e n t COMPLETENESS TEST : (PASSED) t r a n s f e r COMPLETENESS TEST : (PASSED) decrement COMPLETENESS TEST : (PASSED) ############## CONSISTENCY TESTS ############## --------------PAIR OPPOSITION VERIFICATION-------------i n c r e m e n t i n c r e m e n t OPPOSITION TEST : (PASSED) i n c r e m e n t decrement OPPOSITION TEST : (PASSED) i n c r e m e n t t r a n s f e r OPPOSITION TEST : (PASSED) decrement decrement OPPOSITION TEST : (PASSED) decrement t r a n s f e r OPPOSITION TEST : (PASSED) t r a n s f e r t r a n s f e r OPPOSITION TEST : (PASSED) --------------PAIR STABILITY VERIFICATION-------------i n c r e m e n t i n c r e m e n t STABILITY TEST : (PASSED) i n c r e m e n t decrement STABILITY TEST : (PASSED) i n c r e m e n t t r a n s f e r STABILITY TEST : (PASSED) decrement decrement STABILITY TEST : (PASSED) decrement t r a n s f e r STABILITY TEST : (PASSED) t r a n s f e r t r a n s f e r STABILITY TEST : (PASSED) --------------PAIR COMMUTATIVITY VERIFICATION-------------i n c r e m e n t i n c r e m e n t COMMUTATIVITY TEST : (PASSED) i n c r e m e n t decrement COMMUTATIVITY TEST : (PASSED) i n c r e m e n t t r a n s f e r COMMUTATIVITY TEST : (PASSED) decrement decrement COMMUTATIVITY TEST : (PASSED) decrement t r a n s f e r COMMUTATIVITY TEST : (PASSED) t r a n s f e r t r a n s f e r COMMUTATIVITY TEST : (PASSED) --------------EQUALITY SOLVER----------------------------TOKEN MODEL --------------Tokens p e r o p e r a t i o n s : type O b j e c t ; type Ref ; type F i e l d a ; type L i s t T y p e = [ Ref ]<a >[ F i e l d a ] a ; type F l a g = [ Ref ] bool ; const unique c o n t e n t : F i e l d O b j e c t ; const unique n e x t : F i e l d Ref ; const unique c l o c k _ i n s : F i e l d i n t ; const unique clock_up : F i e l d i n t ; const tombstone : O b j e c t ; const head : Ref ; const t a i l : Ref ; function c r e a t e _ n o d e ( o b j : Object , time : i n t ) returns ( r e s u l t : Ref ) ; function g e t _ a c t u a l _ r e f e r e n c e ( l i s t : ListType , b a s e : Ref , time : i n t ) returns ( r e s u l t : Ref ) { i f ( l i s t [ l i s t [ b a s e ] [ n e x t ] ] [ c l o c k _ i n s ] < time ) then ( b a s e ) e l s e ( g e t _ a c t u a l _ r e f e r e n c e ( l i s t , l i s t [ b a s e ] [ n e x t ] , time ) ) } function i s _ s u c c e s s o r ( l i s t : ListType , b a s e : Ref , s u c c e s s o r : Ref ) returns ( r e s u l t : bool ) { l i s t [ b a s e ] [ n e x t ] == s u c c e s s o r | | i s _ s u c c e s s o r ( l i s t , l i s t [ b a s e ] [ n e x t ] , s u c c e s s o r ) } axiom ( f o r a l l l i s t : ListType , p r e s e n c e : Flag , r : Ref : : p r e s e n c e [ r ] == p r e s e n c e [ l i s t [ r ] [ n e x t ] ] ) ; axiom ( f o r a l l l i s t : ListType , p r e s e n c e : F l a g : : l i s t [ t a i l ] [ c o n t e n t ] == tombstone && l i s t [ t a i l ] [ c l o c k _ i n s ] == 0 && l i s t [ t a i l ] [ clock_up ] == 0 && l i s t [ t a i l ] [ n e x t ] == t a i l && p r e s e n c e [ t a i l ] == true ) ; axiom ( f o r a l l l i s t : ListType , p r e s e n c e : F l a g : : l i s t [ head ] [ c o n t e n t ] == tombstone && l i s t [ head ] [ c l o c k _ i n s ] == 0 && l i s t [ head ] [ clock_up ] == 0 && p r e s e n c e [ head ] == true ) ; axiom ( f o r a l l l i s t : ListType , p r e s e n c e : Flag , r : Ref : : r != t a i l && r != head && p r e s e n c e [ r ] == true ==> l i s t [ r ] [ c l o c k _ i n s ] > 0 && l i s t [ r ] [ clock_up ] > 0 ) ; axiom ( f o r a l l l i s t : ListType , r1 , r 2 : Ref : : r 1 != head && r 2 != head && r 1 != t a i l && r 2 != t a i l && r 1 != r 2 ==> l i s t [ r 1 ] [ clock_up ] != l i s t [ r 2 ] [ clock_up ] && l i s t [ r 1 ] [ c l o c k _ i n s ] != l i s t [ r 2 ] [ c l o c k _ i n s ] ) ; axiom ( f o r a l l obj1 , o b j 2 : Object , time1 , time2 : i n t : : ( o b j 1 != o b j 2 | | time1 != time2 ==> c r e a t e _ n o d e ( obj1 , time1 ) != c r e a t e _ n o d e ( obj2 , time2 ) ) && ( o b j 1 == o b j 2 && time1 == time2 ==> c r e a t e _ n o d e ( obj1 , time1 ) == c r e a t e _ n o d e ( obj2 , time2 ) ) ) ; axiom ( f o r a l l o b j : Object , time : i n t : : c r e a t e _ n o d e ( obj , time ) != head && c r e a t e _ n o d e ( obj , time ) != t a i l ) ; axiom ( f o r a l l l i s t : ListType , p r e s e n c e : Flag , r1 , r 2 : Ref : : r 1 != t a i l && r 2 != t a i l && r 1 != r 2 && p r e s e n c e [ r 1 ] == true && p r e s e n c e [ r 2 ] == true ==> l i s t [ r 1 ] [ n e x t ] != l i s t [ r 2 ] [ n e x t ] ) ; axiom ( f o r a l l l i s t : ListType , p r e s e n c e : Flag , r : Ref : : p r e s e n c e [ r ] == true ==> i s _ s u c c e s s o r ( l i s t , r , t a i l ) ) ; axiom ( f o r a l l l i s t : ListType , p r e s e n c e : Flag , r : Ref : : p r e s e n c e [ r ] == true ==> i s _ s u c c e s s o r ( l i s t , head , r ) ) ; @ v a r i a b l e s Inria var l i s t : L i s t T y p e ; var p r e s e n c e : Fl a g ;

  ( e x i s t s r : Ref : : p r e s e n c e [ r ] == true && l i s t [ head ] [ n e x t ] == r ) && ( e x i s t s r : Ref : : p r e s e n c e [ r ] == true && l i s t [ r ] [ n e x t ] == t a i l ) ; @ o p e r a t i o n s procedure d e l e t e ( b a s e : Ref , time : i n t ) modifies l i s t ; requires ( b a s e != t a i l ) && ( p r e s e n c e [ b a s e ] == true ) ; ensures ( f o r a l l r : Ref : : ( r == b a s e && old ( l i s t ) [ b a s e ] [ clock_up ] < time ==> l i s t [ r ] [ c o n t e n t ] == tombstone && l i s t [ r ] [ clock_up ] == time ) && ( r != b a s e | | old ( l i s t ) [ b a s e ] [ clock_up ] >= time ==> l i s t [ r ] [ c o n t e n t ] == old( l i s t ) [ r ] [ c o n t e n t ] && l i s t [ r ] [ clock_up ] == old ( l i s t ) [ r ] [ clock_up ] ) && l i s t [ r ] [ n e x t ] == old ( l i s t ) [ r ] [ n e x t ] && l i s t [ r ] [ c l o c k _ i n s ] == old ( l i s t ) [ r ] [ c l o c k _ i n s ] ) ;procedure update ( b a s e : Ref , o b j : Object , time : i n t ) modifies l i s t ; requires ( b a s e != t a i l ) && ( p r e s e n c e [ b a s e ] == true ) ; ensures ( f o r a l l r : Ref : : ( r == b a s e && old ( li s t ) [ r ] [ clock_up ] < time ==> l i s t [ r ] [ c o n t e n t ] == o b j && l i s t [ r ] [ clock_up ] == time ) && ( r != b a s e | | old ( l i s t ) [ r ] [ clock_up ] >= time ==> l i s t [ r ] [ c o n t e n t ] == old ( l i s t ) [ r ] [ c o n t e n t ] && l i s t [ r ] [ clock_up ] == old ( l i s t ) [ r ] [ clock_up ] ) && l i s t [ r ] [ n e x t ] == old ( l i s t ) [ r ] [ n e x t ] && l i s t [ r ] [ c l o c k _ i n s ] == old ( l i s t ) [ r ] [ c l o c k _ i n s ] ) ;procedure r e a d ( b a s e : Ref ) requires ( b a s e != t a i l ) && ( p r e s e n c e [ b a s e ] == true ) ; procedure i n s e r t ( b a s e : Ref , new : Object , time : i n t ) modifies l i s t , p r e s e n c e ; requires ( b a s e != t a i l ) && ( p r e s e n c e [ b a s e ] == true ) && ( new != tombstone ) && ( p r e s e n c e [ c r e a t e _ n o d e ( new , time ) ] == f a l s e ) && ( c r e a t e _ n o d e ( new , time ) != b a s e ) ; ensures ( f o r a l l r : Ref : : ( r == g e t _ a c t u a l _ r e f e r e n c e ( old ( l i s t ) , base , time ) ==>l i s t [ r ] [ c l o c k _ i n s ] == old ( l i s t ) [ r ] [ c l o c k _ i n s ] && l i s t [ r ] [ clock_up ] == old ( l i s t ) [ r ] [ clock_up ] && l i s t [ r ] [ n e x t ] == cr e a t e _ n o d e ( new , time ) && l i s t [ r ] [ c o n t e n t ] == old ( l i s t ) [ r ] [ c o n t e n t ] ) && ( r == c r e a t e _ n o d e ( new , time ) ==> l i s t [ r ] [ c l o c k _ i n s ] == time && l i s t [ r ] [ clock_up ] == time && l i s t [ r ] [ n e x t ] == old ( l i s t ) [ g e t _ a c t u a l _ r e f e r e n c e ( old ( l i s t ) , base , time ) ] [ n e x t ] && l i s t [ r ] [ c o n t e n t ] == new ) && ( r != g e t _ a c t u a l _ r e f e r e n c e ( old ( l i s t ) , base , time ) && r != c r e a t e _ n o d e ( new , time ) ==> l i s t [ r ] [ c l o c k _ i n s ] == old ( l i s t ) [ r ] [ c l o c k _ i n s ] && l i s t [ r ] [ clock_up ] == old ( l i s t ) [ r ] [ clock_up ] && l i s t [ r ] [ n e x t ] == old ( l i s t ) [ r ] [ n e x t ] && l i s t [ r ] [ c o n t e n t ] == old ( l i s t ) [ r ] [ c o n t e n t ] ) ) && (f o r a l l r : Ref : : ( r == c r e a t e _ n o d e ( new , time ) ==> p r e s e n c e [ r ] == true ) && ( r != c r e a t e _ n o d e ( new , time ) ==> p r e s e n c e [ r ] == old ( p r e s e n c e ) [ r ] ) ) ; Token [ { " o p e r a t i o n 1 " : " update " , " o p e r a t i o n 2 " : " update " , " r e s t r i c t i o n s " : [ "@3 != @6" ] RR n°9111 --------------PAIR STABILITY VERIFICATION-------------update update STABILITY TEST : (PASSED) i n s e r t i n s e r t STABILITY TEST : (PASSED) d e l e t e update STABILITY TEST : (PASSED) d e l e t e d e l e t e STABILITY TEST : (PASSED) d e l e t e r e a d STABILITY TEST : (PASSED) d e l e t e i n s e r t STABILITY TEST : (PASSED) update r e a d STABILITY TEST : (PASSED) update i n s e r t STABILITY TEST : (PASSED) r e a d r e a d STABILITY TEST : (PASSED) r e a d i n s e r t STABILITY TEST : (PASSED) --------------PAIR COMMUTATIVITY VERIFICATION-------------update update COMMUTATIVITY TEST : (PASSED) i n s e r t i n s e r t COMMUTATIVITY TEST : (PASSED) d e l e t e update COMMUTATIVITY TEST : (PASSED) d e l e t e d e l e t e COMMUTATIVITY TEST : (PASSED) d e l e t e r e a d COMMUTATIVITY TEST : (PASSED) d e l e t e i n s e r t COMMUTATIVITY TEST : (PASSED) update r e a d COMMUTATIVITY TEST : (PASSED) update i n s e r t COMMUTATIVITY TEST : (PASSED) r e a d r e a d COMMUTATIVITY TEST : (PASSED) r e a d i n s e r t COMMUTATIVITY TEST : (PASSED) --------------EQUALITY SOLVER----------------------------TOKEN MODEL --------------Tokens p e r o p e r a t i o n s : Token c o n f l i c t s : RR n°9111

RR n°9111

The replicas are bounded between 0 and 99, since Boogie gives a verification failure for replicas more than 99. This is yet to be investigated though.RR n°9111

rue Simone Iff -CS 42112

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Acknowledgement

The author would like to thank Marc Shapiro and Paolo Viotti for their guidance and feedback and Gonçalo Marcelino for answering questions related to the tool. This research is supported in part by the RainbowFS project (Agence Nationale de la Recherche, France, number ANR-16-CE25-0013-01) and by European H2020 project 732 505 LightKone (2017-2020).

@ i n i t type matrix2d =[ int , i n t ] i n t ; type matrix1d =[ i n t ] i n t ; const r e p l i c a s : i n t ; const min : i n t ; axiom ( f o r a l l r : int , U: matrix1d : : r >= 0 && r <= r e p l i c a s ==> U[ r ] >= 0 ) ; axiom ( f o r a l l r1 , r 2 : int , R : matrix2d : : r 1 >= 0 && r 1 <= r e p l i c a s && r 2 >= 0 && r 2 <= r e p l i c a s ==> R[ r1 , r 2 ] >= 0 ) ; axiom ( r e p l i c a s > 0 && r e p l i c a s < 9 9 ) ; function v a l u e (R: matrix2d , U: matrix1d ) returns ( i n t ) { min + diagonal_sum (R, 0 ) + sum (U, 0 ) } function diagonal_sum (R: matrix2d , i n d e x : i n t ) returns ( i n t ) { i f i n d e x < r e p l i c a s then (R[ index , i n d e x ] + diagonal_sum (R, i n d e x + 1 ) ) e l s e ( 0 ) } function sum (U: matrix1d , i n d e x : i n t ) returns ( i n t ) { i f i n d e x < r e p l i c a s then (U[ i n d e x ] + sum (U, i n d e x + 1 ) ) e l s e ( 0 ) } function l o c a l _ r i g h t s ( i d : int , R : matrix2d , U: matrix1d ) returns

) ) e l s e ( 0 ) } function row_sum (R: matrix2d , row : int , i n d e x : i n t ) returns ( i n t ) { i f i n d e x > r e p l i c a s then (R[ row , i n d e x ] + row_sum (R, row , i n d e x + 1 ) ) e l s e ( 0 ) } function i n c r e m e n t _ e f f e c t (R : matrix2d , oldR : matrix2d , i d : int , n : i n t ) returns ( bool ) { ( f o r a l l r1 , r 2 : i n t : :

) ) } function d e c r e m e n t _ e f f e c t (U: matrix1d , oldU : matrix1d , i d : int , n :

) ) } function t r a n s f e r _ e f f e c t (R: matrix2d , oldR : matrix2d , from : int , t o : int , n :

) ) } @ v a r i a b l e s var R: matrix2d ; var U: matrix1d ; @equals matrix2d @as f o r a l l r1 , r 2 : i n t : : @ t h i s [ r1 , r 2 ] == @other [ r1 , r 2 ] ; @equals matrix1d @as f o r a l l r : i n t : : @ t h i s [ r ] == @other [ r ] ; @ i n v a r i a n t v a l u e (R, U) >= min ; ) ) e l s e ( 0 ) } function e d i t _ m a t r i x 2 d (R: matrix2d , oldR : matrix2d , row : int , column : int , v a l u e : i n t ) returns ( bool ) { ( f o r a l l r , c : i n t : :

RR n°9111

( i f a > b then a e l s e b ) } @ v a r i a b l e s var R: matrix2d ; var U: matrix1d ; @equals matrix2d @as f o r a l l r1 , r 2 : i n t : : @ t h i s [ r 1 ] [ r 2 ] == @other [ r 1 ] [ r 2 ] ; @equals matrix1d @as f o r a l l r : i n t : : @ t h i s [ r ] == @other [ r ] ; @ i n v a r i a n t v a l u e (R, U) >= min ; @ o p e r a t i o n s procedure i n c r e m e n t ( i d : int , n : i n t ) modifies R; requires i d >= 0 && i d < r e p l i c a s ; ensures e d i t _ m a t r i x 2 d (R, old (R) , id , id , n ) ; procedure decrement ( i d : int , n : i n t ) modifies U; requires i d >= 0 && i d < r e p l i c a s ; ensures e d i t _ m a t r i x 1 d (U, old (U) , id , n ) ; procedure t r a n s f e r ( from : int , t o : int , n : i n t ) modifies R; requires from >= 0 && from < r e p l i c a s && t o >= 0 && t o < r e p l i c a s && from != t o ; ensures e d i t _ m a t r i x 2 d (R, old (R) , from , to , n ) ; Inria Sreeja } , { " o p e r a t i o n 1 " : " i n s e r t " , " o p e r a t i o n 2 " : " i n s e r t " , " r e s t r i c t i o n s " : [ "@3 != @6" ] } , { " o p e r a t i o n 1 " : " d e l e t e " , " o p e r a t i o n 2 " : " update " , " r e s t r i c t i o n s " : [ "@2 != @5" ] } ] ------------BASE VERIFICATION-------------