Reflecting On A Queueing Prism Leads To Unexpected Results

Computers are difficult enough to reason about when there’s just a single thread doing one task. There are dozens of cores in today’s modern processor world, and your program might try to take advantage of using more than just one. Things happening concurrently makes the number of states and interactions explode in to a mess we as humans are likely going to have trouble understanding. So, like [Hillel], you might turn to the computer to try and model those interactions.

The model in question is a task queue. Things are added to the pile, and “workers” grab one from the pile and process it. There are two metrics used to measure the effectiveness of a task queue: throughput and latency. Throughput is the number of things you can do per second (like this maximum throughput 3d printer), while latency is the amount of time it takes to finish one thing.

Instead of writing a simulation, [Hillel] turned to a probabilistic model checker called PRISM. There are a few constraints on the model, such as each task being dependent and taking a different time to complete. This is modeled by the fact that each step a worker has a 50% chance of completing their task. For each step, there is a 50% chance a new task comes into the queue, up to a limit of N total tasks. Next, he modeled throughput by creating a reward function that gives us the total number of steps it took us to complete all tasks. Latency is another reward function, but, it is the sum of the number of items in the queue for each timestep.

With just one worker, the growth in latency looks quadratic. Just ten tasks wait for 29-time steps, while 20 tasks wait for 97-time steps. When adding in a second worker, the throughput doesn’t double but instead is about 2/3rds of what it was for one worker. But on the flipside, latency has fallen to something closer to linear.

While a simple model, the idea of a model to simulate a complex domain is there. You could easily add priority, more workers, retrying, adding items back to the queue, adding multiple items in one time step, and other things. [Hillel] provides a little python gist to help you generate the PRISM for an arbitrary number of workers.

Formal methods/verification isn’t something we talk about often on Hackaday, and if you’re curious for more, we talked about how to verify your C compiler as being trustworthy.