Performance/reliability trouble with actor-based Raft implementation (CloudMessaging sample)

[fhackett]

As part of a related research project, I'm trying to benchmark the runtime performance of the Raft implementation in the Samples directory (CloudMessaging).
So far, I've managed to recreate the Azure Service Bus setup, get a cluster of 3 servers running, and I've run the existing single-client workload against it.

What's confusing is that the performance is quite slow compared to other verified Raft implementations (1-2 ops per second), and I'm seeing a lot of glitchy behavior:

• It often gets stuck unable to process all of the client requests.
• Looking at the request responses, I also see a lot of duplicate responses.
• When using debug mode, it often claims to receive far too many votes for things ("10 out of max 4" might show up in the log)

I've included a summary of what the client "sees" on a run with 50 client requests which gets stuck at the end:

<Client> sending request-0.
<Client> received response for request-0 from  Server-3.
<Client> sending request-1.
<Client> received response for request-0 from  Server-3.
<Client> sending request-2.
<Client> received response for request-1 from  Server-3.
<Client> sending request-3.
<Client> received response for request-1 from  Server-3.
<Client> sending request-4.
<Client> received response for request-2 from  Server-3.
<Client> sending request-5.
<Client> received response for request-3 from  Server-3.
<Client> sending request-6.
<Client> received response for request-3 from  Server-3.
<Client> sending request-7.
<Client> received response for request-4 from  Server-3.
<Client> sending request-8.
<Client> received response for request-5 from  Server-3.
...
<Client> sending request-45.
<Client> received response for request-28 from  Server-3.
<Client> sending request-46.
<Client> received response for request-25 from  Server-3.
<Client> sending request-47.

My question is: is this expected, or is it possible that I have set something up incorrectly?

Notes:

• I checked to see whether the duplicate detection setting in Service Bus helped, but it still got stuck.
• Even executions with no obvious duplicates still get stuck
• Longer executions get stuck more easily. 1 request almost always works, 10 works often, 50 almost never
• I'm running this locally on my laptop, which I know adds some overhead since Service Bus is in Azure. I have good quality wired internet though, and if I can get this working better I will properly run everything on Azure.

[pdeligia]

Hi @fhackett, I have not looked in this sample for a long time now, but I believe what you are seeing here is expected.

Please note that we are not trying to provide a correct, performant or production-quality Raft implementation here. Instead, the focus of this sample is to showcase the bug-finding capabilities of coyote (see the corresponding tutorial here). We only provide the "production-ish" version to showcase how to setup a coyote test on a realistic looking application. The application itself has bugs injected in-purpose, which coyote is able to find, showing how you can use this tool in your own C# projects.

Also just to clarify to what you mentioned about "other verified Raft implementations": coyote is not a verification tool. Instead, it focuses exclusively on bug-finding (under a default or given bound, such as test time, number of test iterations, max scheduling decisions, etc.) and driving high coverage (using state-of-the-art exploration strategies from the "controlled concurrency testing" literature) on (typically) existing C# projects. In practice, this works really well on production-scale systems and (for example) a large number of distributed systems inside Azure rely today on coyote for concurrency-related bug-finding, regression testing and bug-repro. So, this is a very different approach from say tools like Dafny that produce verifiable C# code. I am not sure if I misunderstood you here, when you compared with other "verified" implementations, but just wanted to mention this to avoid any confusion.

Hope this helps!

[fhackett]

Thank you, that does help. We were not aware that this sample was mostly a model checking demo with proof of concept I/O.

Regarding "other verified Raft implementations", our own work (https://github.com/DistCompiler/pgo) is a bit of an in-between, so we've received recommendations to compare to various kinds of related work. We're similar to Dafny, in that we produce verified code, but we also use a form of bounded model checking like Coyote. So, your clarification is important in that there are a lot of definitions of "verified" and a lot of tool designs in this space, and I was being unclear.

[pdeligia]

Glad this discussion helped @fhackett, and thanks for sharing the context around what you are trying to do and about your PGo project. Looks like very interesting work, I will check it out!