inaseer

Have you looked at model-based testing? One way to think of it as property-based testing for stateful system, though that's underselling it a little. It's surprisingly easy to come up models/specs for most stateful systems, including CRUD apps.

Source: I've modeled a number of CRUD like and non-CRUD like systems through the Accordant framework (https://github.com/microsoft/accordant)

There are really two separate concerns here.

The first is that some effect happens asynchronously, potentially interleaved with other operations. Whether a client observes completion by polling or by receiving an event from a message broker is orthogonal to the specification itself - the model looks essentially the same in both cases. The built-in test executor uses polling, but that's an execution strategy, not a specification construct.

If you have a trace containing both requests/responses and observed events, you can use the model to check that the trace conforms to the specification. In practice, it helps if the events can be localized to some interval in the execution (e.g. "this happened after A and before B"); otherwise the checker has to consider many more possible concurrent interleavings.

The conformance testing docs hint at how this can be done, but don't yet show an event-driven example. It's a good enough question that I'll write a dedicated doc page on it.

Conformance testing page: https://microsoft.github.io/accordant/docs/concepts/conforma...

Property-based testing and model-based testing are closely related. Both ask the developer to state the expected behavior of a system (whether you call it a property, invariant, model, specification, or contract) and then validate that behavior over arbitrary inputs and arbitrary sequences of operations. Property-based testing frameworks also typically provide fuzzing and shrinking.

Where we felt there was a gap was in expressing rich stateful behavior: models involving non-determinism (e.g. a timeout where the write may or may not have committed), concurrency, and eventual asynchronous completion, and then checking that an observed execution trace conforms to that model. Accordant aims to make those kinds of specifications concise and readable.

Once you have such a model, it's possible to integrate it with the fuzzing and shrinking capabilities of existing property-based testing libraries. We'll have documentation on that integration soon.

I've been working on a framework for writing executable specs in .NET called Accordant, developed at Microsoft and open sourced recently.

Github: https://github.com/microsoft/accordant

Docs: https://microsoft.github.io/accordant

Every API has a contract - the rules for how it should behave. You can't withdraw more than the balance. You can't delete a resource with active references. You can't re-create what already exists. But usually these rules are never written down in one place. Accordant lets you write the contract directly, as executable code. Not documentation that drifts, but code - if the implementation stops behaving according to the contract, you get immediate failures. Not only can you use the executable spec to validate _arbitrary_ scenarios, you can also use the spec - a first class construct - to mechanically explore the state space of a system and generate interesting test sequences. The docs above have examples.

Also worth calling out that we've used the framework to model a number of complex, distributed real-world systems: those involving async processes, concurrency, retries and crash consistency. These are non-trivial specs (and they pair quite well with techniques like deterministic simulation testing). Great care has been taken to ensure the specs remain readable and concise despite that richness of behavior. For those of you old timers who might be familiar with Spec#/SpecExplorer and NModel, this model-based testing library is a descendant of that line of work.

With the rise in AI-assisted software development, I feel we need richer ways of specifying and validating software and I feel quite excited and bullish about the possibilities here. There's a lot more to say on the topic - follow my twitter feed if interested in more updates ;)

Soon!

Yes, I understand why you made these design decisions. And I also agree that sticking to JS/TS keeps things simple (for humans, and LLMs). I generally default to the s and s' way of specifying things (in a C# property-based testing framework I'm working on) but looking at how you approached things here gives me another angle to think about.

Good work!

Bombadil takes a fresh approach to UI testing I haven't seen before: online monitoring through LTL formulas. Unlike model-checking (say by TLC), LTL formulas over here unfold in lock-step with the UI and allow users to express interesting temporal properties during testing.

The other intriguing aspect was how state is modeled (or rather, maybe not explicitly modeled?). A lot of the examples show the state extracted from the DOM and temporal properties indicating what the next (or eventual) state _should be_. If we want to look at the existing state (according to the model/spec) when predicting the next state (similar to how you can use s when specifying s' in TLA+), there seems to be no direct way to do that. It should of course be possible to capture the state at an earlier time in a closure and use it in a thunk at a later point, so it should be possible to work around this but that can be a little awkward, maybe. I'm working on a project in this space (primarily geared towards backend API model-based testing) and the state of the _real_ system isn't globally inspectable unlike a web page so took a different route over there. Having said that, this is a very interesting design choice that's very intriguing (in a good way).

+1.

We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.

Microsoft Azure Storage | Seattle, WA | Onsite or Remote (US only)

Our team in Azure Storage is working on applying automated reasoning and validation techniques to scalably generate hundreds of thousands of tests to check data integrity and durability issues, and scalably validate a combinatorial number of feature interactions to catch regressions and subtle bugs that only happen under rare conditions. As a Software Engineer in this team, not only will you get an opportunity to use tools to specify and check the integrity, correctness and performance guarantees of a large and critical Azure service, you will also get an opportunity to work on building and improving the tools themselves as well as learn about existing state-of-the-art tools in this space. The lessons you will learn will be broadly applicable to any distributed system and will help accelerate your growth as a disciplined and thoughtful distributed systems engineer.

Microsoft's mission is to empower every person and every organization on the planet to achieve more. As employees we come together with a growth mindset, innovate to empower others, and collaborate to realize our shared goals. Each day we build on our values of respect, integrity, and accountability to create a culture of inclusion where everyone can thrive at work and beyond.

The official job posting is not live yet, so please reach out to me directly at imnaseer@microsoft.com and include "Automated Reasoning and Validation Position" in the subject.

My team used Coyote to test their distributed service against network race conditions. It requires a little bit of setup to ensure all components that typically run on separate machines can run in a single process, and inter-process communication happens through interfaces that can be stubbed out during testing.

I designed a series of workshops to teach these ideas internally at Microsoft. You can find the source code used in the workshop at https://github.com/microsoft/coyote-workshop - the repo can use better README files but sharing it nonetheless in case the setup helps inspire your own use of Coyote.

TLA+ and Coyote pair quite well actually. Verifying the high level design in TLA+ while checking subtle bugs as you translate that design to an implemention.

Check out Coyote (which is an evolution of P) and allows you to "model check" .NET code to find hard to find race condition-y bugs in your implementation. We have used it very successfully on a number of projects at Microsoft. I should probably do more public talks on it to get the word out. Finding subtle bugs in your implementation using tools like Coyote is easier than most people realize.

Coyote (concurrency exploration tool for .NET programs) can be used to do something "similar". My team often writes tests which set up focused concurrency between different APIs, the tests use Coyote to explore different ways that concurrency can unfold and write a strong set of assertions and invariants that must be true at the end. It's not TLA+ but it's still quite effective, very teachable as developers are already familiar with writing C# tests and helps catch safety and liveness bugs in our actual code base (as opposed to a model of it). It's not the same, by design, and does a decent job at finding concurrency and distributed system bugs.

Visualizations do help a lot when model checkers and concurrency schedule exploration tools like Coyote find bugs. Coyote include the ability to visualize the traces if you express your concurrency using actors (see https://microsoft.github.io/coyote/#concepts/actors/state-ma...)

It also allows you to implement your own "logger" through which you can emit enough information to construct some cool visualizations. I had a lot of fun working on visualizing an implementation of Paxos using Coyote (then P#) (screenshot at https://ibb.co/TTk2hYb)

Loom's style of exploration (and that of aws shuttle mentioned below) can be quite effective. Coyote is the equivalent library in the .NET world (formerly known as P#) and comes with a bunch of exploration "schedulers" (from random exploration to probabilistic and even an experimental reinforcement learning based one). They released an animation rich video today (see https://news.ycombinator.com/item?id=26718273). Worth watching even if you're using Rust as Loom and aws shuttle are conceptually similar.

There has been a bunch of content on Coyote shared before as well but the quality of animations and how they explain how it works under the hood in this introduction was excellent.

Hi HN,

The tweet links to a couple of tutorials showing how to test an extremely simple CRUD service using Coyote to find concurrency bugs. Developers write simple unit tests whose concurrency is explored by Coyote to find bugs. You might be surprised to learn how we can write a number of interesting concurrency tests for even the simplest of CRUD services.

https://microsoft.github.io/coyote/#tutorials/first-concurre... https://microsoft.github.io/coyote/#tutorials/test-concurren...

Shameless plug: http://imnaseer.net/paxos-from-the-ground-up.html

I worked on an explanation of Paxos where we start with a simple but incorrect implementation of the protocol. The bug is then fixed and the protocol refined. Which leads to another bug. Interestingly, after fixing 6 or 7 bugs we arrive at the actual working implementation of Paxos. The reader, having walked the path of arriving at the protocol (hopefully) understands the nuances better than just reading the description of the protocol from the get-go.

Bonus: The explanation uses simulated visual runs as well, eg. http://imnaseer.net/paxos-from-the-ground-up.html?section=3&...

Concurrency is hard - this was a great investigation into the bug using TLA+ by the author which suggested simplifications to the code in addition to the bug fix.

This reminded me of another reader/writer concurrency bug posted by Tom Cargill in the c2 wiki caused by surprising behavior of Java monitors, which Hillel Wayne showed how to discover and then fix using TLA+ at https://www.hillelwayne.com/post/augmenting-agile/

We were able to reproduce and fix the same bug using Coyote as well, and documented our experience at https://cloudblogs.microsoft.com/opensource/2020/07/14/extre... I was pleasantly surprised at the finding and was definitely heartened by our experiment where we were able to reproduce the bug in actual working C# code without the need of an additional modeling step. While TLA+ is undoubtedly very powerful when it comes to modeling and catching concurrency bugs, I do hope tools like Coyote get wider adoption and are implemented for more languages so bugs in critical infrastructure code can be caught in a scalable and repeatable way while staying within just one language for implementation _and_ testing.

This is a fair call-out. I'll like to share a counter-example where we 'model check' our real-world service written in C# with pretty decent effectiveness. As you rightly call out, the number of execution points around which the model checker explores interleavings in a concurrent situation cannot be too large. If you look at _most_ micro-services, the really interesting points around which interleavings have to be explored are to external storage systems, say, Cosmos DB or Azure Storage etc. This is because most micro-services maintain their state in these external systems and are otherwise stateless. This insight allows us to only explore interleavings around calls to these external services as that's where a ton of concurrency bugs reside and ignore the interleavings at arbitrary points _within_ the services. Leveraging this insight allows us to utilize concurrency testing tools like Coyote on real world code and services with the testing scaling decently with the size of the program.

This is a good callout. P language evolved into the P# framework (as opposed to a language) which then evolved into Coyote (https://microsoft.github.io/coyote/)

Coyote allows developers to systematically test concurrency expressed through .NET async/await tasks. I encouraged my team to embrace Coyote based concurrency testing right from the start as we set out to build a new Azure service from the ground up. The results have been encouraging. The unification of the programming and modeling language is actually _quite_ useful in practice. For one, developers who aren't experts in formal methods are able to write concurrency tests fairly easily with minimal guidance. Secondly, the model and code never go out of sync as they are one and the same. The trick through which we are able to scale out these techniques to large scale software-in-the-wild is to have numerous tests, each test exercising concurrency in one set of APIs. This approach has scaled out in a decent manner. We run our entire distributed system in one process with various tests exercising concurrency and faults triggered through a focused set of APIs. We'll blog more about our usage of Coyote in the coming months.

While TLA+ is very powerful and useful, we've also found language integrated tools like Coyote to be quite effective in testing and catching concurrency bugs in real world code in Azure.

Neat to learn about thread sanitizer. It sounds similar to another tool from Microsoft Research called Torch (https://www.microsoft.com/en-us/research/project/torch/) which automatically instruments binaries to detect data races. Coyote is similar in some ways but different in others. Coyote serializes the execution of the entire program (running one task at a time), exploring one set of interleavings and then rewinding, and then exploring another set of interleavings, hoping to hit hard-to-find safety and liveness bugs. In addition to finding concurrency bugs in one isolated process, we use it to find bugs in our distributed system by effectively running our entire distributed system in one process and having Coyote explore the various states our system can be in. It sounded mind-boggingly cool when I first came across this way of testing distributed systems through Foundation DB (https://www.youtube.com/watch?v=4fFDFbi3toc); we're emulating this kind of testing in our distributed system through Coyote. And unlike Foundation DB which had to develop their own variant of C++ to be able to do this kind of testing (kudos to them for doing it), Coyote allows us to do it on regular C# programs written using async/await asynchrony and benefit from decades of Microsoft Research in exploring large state spaces effectively.

That's a great question. Stress testing, which is what you are suggesting helps, but is not super effective and often misses bugs. You need tools which can precisely control the task/go-routine scheduling during testing and systematically explore the various interleavings which can happen in the system. We generally don't have good tool support for such testing. There are promising tools emerging however; here is a case study of one such tool and how it was used to reliably reproduce and fix a subtle concurrency bug: https://cloudblogs.microsoft.com/opensource/2020/07/14/extre...

That's a fair point. Having said that, it's also interesting to realize that most distributed systems (which are concurrent by their very nature) don't have that luxury. Our micro-services interact with databases, event queues, blob stores etc and each of those external entities is shared mutable state. Furthermore, services can crash at any time and can't start from a clean slate (unlike in-process concurrency which doesn't have to worry about that). My meta-point is that while I agree with your sentiment, the reality of modern day services is that you are _forced_ to reckon with mutable complexity when designing distributed concurrent services (and more and more of us are doing that with the shift to micro-services in the industry)

Concurrency is hard and we have very poor support for testing correctness of concurrent and distributed systems. Language abstractions help but they aren't nearly enough (as evidenced by this post). My team at Microsoft leverages Coyote to check the safety of our services against such subtle race conditions. We blogged about using it to reliably reproduce and fix a very subtle bug in a bounded buffer implementation over at https://cloudblogs.microsoft.com/opensource/2020/07/14/extre...

If you're using .NET in your projects, you can start taking advantage of such tools _today_. I would like for such tools and testing techniques to become more and more common place in the industry as concurrent and distributed systems are _hard_ and we should use all the help we can get.

Looms looks quite interesting and is similar to Coyote in a lot of ways. The exploration engine used by Coyote is based on years of investigation by Microsoft Research so it scales nicely on real world programs. I believe the Coyote team is looking into exposing the systematic exploration capabilities in a language and platform agnostic way so developers can create language-specific bindings in their language of choice and benefit from all the research done over decades. No timelines that I'm aware of but it is on the road map I believe.

We've used Coyote (https://microsoft.github.io/coyote/) which offers an actor-based programming model, as well as as async/await programming model on top of .NET's Tasks to express the concurrency in our services. Coyote includes a powerful systematic testing and exploration engine which explores the various states your programs can be in and helps you find violations to safety and liveness properties. This gives us the same benefits you get when using a model checker like TLA+ but on our actual production code as opposed to a model of the code. If your services are written in .NET, I seriously recommend taking a deeper look here.

Writing tests to prove you've a correct implementation is indeed a very hard problem. I toyed with an interesting idea last year where I began to write a simple (but intentionally incorrect) Paxos implementation using P# (now known as Coyote) and wanted to see if P#/Coyote's systematic exploration of the state space will show me the various race conditions which violated the protocol's correctness. To my surprise, the technique was quite effective. P#/Coyote was able to point out to a number of bugs after I specified the safety and liveness properties which weren't too hard to do. In effect, after specifying the safety/liveness properties, I was able to use P#/Coyote's state-space exploration to ensure the implementation had solid test coverage. More details are at https://github.com/imnaseer/DiscoveringPaxos where the project starts out with a simple naive implementation, uses P#/Coyote to find bugs, makes incremental modifications till we finally have a working version faithfully following the Paxos description.

Yes, database transactions should be heavily leveraged wherever possible. We've often had to write services which create multiple resources in response to user requests. As an example, create an entry in the database and trigger the creation of, say, an Azure storage account. Transactions across independent services and resources don't work and correctness requires thoughtful design. In the more general case, whenever your service talks to more than micro-service to complete an operation, you will probably have to think through issues of consistency and transactionality.

There is a good body of knowledge around dealing with concurrency issues within a single process. We've tools (locks, semaphores ...) to deal with the complexity as well as programming paradigms which help us write code which minimizes data races. It's interesting to realize that in a world with an increasing number of micro-services manipulating shared resources (a shared database, shared cloud resources), or even multiple nodes backing a single micro-service all reading and writing to shared resources, similar concurrency bugs arise all the time. Unlike a single process where you can use locks and other primitives to write correct code, there is no locking mechanism we can use to protect access to these global shared resources. We have to be more thoughtful so we write correct code in the presence of pervasive concurrency, which is easier said than done.