[erlang-questions] PropEr and determinism of statem scenario execution

[Paul Peregud]

Hi everyone!

This is a PropEr-related question. I am developing a distributed algorithm
for broadcasting messages, with very specific requirements (which are not
really relevant to the problem, but prohibits use of e.g. Paxos in my case).

Situation is following: I want to test a distributed algorithm. It's goal -
synchronization of state consisting of sequence of broadcasted messages.
Configuration is following - there are N actors, each actor implements
publish/2 that adds new entry to cache and broadcasts. Actors are
communicating, trying to achieve consistent state of cache among all of
them. Actors are unreliable - they can be added and they may crash.

My test case is a sequence of commands from following set: [actor_up,
actor_down, publish]. My "system under test" is a process that starts
actors, shuts them down and publishes new messages. It also collects
reports that actors provide and provides that reports as a material for
postcondition that checks cache consistency.

The problem - I don't have a control over schedulers. That leads to
scenarios that MAY OR MAY NOT fail. And that causes problems with
shrinking. As a result after a night of crunching scenarios on a fast
machine I get a test case of 70 steps that is impossible to debug, because
it is too large. When I repeat this test case using proper:check/2, it
fails very seldom.

I've tried to tackle the problem in following way.
I have introduced an execution token. An actor is waiting in selective
receive for the token, when it gets it, it takes one message from it's
queue and processes it. After that token is returned to proper tester
process and can be passed to another actor.

This approach is not good enough, because every generated scenario passes.
I can think of one reason only - if actors A and B perform and they both
send 2 messages (upon receiving the execution token) to actor C then actors
C queue may look only like that: [A1, A2, B1, B2]. In real life scenario
queue [A1, B1, A2, B2] is also possible.

I understand that I can modify actors even more and introduce more
fine-grained control over their actions - execution token will be returned
after one single message sent. But this approach feels like an ugly hack.
Is there a more general way to deal with this problem? Is it possible to
achieve fine-grained concurrent simulation using Proper/Quickcheck?

Any ideas are welcome!

As far as I understand McErlang solves this problem in a more low level
way, but I have never heard it used for practical problems. Did anyone used
it to test non-academic systems? Any success stories here? How hard is it
to use?

Best regards,
Paul Peregud
+48602112091
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20121123/b82a3cb1/attachment.htm>