Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Writing correct lock-free and distributed stateful systems in Rust, with TLA+

github.com

Post reply on HN
Print view View original

31–40 of 96 posts

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#31

Post by dronemallone »

munin wrote: post #11
unboxed_type wrote: post #10

Lets say you model-checked some distributed algorithm with TLA+. You then implement it in Rust. How are you going to check that your implementation implements exactly the algorithm you have checked and not some other algorithm which looks very similar? I think the phrase 'reliable systems' is more appropriate to what you are up to, as opposed to the phrase 'correct systems' which usually corresponds to formal verific…

This is a gap in this kind of verification work. Systems like coq get around this by having a facility to "extract" code from the proof itself. You would define your algorithm as a Fixpoint, prove properties of that Fixpoint, then extract that Fixpoint into some ocaml code and use it directly in your real programs. This closes the loop you describe, insamuch as you trust the extraction process and the ocaml compiler…

That "facility" is the Curry-Howard correspondence!

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#32

Post by mhh__ »

burntsushi wrote: post #21
cabaalis wrote: post #20

Rust-ignorant here; I was reading your "why rust" section. It contains a lot of information about how safe the resulting code is and how that is such a great benefit, and that's why Rust was selected. But then it has this statement: "However, it needs to be noted that when creating lock-free high-performance algorithms, we are going to need to sidestep the safety guarantees of the compiler." .... So why Rust?

The benefit of Rust is not necessarily to completely avoid unsafe (although, that does happen in practice a lot). The benefit is that unsafe can be buttoned up behind a safe API, hopefully in a way that is Zero Cost. So you might have some unsafe core that you need to pay extra special attention to, but the rest of your code can be in safe Rust. For example, I maintain a Snappy compression crate in Rust. It uses quit…

That's still not really unique to rust, D (at least) does that too. However, good point nonetheless.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#33

Post by pron »

nickpsecurity wrote: post #30
pron wrote: post #26

Earlier quoted context omitted.

In principle, you could translate your code -- or even the generated machine code -- back to TLA+ and check it there. This has been done as research projects for C[1] and Java bytecode[2]. But the reality of formal verification is that we simply do not yet have the capability -- with any tool -- to formally specify and verify a large, complex software system end-to-end (namely, from high-level global correctness prop…

"In principle, you could translate your code -- or even the generated machine code -- back to TLA+ and check it there. This has been done as research projects for C[1] and Java bytecode[2]." There's also ASM's and equational methods that allowed specification or verification of instructions or their use to happen in days when the tooling was already adequate. I wouldn't use TLA+ for this unless we're talking about co…

It all depends on your precise requirements and aesthetic preferences. I personally find TLA+ more elegant than any other high-level specification language, and very few projects actually require end-to-end verification. Those that do, must be kept small as we simply do not have the ability to do end-to-end verification of large software, no matter what tools or combination of tools we have. We don't even have a theoretical breakthrough to point us at a likely method of achieving that. If you need end-to-end verification, you must accept that the software (or component) verified will be small, and the process arduous. Then again, if you really need end-to-end verification, you must be ready to make that sacrifice. Moreover, to the best of my knowledge, no significant end-to-end verification was ever done in industry without close assistance from expert researchers, except in specialized niches where model-checkers give you sufficient coverage.

Supplementing a high-level verification with code-level specification tools is always possible, but, again, everything here is a matter of the required confidence vs. affordable cost. Additional confidence always comes with additional cost.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#34

Post by steveklabnik »

mhh__ wrote: post #32
burntsushi wrote: post #21

Earlier quoted context omitted.

The benefit of Rust is not necessarily to completely avoid unsafe (although, that does happen in practice a lot). The benefit is that unsafe can be buttoned up behind a safe API, hopefully in a way that is Zero Cost. So you might have some unsafe core that you need to pay extra special attention to, but the rest of your code can be in safe Rust. For example, I maintain a Snappy compression crate in Rust. It uses quit…

That's still not really unique to rust, D (at least) does that too. However, good point nonetheless.

A big difference is the defaults; Rust made an explicit design decision to make unsafe the default, to mark it with a keyword and to make unsafe a superset of safe. It is totally true that these things aren't unique, but there is a lot of advantage for this specific set of choices in combination.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#35

Post by pron »

munin wrote: post #11
unboxed_type wrote: post #10

Lets say you model-checked some distributed algorithm with TLA+. You then implement it in Rust. How are you going to check that your implementation implements exactly the algorithm you have checked and not some other algorithm which looks very similar? I think the phrase 'reliable systems' is more appropriate to what you are up to, as opposed to the phrase 'correct systems' which usually corresponds to formal verific…

This is a gap in this kind of verification work. Systems like coq get around this by having a facility to "extract" code from the proof itself. You would define your algorithm as a Fixpoint, prove properties of that Fixpoint, then extract that Fixpoint into some ocaml code and use it directly in your real programs. This closes the loop you describe, insamuch as you trust the extraction process and the ocaml compiler…

It's not "getting around", and one could write an extraction tool like that for TLA+, too. The difficulty is simply verifying any system, by whatever method, end-to-end, namely verifying that the high-level global correctness properties are preserved all the way down to machine code. We simply have no idea how to do it for real-world, large software, and in those cases it's been done for small, simple software (seL4, CompCert), the process was extremely expensive.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#36

Post by pron »

nicknash wrote: post #16

For lock-free data structures, how does this verification encode the memory model? E.g. high-quality model checkers for the C++11 memory model allow for outcomes inconsistent with the execution order of the code (in addition to outcomes that aren't sequentially consistent, but are consistent with the execution order). They also work on unmodified source. In the past I've seen SPIN/Promela used as a tool for concurren…

You just define it :) TLA+ doesn't have a built-in memory model, nor any concept of memory whatsoever. You define your constructs at the level of detail you think is important. Weak memory can be defined using a CPU-local memory that is occasionally reconciled with RAM or other core-local memory.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#37

Post by staticassertion »

steveklabnik wrote: post #34
mhh__ wrote: post #32

Earlier quoted context omitted.

That's still not really unique to rust, D (at least) does that too. However, good point nonetheless.

A big difference is the defaults; Rust made an explicit design decision to make unsafe the default, to mark it with a keyword and to make unsafe a superset of safe. It is totally true that these things aren't unique, but there is a lot of advantage for this specific set of choices in combination.

> Rust made an explicit design decision to make unsafe the default

You mean 'safe the default'.

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#38

Post by steveklabnik »

staticassertion wrote: post #37
steveklabnik wrote: post #34

Earlier quoted context omitted.

A big difference is the defaults; Rust made an explicit design decision to make unsafe the default, to mark it with a keyword and to make unsafe a superset of safe. It is totally true that these things aren't unique, but there is a lot of advantage for this specific set of choices in combination.

> Rust made an explicit design decision to make unsafe the default You mean 'safe the default'.

Yes, whoops!

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#39

Post by burntsushi »

mhh__ wrote: post #32
burntsushi wrote: post #21

Earlier quoted context omitted.

The benefit of Rust is not necessarily to completely avoid unsafe (although, that does happen in practice a lot). The benefit is that unsafe can be buttoned up behind a safe API, hopefully in a way that is Zero Cost. So you might have some unsafe core that you need to pay extra special attention to, but the rest of your code can be in safe Rust. For example, I maintain a Snappy compression crate in Rust. It uses quit…

That's still not really unique to rust, D (at least) does that too. However, good point nonetheless.

Sure, it's not strictly unique. There are very few language features in any language that are unique. Language design is an evolutionary process. I wish I knew D better so I could provide a better comparison, but if I am to believe[1] and allow myself to wave my hands a bit, then there's a lot more you can do in safe Rust than in safe D. That's important, because if you wind up needing `unsafe` a lot, then you start to lose the possibility of buttoning up a small amount unsafe code behind a safe interface. (This is NOT to say that D's feature here is worthless, but the languages have very different designs and very different trade offs.)

Steve's point is also pertinent. Safe Rust is the default, so it's very easy to audit for places in your code that need extra care.

[1] - https://dlang.org/spec/memory-safe-d.html

Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+

#40

Post by oconnore »

unboxed_type wrote: post #24
oconnore wrote: post #22

Earlier quoted context omitted.

Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.

Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.

You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended.

If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.

Post reply on HN