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

61–70 of 96 posts

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

#61

Post by joshuata »

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?

An interesting solution to this problem is verification witnesses[1]. A witness is a machine readable record of a verification task. Several different programs can read the witness and verify it independently. It is especially useful for counterexamples, where it can be a simple program trace to the error state. Given the input program and witness another can check whether the error state is reached.

[1] https://www.sosy-lab.org/~dbeyer/verification-witnesses/

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

#62

Post by EGreg »

If you're working with a language that has closures, I started to have a heuristic:

  // if you are writing a comment like this
  // explaining what the next block of code does
  // chances are you should just refactor it
  // into a closure
  _doWhateverCommentSaid(arg1, arg2, arg3);
it's true that this needlessly adds stack overhead, but this way, you are more likely to structure your code properly, re-use it properly (which more than pays for the stack overhead), and move your closure / method to be more and more global as needed.

Perhaps if you have a comment like this:

  f(x); // x matches some assumption
then in fact, you should add validation to f itself, in the form of a function, same as above.

  function f(x) {
     _theAssumption(x);
  }
this habit encourages re-use and proper structuring of code.

in short, comments may be an anti-pattern!

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

#63

Post by eridius »

EGreg wrote: post #62

If you're working with a language that has closures, I started to have a heuristic: // if you are writing a comment like this // explaining what the next block of code does // chances are you should just refactor it // into a closure _doWhateverCommentSaid(arg1, arg2, arg3); it's true that this needlessly adds stack overhead, but this way, you are more likely to structure your code properly, re-use it properly (which…

How does wrapping up code in a closure "fix" the need for comments? And what's wrong with having comments anyway? You haven't demonstrated that comments are an "anti-pattern", all you've demonstrated is that you personally prefer a different style.

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

#64

Post by samth »

nickpsecurity wrote: post #58
samth wrote: post #48

Earlier quoted context omitted.

Right, the concept of the TCB (trusted computing base) is the important thing. Good discussions of remaining TCB in verified code are in the seL4 work, or in this paper: https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf

See my link to Myreen's page and follow all those people's publications. Much of the TCB functions in papers like that has been eliminated in other work. It just needs to be cross-checked, integrated, and applied.

Right, that's one of the nice things about Appel's paper: he shows how to integrate a few different pieces to significantly reduce the TCB (ie, it doesn't include anything about C the language at all).

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

#65

Post by nickpsecurity »

samth wrote: post #64
nickpsecurity wrote: post #58

Earlier quoted context omitted.

See my link to Myreen's page and follow all those people's publications. Much of the TCB functions in papers like that has been eliminated in other work. It just needs to be cross-checked, integrated, and applied.

Right, that's one of the nice things about Appel's paper: he shows how to integrate a few different pieces to significantly reduce the TCB (ie, it doesn't include anything about C the language at all).

I think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.

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

#66

Post by EGreg »

eridius wrote: post #63
EGreg wrote: post #62

If you're working with a language that has closures, I started to have a heuristic: // if you are writing a comment like this // explaining what the next block of code does // chances are you should just refactor it // into a closure _doWhateverCommentSaid(arg1, arg2, arg3); it's true that this needlessly adds stack overhead, but this way, you are more likely to structure your code properly, re-use it properly (which…

How does wrapping up code in a closure "fix" the need for comments? And what's wrong with having comments anyway? You haven't demonstrated that comments are an "anti-pattern", all you've demonstrated is that you personally prefer a different style.

Whenever you put a comment, chances are you should have encapsulated the block there into a reusable block of code.

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

#67

Post by eridius »

EGreg wrote: post #66
eridius wrote: post #63

Earlier quoted context omitted.

How does wrapping up code in a closure "fix" the need for comments? And what's wrong with having comments anyway? You haven't demonstrated that comments are an "anti-pattern", all you've demonstrated is that you personally prefer a different style.

Whenever you put a comment, chances are you should have encapsulated the block there into a reusable block of code.

Why? You're saying that without any supporting evidence. And frankly, what you're suggesting sounds to me like an unreadable mess. You're going to bloat your code with closures all over the place, simply so you can attach a name to the closure, all to avoid having a simple comment. Naming closures is not a good substitute for comments.

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

#68

Post by nickpsecurity »

kibwen wrote: post #41
michaelmior wrote: post #9

Earlier quoted context omitted.

Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation is proven correct?

This is going to sound tautological, but the unsafe keyword is for operations that the compiler can't prove. The unsafe keyword only unlocks a very small number of possible new operations (it doesn't turn off any existing checks), and those operations make unsafe Rust as freeform as C; if you could prove unsafe Rust correct then you could just prove C code correct.

Which Frama-C, Simpl/C, and Astree Analyzer all do. Then that C code is quite trustworthy. Rust has stuff like Simpl in the works but needs something like Frama-C or SPARK for unsafe.

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

#69

Post by nickpsecurity »

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

C programmers could've had so much fun with that quote. ;)

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

#70

Post by kibwen »

nickpsecurity wrote: post #68
kibwen wrote: post #41

Earlier quoted context omitted.

This is going to sound tautological, but the unsafe keyword is for operations that the compiler can't prove. The unsafe keyword only unlocks a very small number of possible new operations (it doesn't turn off any existing checks), and those operations make unsafe Rust as freeform as C; if you could prove unsafe Rust correct then you could just prove C code correct.

Which Frama-C, Simpl/C, and Astree Analyzer all do. Then that C code is quite trustworthy. Rust has stuff like Simpl in the works but needs something like Frama-C or SPARK for unsafe.

Can you give me an example of something that safe Rust doesn't allow, thereby requiring the unsafe keyword to implement, but that also contains an error that passes the Rust compiler silently but that Frama-C or SPARK would statically detect?
Post reply on HN