RustBelt: Logical Foundations for the Future of Safe Systems Programming

http://plv.mpi-sws.org/rustbelt/#project

by ingve • 11 years ago

98 16 11 years ago

plv.mpi-sws.org

bitL• 11 years ago

How do you address the inherent unsafeness of hardware? Even "pure" functional languages are hacking around this...

pjc50• 11 years ago

Elaborate on what you mean please?

johnbender• 11 years ago

Assuming you mean the weak memory models, the compiler normally enforces the guarantees made by the semantics of the programming language ... assuming you have a semantics.

That's where this project comes in and that is why the C++ memory model definition/formalization was so important. Programmers need to know what guarantees the compiler gives about the behavior of the code after compilation and the semantics is the final word.

GolDDranks2• 11 years ago

What do you mean? Do you mean that hardware is unreliable or might break and thus even a sound program, or a program that doesn't do anything that counts as unspecified behaviour, is not 100% safe? Or that with "unsafe" escape hatches often needed to directly interop with hardware are a problem?

GolDDranks2• 11 years ago

If it's the former, I agree.

If it's the latter, well, in Rust, the norm is to design safe abstractions around unsafe code. For example the vector class of the Rust standard library contains some unsafe code, but with the all parts that are unsafe being private, the public API exposed is essentially safe.

If this project comes up with reasonable semantics what can be considered to be "safe" with unsafe code, we can verify, that the unsafe bits of the standard library (and other libraries) are being used in a safe manner.

bassislife• 11 years ago

I think the assumption is that the hardware spec is correctly implemented and that it runs ideally well. Otherwise that would require some kind of probabilistic model I guess. But you're right, "purity" is a simplification. Computations are inherently effectful(and even side-effectful depending on the reference frame) in practice.

Also, I seem to understand that the research is merely done in the context of the Rust language. The title is maybe a bit too much :)

pcwalton• 11 years ago

How do you address the inherent unsafeness of hardware? Even "pure" functional languages are hacking around this...

By proving the hardware correct. Then if you're running proven memory safe Rust on formally verified hardware, you're guaranteed by construction that the Rust you're writing is memory safe (for the formally-specified notion of "correct" and "memory-safe" in use, which will probably issues like manufacturing problems and compiler bugs).

A Google search for [hardware formal verification] can get you started, if you're interested. There's been a good deal of work in this area.

irq-1• 11 years ago

Rust 1.5 src has 2121 instances of "unsafe {". Didn't expect it to be so high.

kibwen2• 11 years ago

That's not a particularly useful metric, because that would also be counting all the occurences in documentation (Rust makes extensive use of executable docstrings, so restricting your search to just .rs files doesn't solve the problem), test cases (where you absolutely want lots of tests for unsafe functionality, and Rust often puts tests in the same file as the functions being tested, so excluding certain directories doesn't solve the problem), all the APIs that wrap C interfaces (where unsafe blocks are necessarily unavoidable), and bits of the compiler itself (for e.g. talking to LLVM).

Even then, the standard libraries are exactly where you want your unsafe code to be; safely encapsulating useful unsafe patterns in a highly-visible and well-audited venue is ideal, and reduces the usage of unsafe code in (presumably less well-audited) third-party libraries.

akkartik2• 11 years ago

Here's a concrete data point in rust 1.5.0 to critique:

  $ grep 'unsafe {' src/lib* -r |wc -l
  1529

I'm skipping src/test and src/doc and a few other things, so this is likely a mild under-estimate on that front.

Docstrings seem to always require a comment leader, so let's ignore any lines where the first non-whitespace characters are not '//'.

  $ grep 'unsafe {' src/lib* -rh |grep -v "^\s*//" |wc -l
  1480

Inline tests are created using 'mod test', so let's look:

  $ grep 'mod test {' src/lib* -rl |wc -l
  6
  $ grep 'unsafe {' `grep 'mod test {' src/lib* -rl` |wc -l
  13

So of 1.5k occurrences, 13 lie in modules with inline tests. Let's conservatively ignore them all.

Final count of non-docstring non-test occurrences of 'unsafe {' in the 1.5.0 sources: 1463.

Animats2• 11 years ago

They're hiring "postdocs". Do "postdoc" positions in Germany mean, as in the US, paying $30K for people who could make $200K in industry?

samth• 11 years ago

CS postdocs in the US are certainly not paid $30k.

Source: I've been a postdoc in CS, and I currently employ postdocs.

Animats2• 11 years ago

OK, $44K. [1]

[1] http://www.payscale.com/research/US/Job=Postdoctoral_Researc...

RustBelt: Logical Foundations for the Future of Safe Systems Programming

Related Stories