Introducing Runway, a distributed systems design tool
1–10 of 12 posts
Re: Introducing Runway, a distributed systems design tool
#2Very happy to see more tooling being created for distributed systems, it is much needed. Will have to check out the talk, too.
We've also released a tool for testing distributed systems, https://github.com/gundb/panic-server . It integrates with your existing tests (like mocha and others), and even reports/throws bugs back from the remote machines you're testing across.
Re: Introducing Runway, a distributed systems design tool
#3This is very interesting. It seems like a much more user-friendly version of TLA+. Wonder what Lamport thinks about it :)
I think the next logical feature would be to have Runway compile a model-checked specification to an actual C++/Java/go/python implementation, using something like Thrift or CapnProto RPC codegen. There has been some work on doing similar spec->implementation compilation from Coq to erlang [0] but the author hit a lot of obstacles.
[0] - http://christophermeiklejohn.com/coq/erlang/2013/11/19/verif...
Re: Introducing Runway, a distributed systems design tool
#4Seems a lot more accessible than TLA+. I have tried to get started with TLA+ a few times and never been able to get going so hopefully this yields better results.
Re: Introducing Runway, a distributed systems design tool
#5This tool seems to be equally useful for modeling any complex software at the concept level. Is there any thing that would prevent this from being used in non-distributed systems scenarios?
Re: Introducing Runway, a distributed systems design tool
#6This is very interesting. It seems like a much more user-friendly version of TLA+. Wonder what Lamport thinks about it :) I think the next logical feature would be to have Runway compile a model-checked specification to an actual C++/Java/go/python implementation, using something like Thrift or CapnProto RPC codegen. There has been some work on doing similar spec->implementation compilation from Coq to erlang [0] but…
The Banana and Elevator demos did not specify/verify temporal properties so I suspect it doesn't support specifying temporal formulas at the moment (the T in TLA+). This means it can be used to check correctness properties but not liveness properties. Despite this limitation I believe this is a fantastic tool as it makes writing specs way more approachable.
Re: Introducing Runway, a distributed systems design tool
#7This is very interesting. It seems like a much more user-friendly version of TLA+. Wonder what Lamport thinks about it :) I think the next logical feature would be to have Runway compile a model-checked specification to an actual C++/Java/go/python implementation, using something like Thrift or CapnProto RPC codegen. There has been some work on doing similar spec->implementation compilation from Coq to erlang [0] but…
That is exactly the effort done in our group before (from TLA+ to real C++ implementation) - the challenge is that the gap between specification and the implementation is large in terms of both implementation details and language expressiveness. As a complementary approach, we have come up libraries for distributed system development with built-in implementation-level model checking support. You may check out https://github.com/Microsoft/rDSN for details.
Re: Introducing Runway, a distributed systems design tool
#8[deleted]
Re: Introducing Runway, a distributed systems design tool
#9If you like this, you might also like http://www.win.tue.nl/mcrl2/release/user_manual/index.html
Re: Introducing Runway, a distributed systems design tool
#10> I’ve explored many techniques to help with distributed systems design,
> including formal specification, model checking, formal and informal
> proofs, simulation, and visualization. I’ve found all of these things
> valuable to learn about, and I think some of them are entirely practical
> to use. However, standard practice in industry is to use none of them.
This is what surprised me most when I started learning about formal specifications. I had been developing distributed systems for years armed with nothing but algorithms, papers, and my own sloppy thinking. I had worked alongside some very smart, senior people who never brought out any kind of formal specification.
It wasn't until I met a researcher developing his own specification method that I heard about such tools.
And I'm super-glad I jumped in.
I'm happy to see more tools entering the space. My feeling is that they are becoming sophisticated enough that we will be able to see people adopting them in the wider industry, even in open-source software. I believe they should be the state of the art. I also think that any distributed system should be published with a formal specification, if not proof, before being accepted into wider adoption by industry.
update formatting