inaseer (u/inaseer) - Readit News

inaseer commented on Systems Correctness Practices at Amazon Web Services cacm.acm.org/practice/sys... · Posted by u/tanelpoder

algorithmsRcool · 7 months ago

It looks like Coyote[0], which is used in azure, was an evolution of P# which was an evolution of P

[0]https://www.microsoft.com/en-us/research/wp-content/uploads/...

inaseer · 7 months ago

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

inaseer commented on Ask HN: Who is hiring? (August 2024) · Posted by u/whoishiring

inaseer · a year ago

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.

inaseer commented on Turmoil, a framework for developing and testing distributed systems tokio.rs/blog/2023-01-03-... · Posted by u/zbentley

DylanSp · 2 years ago

Always good to see more examples of this sort of project; making it straightforward to test how systems behave with unreliable networks [1] should make building resilient systems easier.

I came across Microsoft's Coyote project [2] a while back, which seems similar to this, though for C#. Has anyone here tried that out? If so, what have your experiences with it been like?

[1] Also known as any network ever.

[2] https://github.com/microsoft/coyote

inaseer · 2 years ago

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.

inaseer commented on Learn TLA+ learntla.com/... · Posted by u/yarapavan

inaseer · 3 years ago

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.

inaseer · 3 years ago

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.

inaseer commented on Learn TLA+ learntla.com/... · Posted by u/yarapavan

hwayne · 3 years ago

The universal problem is "generating code from a formal spec" is extremely, maddeningly, pull-your-hair-outingly hard. A slightly easier thing, as you said, generating test cases, which is what the Mongo people have been advancing: https://arxiv.org/abs/2006.00915

(Another interesting approach in this space is P, which is lower-level than TLA+ but also can compile to C#: https://github.com/p-org/P)

inaseer · 3 years ago

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.

inaseer commented on TLA+ is hard to learn (2018) surfingcomplexity.blog/20... · Posted by u/azhenley

IanCal · 4 years ago

Are there good alternatives for solving the same / similar kinds of problems?

I am a big fan of property based testing that can fuzz through very similar types of problems but it's not quite the same.

Or is tla+ just the thing to use and it's worth ploughing through?

inaseer · 4 years ago

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.

inaseer commented on TLA+ Graph Explorer github.com/afonsonf/tlapl... · Posted by u/hwayne

inaseer · 5 years ago

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)

inaseer commented on Eliminating Data Races in Firefox hacks.mozilla.org/2021/04... · Posted by u/caution

kibwen · 5 years ago

And when it comes to finding bugs in your unsafe concurrency primitives in Rust programs, there is a tool called Loom that helps with that, as a powerful complement to what ThreadSanitizer provides: https://github.com/tokio-rs/loom . You can think of Loom sort of like QuickCheck, except the permutations are all the possible thread states of your program based on the memory orderings that you have specified.

Here's a video that briefly talks about what Loom can do https://youtu.be/rMGWeSjctlY?t=7519 (it's part of a larger video about memory orderings, and is a great introduction to the topic).

inaseer · 5 years ago

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.