[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:comment-tabpanel&focusedCommentId=13051048#comment-13051048 ] 

Richard Achmatowicz commented on ISPN-5309:
-------------------------------------------

Dan, Bela and I started discussions on this a few days ago, believing it's probably a good time to get started on this.
This issue will collect comments, discussions.
 

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