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

[Sebastian Łaskawiec (JIRA)]

Sebastian Łaskawiec created ISPN-6832:
-----------------------------------------

             Summary: Proof of correctness for complex distributed patterns
                 Key: ISPN-6832
                 URL: https://issues.jboss.org/browse/ISPN-6832
             Project: Infinispan
          Issue Type: Feature Request
            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)