[infinispan-issues] [JBoss JIRA] (ISPN-5309) Model data consistency for get()/put() operations in Infinispan

[Richard Achmatowicz (JIRA)]

Richard Achmatowicz created ISPN-5309:
-----------------------------------------

             Summary: Model data consistency for get()/put() operations in Infinispan
                 Key: ISPN-5309
                 URL: https://issues.jboss.org/browse/ISPN-5309
             Project: Infinispan
          Issue Type: Task
            Reporter: Richard Achmatowicz
            Assignee: Richard Achmatowicz


This will be the first in a series of modelling/validation exercises for some of the more critical Infinispan protocols. 

We shall use TLA+ / PlusCal / TLA+ Tools to do the following:
- model the design of processing of get()/put() operations in an Infinispan cluster
- model client interactions with that cluster
- describe the data consistency requirements of get()/put() operations
- verify that the data consistency semantics of Infinispan are preserved in the face of concurrent client interactions

TLA+ / PLusCal can be thought of as a pseudo-code language which has a well-defined semantics and is testable using the tools in the TLA+ Toolkit. 

The benefits of such an exercise are that we end up with:
- a specification of data consistency guarantees that Infinispan 
- a semantically precise pseudo-code description of the design of get()/put() processing
- a verification that the protocol design is correct 

We start here with the simple case of modelling data consistency in the absence of failures. In later exercises, we aim to tackle rebalancing and non-blocking state transfer in the face of membership changes and partitions.



--
This message was sent by Atlassian JIRA
(v6.3.11#6341)