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

11–20 of 96 posts

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

#11

Post by munin »

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 and runtime (but other work is ongoing to close that loop as well).

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

#12

Post by chrisseaton »

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…

The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?

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

#13

Post by nickpsecurity »

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…

That's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automatically. Those that aren't can be turned into runtime checks.

https://en.wikipedia.org/wiki/SPARK_(programming_language)

http://www.electronicdesign.com/industrial/rust-and-spark-so...

Here's an example of combining Event-B with SPARK to split overall verification between tools with each handling what they're good at:

https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f37...

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

#14

Post by nickpsecurity »

chrisseaton wrote: post #12
munin wrote: post #11

Earlier quoted context omitted.

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…

The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?

It's been done down to the hardware. Originally by Computational Logic Inc for FM9001 whose prover became ACL2. Then Verisoft went from apps to OS to C subset to VAMP processor (DLX-style). Recently people are doing HOL to hardware that will integrate with HOL/Light whose core is a few hundred or thousand lines to trust. Those people eliminated trust requirements in everything from extraction mechanisms to provers to assembly generation:

http://www.cse.chalmers.se/~myreen/

Follow he and his colleagues work for all that. Especially Milawa and CakeML. If you want a starting point, a small, Forth-like processor verifiable by hand on a node verifiable by eye could run the initial interpreter and prover for the first, real CPU. Plus, common practice is to split work into untrusted generation of artifacts with traces that are verified by a trusted checker that's comparatively tiny and simple. The little CPU would just run the checkers. You can run the generation on anything you like with the speed benefit. :)

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

#15

Post by [deleted] »

chrisseaton wrote: post #12
munin wrote: post #11

Earlier quoted context omitted.

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…

The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?

[deleted]

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

#16

Post by nicknash »

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 concurrency-checking, but it's silent on memory-models (implicitly sequentially consistent)

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

#17

Post by unboxed_type »

nickpsecurity wrote: post #13
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…

That's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automatically. Those that aren't can be turned into runtime checks. https://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.electronicdesign.com/industrial/rust-and-spark-so... Here's an example of combining Event-B with SPARK to split overall verification b…

How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation?

Runtime checks are good as to prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?

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

#19

Post by unboxed_type »

nickpsecurity wrote: post #14
chrisseaton wrote: post #12

Earlier quoted context omitted.

The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?

It's been done down to the hardware. Originally by Computational Logic Inc for FM9001 whose prover became ACL2. Then Verisoft went from apps to OS to C subset to VAMP processor (DLX-style). Recently people are doing HOL to hardware that will integrate with HOL/Light whose core is a few hundred or thousand lines to trust. Those people eliminated trust requirements in everything from extraction mechanisms to provers to…

What about real CPUs (much more complex than 'Forth CPU'), network adapters (has its own CPU), memory controllers, real OS kernels, POSIX library (which is sometimes loosely specified) and so on?

As far as I understand modern truly reliable system (commerical avionics-like) still must be relatively simple to be verified up to hardware level.

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

#20

Post by cabaalis »

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?
Post reply on HN