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...

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.

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 ;)

Good work!

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).

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.

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.

Comments URL: https://news.ycombinator.com/item?id=37408579

Points: 5

# Comments: 0

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.

Comments URL: https://news.ycombinator.com/item?id=26797654

Points: 2

# Comments: 0

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)

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...

Comments URL: https://news.ycombinator.com/item?id=26532547

Points: 1

# Comments: 1

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&...