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

[Richard Achmatowicz (JIRA)]

     [ https://issues.jboss.org/browse/ISPN-5309?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel ]

Richard Achmatowicz updated ISPN-5309:
--------------------------------------
    Description: 
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.

  was:
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.



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



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