[infinispan-dev] Formal verification (thesis)

[Bela Ban]

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 at lists.jboss.org
> https://lists.jboss.org/mailman/listinfo/infinispan-dev
>

-- 
Bela Ban, JGroups lead (http://www.jgroups.org)