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

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 provides - 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.