[infinispan-dev] Formal verification (thesis)

[Radim Vansa]

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


-- 
Radim Vansa <rvansa at redhat.com>
JBoss Performance Team