News for hackers. Stuff that matters.

A comment on Writing correct lock-free and distributed stateful systems in Rust, with TLA+. Parent comment

Re:Writing correct lock-free and distributed stateful system... by samth on Friday May 19, 2017 @01:58PM (#14377963)
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).
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @01:59PM (#14377976)
I think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by samth on Friday May 19, 2017 @05:34PM (#14379521)
No, I'm talking about the one I linked to, which is done in Coq.
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @09:15PM (#14380486)
Oh my bad. I just saw work such as seL4 then assumed it was a seL4 reference. I actually didn't have this one by Appel. Thanks for the paper! :)

Here's the one I was referencing with the tiny TCB:

https://www.cs.princeton.edu/~appel/papers/flit.pdf

OK. So, it was a few Kloc. Still smaller than Coq. They could probably get it even smaller with recent work given translation validation knocks compilers out of TCB. So, in between 803-2668loc.

[ Parent | on HN ]