Hi everyone!<br><br>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).<br>
<br>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.<br>
<br>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.<br>
<br>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.<br>
<br>I've tried to tackle the problem in following way. <br>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. <br>
<br>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. <br>
<br>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?<br>
<br>Any ideas are welcome!<br><br>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?<br>
<br>Best regards,<br>Paul Peregud<br>+48602112091<br>