AFAIK Jepsen/Knossos verify actual behaviour of a system (execute random requests, record return values and then analyse consistency of these data). That's testing, but not verification - it can find some failing scenarios, but it cannot prove correctness.
Not that this wouldn't be useful, but it would be completely different subject. Radim On 01/14/2016 03:52 PM, Bela Ban wrote: > 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-hash-table >> [2] >> http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext >> _______________________________________________ >> infinispan-dev mailing list >> infinispan-dev@lists.jboss.org >> https://lists.jboss.org/mailman/listinfo/infinispan-dev >> -- Radim Vansa <rva...@redhat.com> JBoss Performance Team _______________________________________________ infinispan-dev mailing list infinispan-dev@lists.jboss.org https://lists.jboss.org/mailman/listinfo/infinispan-dev