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.