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

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