Marc Brooker also wrote a post titled Formal Methods Only Solve Half My Problems. He gave a talk with the same title at HPTS’22 but I don’t think that’s online. Anyway this inspired one of my friends to start a reading group for a textbook called Performance Modeling and Design of Computer Systems:
Queueing Theory in Action with the goal of better understanding how to model all the stuff not captured by tools like TLA+.
Properties like latency, throughput, bottlenecks, things of this nature. We finished our reading a few weeks ago and I wish I could say it was a success, but the book is highly analytical - look forward to pages of differential equations. I think any tool used in a wider engineering context must fundamentally be based on modeling the system and running simulations, rather than trying to find some closed-form solution for the expected value of some property of a work queue network. Or maybe this thinking is flawed and we really should learn how to set up these systems of equations, letting computer algebra systems chug it out. Anyway beyond a better understanding of the difference between poisson/exponential/pareto distributions and some markov chain properties I sadly didn’t have many useful takeaways from the book.
I think any tool used in a wider engineering context must fundamentally be based on modeling the system and running simulations, rather than trying to find some closed-form solution for the expected value of some property of a work queue network.
I agree with this. There are some of the equations (e.g. E[N] = ⍴/(1-⍴)) and ideas (PASTA) that are extremely valuable and provide real insight. But for working engineers simulations just seem like a better tool than differential equations in this space. Not only are we more likely to get the answers right (at least because the code is easier to review for most colleagues), but it’s much easier to “explore the space” of parameters (multiple queues, non-Poisson arrivals, etc) without doing the same work over and over.
The simulation space is interesting because it’s heading for the system dynamics stuff that Forester, Meadow, et al did. There are mature tools for doing that kind of modeling, handily. https://systemdynamics.org/ isn’t a terrible place to start, or Meadows’s book Thinking in Systems.
Marc Brooker also wrote a post titled Formal Methods Only Solve Half My Problems. He gave a talk with the same title at HPTS’22 but I don’t think that’s online. Anyway this inspired one of my friends to start a reading group for a textbook called Performance Modeling and Design of Computer Systems: Queueing Theory in Action with the goal of better understanding how to model all the stuff not captured by tools like TLA+. Properties like latency, throughput, bottlenecks, things of this nature. We finished our reading a few weeks ago and I wish I could say it was a success, but the book is highly analytical - look forward to pages of differential equations. I think any tool used in a wider engineering context must fundamentally be based on modeling the system and running simulations, rather than trying to find some closed-form solution for the expected value of some property of a work queue network. Or maybe this thinking is flawed and we really should learn how to set up these systems of equations, letting computer algebra systems chug it out. Anyway beyond a better understanding of the difference between poisson/exponential/pareto distributions and some markov chain properties I sadly didn’t have many useful takeaways from the book.
I agree with this. There are some of the equations (e.g.
E[N] = ⍴/(1-⍴)) and ideas (PASTA) that are extremely valuable and provide real insight. But for working engineers simulations just seem like a better tool than differential equations in this space. Not only are we more likely to get the answers right (at least because the code is easier to review for most colleagues), but it’s much easier to “explore the space” of parameters (multiple queues, non-Poisson arrivals, etc) without doing the same work over and over.I found this paper recently which at least goes to the level of model checking performance properties, which is more applicable than random diff eqs.
The simulation space is interesting because it’s heading for the system dynamics stuff that Forester, Meadow, et al did. There are mature tools for doing that kind of modeling, handily. https://systemdynamics.org/ isn’t a terrible place to start, or Meadows’s book Thinking in Systems.