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

[Radim Vansa (JIRA)]

    [ https://issues.jboss.org/browse/ISPN-5309?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=13051476#comment-13051476 ] 

Radim Vansa commented on ISPN-5309:
-----------------------------------

The suggestion above looks like a good start for learning PlusCal/TLA+, but not considering membership changes in the basic design looks as we won't catch much. I think that the modeling should be based on good approximation of our view ids/topologyIds/CHs as we do use them, rather than focus on cache with multiple keys.

Off course, let's leave cachestores, passivation etc. away - we already know where these are broken. I would even suggest starting just with replicated cache (or rather single value replicated to all nodes).

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