[infinispan-issues] [JBoss JIRA] (ISPN-6832) Proof of correctness for complex distributed patterns

[Sebastian Łaskawiec (JIRA)]

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

Sebastian Łaskawiec updated ISPN-6832:
--------------------------------------
    Component/s: Core


> Proof of correctness for complex distributed patterns
> -----------------------------------------------------
>
>                 Key: ISPN-6832
>                 URL: https://issues.jboss.org/browse/ISPN-6832
>             Project: Infinispan
>          Issue Type: Feature Request
>          Components: Core
>            Reporter: Sebastian Łaskawiec
>
> The core of Infinispan can be represented in very simple "primitives": a set of nodes send messages to each other. The fundamental rules are also relatively simple:
> * a message can't be received before it's sent
> * a message could be lost
> * a node could be killed at any time
> From these basic building blocks one can start building some logical consequences:
> * messages sent to multiple nodes might arrive at different times
> * multiple messages sent to multiple nodes might be delivered in different order
> Some of these problems are resolved by JGroups - but even then it must be configured accordingly, meaning Infinispan' s usage of it is sensible to using the wrong method or flags.
> While the Java/Scala code in Infinispan is not overly complex, it's not suited for reasoning on the consequences of often-needed changes in the codebase. It would be very useful to be able to define patterns in an ad-hoc meta language, and provide a proof correctness of the patterns it uses, or at least proof the events it should avoid can not happen.
> A great help for the project would be to sketch such a language and try it out on some of the distribution schemes Infinispan uses to proof they are correct or identify flaws in correctness. In a second step (optional) one could build some tooling around this to provide automatic demonstration / simulation for proposed changes expressed in this meta language.
> The Promela language could be used for this purpose; so one could build tooling around it, try to apply it on Infinispan, and possibly work on ad-hoc extesions.
> See also previous proposal: "Visualization and tracing of messages between nodes" -> that would make it possible to trace the real Infinispan behaviour and then demonstrate it's correctness or identify problems before they happen.



--
This message was sent by Atlassian JIRA
(v6.4.11#64026)