Hello Jakub, not only are we interested: we have been talking about it for a while, but lack of time has not allowed us to pursue it. So yes, it would be very useful. As far as scope it seems like you already have a good grasp of what to tackle, and we are more than happy to answer any questions you might have. I would like both Bela Ban and Richard Achmatowicz to add their thoughts to this, as they have more intimate knowledge with the tools and the concepts behind formal verification. Tristan On 13/01/2016 16:56, Jakub Senko wrote: > Hi all! > > I'm considering a thesis topic [1] inspired by the successful use > of automated formal verification methods by Amazon engineers for AWS S3 and others [2]. > > The basic idea is to use similar tools to verify core parts of Infinispan > by constructing a simplified model (because of the state space explosion). > Most useful areas seem to be the transport layer, command object execution > (get, put, topology change, state transfer), entry locks etc. > On the other hand, I'd exclude transactional operations > which would be too complicated/costly to verify. > > Do you think this would be useful for you as the infinispan developers? > Do you have suggestions on what (not) to focus? > I'd be happy for any comments. > > Cheers, > Jakub Senko > > [1] https://diplomky.redhat.com/topic/show/355/formal-design-of-distributed-h... > [2] http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-... > _______________________________________________ > infinispan-dev mailing list > infinispan-dev(a)lists.jboss.org > https://lists.jboss.org/mailman/listinfo/infinispan-dev > -- Tristan Tarrant Infinispan Lead JBoss, a division of Red Hat _______________________________________________ infinispan-dev mailing list infinispan-dev(a)lists.jboss.org https://lists.jboss.org/mailman/listinfo/infinispan-dev

Hi Jakub, interesting topic! Here are some areas where an investigation would be fruitful, in no particular order: Correctness of reads and writes in a distributed cache wrt state transfer: - Model gets and puts against a distributed data store - Run the model checker against this and see that there's no scenario where we can end up with inconsistent data - Add state transfer into the fold Split brain / network partitions: - Model a network partition, clients continue accessing the same values - Remove the split - Make sure the data in all nodes is consistent - Simulate multiple network partitions, e.g. from {A,B,C,D,E} -> {ABC} and {DE}, then {ABC} -> {AB} and {C} etc This may be too complex to model in TLA+, have you considered looking into Jepsen/Knossos as well? You'd have to talk to the Infinispan team to see what behavior is guaranteed by which configuration and then use these tools to make sure the actual behavior == the expected behavior. Cheers, On 13/01/16 16:56, Jakub Senko wrote: > Hi all! > > I'm considering a thesis topic [1] inspired by the successful use > of automated formal verification methods by Amazon engineers for AWS S3 and others [2]. > > The basic idea is to use similar tools to verify core parts of Infinispan > by constructing a simplified model (because of the state space explosion). > Most useful areas seem to be the transport layer, command object execution > (get, put, topology change, state transfer), entry locks etc. > On the other hand, I'd exclude transactional operations > which would be too complicated/costly to verify. > > Do you think this would be useful for you as the infinispan developers? > Do you have suggestions on what (not) to focus? > I'd be happy for any comments. > > Cheers, > Jakub Senko > > [1] https://diplomky.redhat.com/topic/show/355/formal-design-of-distributed-h... > [2] http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-... > _______________________________________________ > infinispan-dev mailing list > infinispan-dev(a)lists.jboss.org > https://lists.jboss.org/mailman/listinfo/infinispan-dev >