¶CSP would be a good language for property tests
2023-10-10
Property tests are great. When building a distributed system, simulation tests are great, since they let you test intricate behaviors as faster/easier unit tests instead of as harder/more brittle integration tests. A simulation property test would be even betterer. But how would you express the properties that you want the simulation to test?
CSP seems like a good answer.
As an example in Go, you could make sure that your implementation uses the new structured logging library (slog, new in 1.21). This is a good idea for observability reasons anyway, but doing so means you've got a nice trace of events that each of the nodes in your system performed during the test. You then just need to ensure that it's a valid trace of the CSP process that describes the property that must hold. My hunch is that you could use CSP to express fairly complex properties succinctly and understandably, using operators like parallel composition and interleaving.
[Cirstea2024] describes a similar idea, but using TLA+ as the specification language. It also looks like it requires more code changes to generate a trace of events, instead of piggy-backing on existing structured logging.
[Cirstea2024] Validating Traces of Distributed Programs Against TLA+ Specifications