Implementing an Outbox — model-checking first
The NServiceBus Outbox gives you consistency between database and messaging operations, something that would be nontrivial to do on your own. So how does it work? And how can you prove that it works?
It’s hard to build reliable messaging systems. It’s even harder if you can’t use distributed transactions between your message queues and data storage. Fortunately, NServiceBus fills this gap with the Outbox. The Outbox provides similar guarantees to distributed transactions but avoids the complex and cumbersome Two-Phase Commit protocol. Since NServiceBus introduced the Outbox almost 7 years ago, other frameworks followed and added their own implementations.
In this presentation, we’ll use TLA+ to specify and validate the Outbox. TLA+ is a tool for validating critical parts of distributed and concurrent systems, which makes it a perfect tool for the job. By distilling the Outbox to bare essentials we’ll learn how the algorithm works, which guarantees it gives, and the assumptions it makes about messaging and storage infrastructure.
In this webinar you’ll learn about:
- The main challenges in building reliable systems using modern messaging infrastructure — both on-premises and in the Cloud.
- The Outbox pattern, how it works, and how it guarantees consistent message processing.
- Using TLA+ to model-check the Outbox algorithm. Warning: hard core computer science. Be prepared!
About Tomek Masternak
Tomek is an engineer at Particular Software. He is passionate about the theory and practice of distributed systems and likes to know why they work or fail and what that means in the first place.