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.