[klodolph]

> To summarise, I still don't see how these two sentences are different: ...

To "observe unsafe behavior" means I can write a program that does something safe, e.g., a data race or invalid memory access. It's possible to write library X and Y in such a way that I can observe unsafe behavior using both X and Y in my program, without putting "unsafe" blocks in my program. This is possible even if I can't do the same thing with either X or Y alone.

This is surprising, because it means that the naive definition of "safe interface" is not actually safe enough!

[dbaupp]

I'm still not understanding: other than the hardware/global state thing in another comment in this thread[1], what's a program that demonstrates this "composing safe interfaces is unsafe" property? The example in the paper is not one, it was a bug for crossbeam to mark its API safe.

[1]: I'm ignoring this case, because it's somewhat completely impossible to solve: there's no way Rust (or any language) can control this situation. And, there's a strong argument in my mind that this sort of scenario should have an `unsafe` constructor or something, to act as an assertion from the programmer that they're guaranteeing unique access to the resource.

[AstralStorm]

There is a way. You have to meticulously prove operations down to machine code to not have externally observable side effects.

You can weaken the condition by excluding, say, timing effects or cacheline effects. (Say hello to Spectre)

This means you get to prove bounded access and data race freedom on any piece of memory safe code touches. Likewise prove bounded access for all unsafe code and correct cpu flag and state handling.

It it's not as bad as it seems - you can use the machine code prover designed for seL4 as a good starting point.

[Rusky]

The definition of what you're allowed to do with `unsafe`, however nebulous its specifics may be at the moment, is that such a situation is a bug in one or both of those libraries, not their composition.

To put it another way, if you can't observe unsafety with X or Y alone, but you can with both together, then at least one of them has given you a new capability that you did not have before. Either that new capability is not truly safe, and thus the bug is providing that capability, or it exposes the other library relying on something not truly safe, and thus the bug is relying on that property.

The important point here is that, by definition, at least one of X or Y will have to change when such a situation is discovered, in order to preserve the property that composing safe interfaces is safe.