Simple Simulations for System Builders - Marc's Blog
It's no secret that I'm a big fan of formal methods. I use P and TLA+ often. I like these tools because they provide clear ways to communicate about even the trickiest protocols, and allow us to use computers to reason about the systems we're designing before we build them1. These tools are typically focused on safety (Nothing bad happens) and liveness (Something good happens (eventually))2. Safety and liveness are crucial properties of systems, but far from being all the properties we care about. As system designers we typically care about many other things that aren't strictly safety or liveness properties. For example:
The formal tools we typically use don't do a great job of answering these questions. There are many ways to answer them, of course, from closed-form analysis3 to prototyping. One of my favorite approaches is one I call simple simulation: writing small simulators that simulate the behavior of simple models, where the code can be easily read, reviewed, and understood by people who aren't experts on simulation or numerical methods.
If you hang around with skiers or snowboarders, you'll have heard a lot of talk over the last couple of winters about how crowded resorts have become, and how much time they now spend waiting to ride the ski lift4. Resort operators say that visits have been up only quite modestly, but skiers are seeing much longer waits. Is somebody lying? Or could we see significant increases in wait times with only modest increases in traffic?
