On the design of unsafe operations

[kyouko-taiga]

This discussion is continuing from this answer and the comments on it. I'm opening a new thread to avoid "polluting" one with the other.

What does “handled” mean?

I used "handled" to relate unsafe to throws. You "handle" an unsafe region by vetting that it is indeed safe in places where the compiler can't say. Let's not get fixated on the definition of "handle" though. I only used it to establish the similarities I believe hold between the effects and because it is a word typically associated with effect systems. What's important to my mental model is that try gives you license to use throws(_:) and unsafe gives you license to call an unsafe function. I don't think we disagree on that.

That's not the only way; if you are in a function marked throws, you don't have to utter try.

That depends on your definition of region. You enter a dynamic region when you start evaluating an expression, and that region typically covers more than the text of the expression. In particular, it can cover a call to an unsafe function. That is important because we must guarantee that no unsafe operation can run outside of a dynamic unsafe region.

But I doubt the same should apply to unsafe, because there are very often still plenty of safe operations in such functions and the unsafe markings help with vetting.

I disagree but I can understand the worry that people could write overly long unsafe functions. Then Hylo would devolve into C++ for the users who love clever pointer arithmetic. Writing long unsafe functions should be the smelliest of the smells, but some people have code anosmia. So for the sake of the argument, let's say we want a marker of some sort on unsafe statements but let's not settle on unsafe just yet.

My problem is with functions like this:

/// Does some amazingly efficient business and returns our the captain's age.
///
/// - Requires: `x` refers to initialized memory.
fun unsafe_business(_ x: Pointer<Int>, unsafe?: Unsafe) -> Int {
  let y = PointerToMutable<Int>.allocate(count: 1)
  unsafe y.initialize_pointee(to: 10)
  return unsafe y[] + unsafe x[]
}

There's an important difference between unsafe y[] and unsafe x[] in this function for the user who wrote it:

• The first unsafe can be vetted. They can look at the pre/post-conditions of all the operations in scope and conclude that they wrote safe code.
• The second unsafe can't be vetted. They don't know in what state the pointee of x is when we're called and can only trust that the caller satisfied their precondition. Because that isn't enforceable by the language, they asked for an unsafe capability to make sure the caller pays more attention.

The user wouldn't have had to ask for unsafe if x was a let parameter. So what I'm trying to illustrate here is that there are fundamentally two kinds of unsafe calls: the ones we can verify and the ones requiring our caller (on which we have no control in general) to have verified some precondition for us. From this observation, I claim that the marker of unsafe [x] is really the one we got as an argument, and that's why I don't want to write it.

This is a bad example for the purposes of this discussion [...]

Well, for the purpose of the discussion we do need to think about how we bootstrap the whole "requires unsafe" business. Most likely that will start in standard library functions wrapping some built-in operations. And then then the point I discussed above applies. To run base as* (remote sink Pointee) I need to be sure that base points to initialized memory. As the author of Pointer. pointee I have no way to tel. So I documented my precondition and asked for an unsafe capability to make sure the caller pays extra attention.

[dabrahams]

Thanks for moving this discussion. Let me start by restoring a little more context:

if I use an unsafe operation in a larger operation, must that larger operation be considered unsafe in the type system? I think the answer may be no.

I think the answer is: yes, unless you handled then unsafety in the nested operation.

What does “handled” mean?

And you just replied:

I used "handled" to relate unsafe to throws. You "handle" an unsafe region by vetting that it is indeed safe in places where the compiler can't say. [emphasis mine] Let's not get fixated on the definition of "handle" though.

The whole reason I started to ask about your definition is because, given that the compiler can't say, it doesn't make any sense to me as an answer about whether something is true in the type system, which was what I asked.

I only used it to establish the similarities I believe hold between the effects and because it is a word typically associated with effect systems. What's important to my mental model is that try gives you license to use throws(_:) and unsafe gives you license to call an unsafe function. I don't think we disagree on that.

We do not.

But I doubt the same should apply to unsafe, because there are very often still plenty of safe operations in such functions and the unsafe markings help with vetting.

I disagree but I can understand the worry that people could write overly long unsafe functions. Then Hylo would devolve into C++ for the users who love clever pointer arithmetic. Writing long unsafe functions should be the smelliest of the smells

Sure; I'm much more worried about long supposedly-safe functions that include a few unsafe operations. Those are not as likely to be carefully vetted by anyone doing API-first code review (the only right way to do it of course 😉). And I'm not entirely attached to marking every unsafe statement but I don't think it can be dismissed out of hand based on conclusions we've made about throwing.

There's an important difference between unsafe y[] and unsafe x[] in this function for the user who wrote it:

• The first unsafe can be vetted. They can look at the pre/post-conditions of all the operations in scope and conclude that they wrote safe code.
• The second unsafe can't be vetted.

I will assume that by “safe code” you mean “code that, regardless of its inputs (e.g. x) satisfies the preconditions of all unsafe operations it uses.” If that's right, sure you can vett the first dereference for safety but can't vett the second one.

If this were a safe function, that would be a meaningful difference, but that doesn't fulfill a safety reviewer's obligation for this unsafe function. The reviewer must gather everything they know, including the stated preconditions of the function, and prove that the state preconditions of all unsafe operations are satisfied, which means vetting both of these dereferences. The reason they have to do that, of course, is that code that uses unsafe_business needs to be able to trust that satisfying its preconditions is sufficient to fulfill whatever safety promises that code makes.

Because that isn't enforceable by the language, they asked for an unsafe capability to make sure the caller pays more attention.

? Neither one is enforceable by the language. If the first one were enforceable by the language we'd have put it in the type system and uses of y would be safe.

The user wouldn't have had to ask for unsafe if x was a let parameter.

?? It is a let parameter.

So what I'm trying to illustrate here is that there are fundamentally two kinds of unsafe calls: the ones we can verify and the ones requiring our caller (on which we have no control in general) to have verified some precondition for us. From this observation, I claim that the marker of unsafe [x] is really the one we got as an argument, and that's why I don't want to write it.

Sorry, but: ??? I don't know what “the marker of unsafe [x]” is. I don't see [x] in the code.

Maybe you mean that you could have made this function safe if it weren't for the need to write x[]… and the need to write x[] is what causes the caller to need to pay more attention… but I can't see any reason why that should impact what's worthy of attention in the callee.

This is a bad example for the purposes of this discussion [...]

Well, for the purpose of the discussion we do need to think about how we bootstrap the whole "requires unsafe" business.

The original discussion I was trying to have was a different one; it was not as broad as “the design of unsafe operations,” and the obvious approach to bootstrapping you described (with an unused-in-the-type-system unsafe parameter) seems, well, obvious—and non-problematic—to me. Is there anything further to discuss about that?

[kyouko-taiga]

The whole reason I started to ask about your definition is because, given that the compiler can't say, it doesn't make any sense to me as an answer about whether something is true in the type system.

In general, when I say that the type system can assume something, it doesn't mean that the compiler must guarantee that it is true. You can convince the type system that an Optional<Int> contains an Int and in general the compiler has no way to tell.

unsafe means something very similar to me. When you write unsafe e you tell the type system that it can trust you; that e is guaranteed not to run undefined behavior regardless of the values that it uses or captures, and so the "unsafety" doesn't have to propagate outward any further.

From there I feel important to distinguish between two potential uses of the keyword unsafe and so for the sake of clarity I will use different keywords from now:

The way I see it, we have strawman1 e meaning "I checked and e cannot cause undefined behavior" and strawman2 e meaning "e may run undefined behavior depending on what it uses or captures". My first point is that strawman2 must not be the same keyword as strawman1. My other point is that I don't think strawman2 is necessary at all.

Sure; I'm much more worried about long supposedly-safe functions that include a few unsafe operations.

If you have a supposedly-safe function then in my world you need strawman1 in front of every unsafe operation. If you want to promise a safe API, then you have to convince the type checker that your implementation won't run UB no matter what gets in.

fun f(p: Pointer<Int>) {
  // many, many lines
  let x = p[] // <- nop! That is unsafe and you didn't write `strawman1`
  // many, many more lines
}

The dangerous function is the one that is unsafe and relies on unenforceable preconditions:

/// - Requires: `p` refers to initialized memory.
fun g(p: Pointer<Int>, unsafe?: Unsafe) {
  // many, many lines
  let x = p[] // <- nop? That is unsafe and we didn't write `strawman1` or `strawman2`
  // many, many more lines
}

The reason why we can use strawman2 instead of strawman1 in g is that the vetting is allowed to depend on an unsafe precondition. f was declared a safe function and so the vetting must be done locally [Note: it is probably impossible to implement f in this example]

I will assume that by “safe code” you mean “code that, regardless of its inputs (e.g. x) satisfies the preconditions of all unsafe operations it uses.” If that's right, sure you can vett the first dereference for safety but can't vett the second one.

Yes, that is what I mean.

If this were a safe function, that would be a meaningful difference, but that doesn't fulfill a safety reviewer's obligation for this unsafe function.

We agree on the principle. My position is really that:

• strawman1 and strawman2 are distinct markers
• I am not yet convinced that strawman2 is necessary

Neither one is enforceable by the language.

My point is that guaranteeing that the precondition is satisfied is beyond the author's control, which is unlike guaranteeing the initialization state of y's pointee. There is no reason to ask an unsafe capability otherwise and it should perhaps even be a compiler error or warning (i.e., something like "function is marked unsafe but its implementation does not depend on any unvetted precondition").

It is a let parameter.

I'm talking about x's pointee, not x.

I don't know what “the marker of unsafe [x]” is. I don't see [x] in the code.

It's a typo, sorry. I meant "the marker of unsafe x[]", which I referred to it as strawman2 in this message.

Is there anything further to discuss about that?

Probably not. But note that if strawman2 is necessary, then the unsafe capability wouldn't be unused anymore. You need one to write strawman2.

[dabrahams]

The whole reason I started to ask about your definition is because, given that the compiler can't say, it doesn't make any sense to me as an answer about whether something is true in the type system.

In general, when I say that the type system can assume something, it doesn't mean that the compiler must guarantee that it is true.

In this discussion you haven't said the type system can “assume” anything, so I can't connect this to anything that's come before, nor can I understand its relevance. I asked a question about deductions made by the type system and you answered that it depends on things that you yourself say the type system has no way to know about. If you want me to ignore that apparent inconsistency, just say so, but I think it's important for you to understand why I started trying to nail down your definitions.

When you write unsafe e you tell the type system that it can trust you; that e is guaranteed not to run undefined behavior regardless of the values that it uses or captures, and so the "unsafety" doesn't have to propagate outward any further.

I agree with that in principle, but I think we may differ on what “guaranteed” means. For me, in an unsafe function such a guarantee is implicitly conditional: it depends not the values that e uses or captures, but on the surrounding function's preconditions having been upheld.

From there I feel important to distinguish between two potential uses of the keyword unsafe and so for the sake of clarity I will use different keywords from now:

The way I see it, we have strawman1 e meaning "I checked and e cannot cause undefined behavior" and strawman2 e meaning "e may run undefined behavior depending on what it uses or captures". My first point is that strawman2 must not be the same keyword as strawman1. My other point is that I don't think strawman2 is necessary at all.

Me neither, and I never intended to suggest that it was necessary (perhaps strawman2 is in fact a strawman?). Can we go back to saying unsafe rather than strawman1 now?

Sure; I'm much more worried about long supposedly-safe functions that include a few unsafe operations.

If you have a supposedly-safe function then in my world you need strawman1 in front of every unsafe operation. If you want to promise a safe API, then you have to convince the type checker that your implementation won't run UB no matter what gets in.

Well, I know this is just a qualitative difference, but I'd say you have to promise it that your implementation won't run UB no matter what gets in. There's not a whole lot of convincing in this promise; you just say so for each unsafe operation.

Also, IIUC, it's very easy to (even unintentionally) subvert this "each unsafe operation" requirement in the scheme you've proposed because a single unsafe marker will propagate automatically into closures, so for example

unsafe someOptional.map { 

   // as much unsafe stuff as you want here without uttering `unsafe`.

}

fun f(p: Pointer<Int>) {
  // many, many lines
  let x = p[] // <- nop! That is unsafe and you didn't write `strawman1`
  // many, many more lines
}

Obviously (?) I'm not concerned about code we know won't compile! I'm a bit concerned about the same code when you add the one unsafe marker, because lots of code review never gets past reading signatures, contracts, and tests. That's why I've suggested functions like f should be required to be explicitly marked safe.

The dangerous function is the one that is unsafe and relies on unenforceable preconditions:

/// - Requires: `p` refers to initialized memory.
fun g(p: Pointer<Int>, unsafe?: Unsafe) {
  // many, many lines
  let x = p[] // <- nop? That is unsafe and we didn't write `strawman2`
  // many, many more lines
}

The reason why we (maybe) need strawman2 instead of strawman1 in g is that the vetting can't be done locally.

I absolutely and fundamentally disagree with that. The safety vetting required in an unsafe function is, as I said before, to gather everything including the stated preconditions of the function, and prove that the stated preconditions of all unsafe operations are satisfied. That is done entirely locally. This vetting for an unsafe function is absolutely necessary to uphold the kind of reasoning you are saying can be done locally.

If this were a safe function, that would be a meaningful difference, but that doesn't fulfill a safety reviewer's obligation for this unsafe function.

We agree on the principle. My position is really that:

• strawman1 and strawman2 are distinct markers
• I am not yet convinced that strawman2 is necessary

The distinction is both artificial and counterproductive. In an unsafe function all unsafe operations need to be vetted against the function's preconditions, or the author of a supposedly-safe function that calls this unsafe function will never be able to reliably prove safety. They will reason locally just as you have illustrated based on the stated preconditions of the unsafe function, and if satisfying the unsafe function's preconditions doesn't actually prevent UB, their reasoning will be invalid.

My point is that guaranteeing that the precondition is satisfied is beyond the author's control, which is unlike guaranteeing the initialization state of y's pointee. There is no reason to ask an unsafe capability otherwise and it should perhaps even be a compiler error or warning (i.e., something like "function is marked unsafe but its implementation does not depend on any unvetted precondition").

The compiler can't tell what's been vetted and what hasn't, that message wouldn't make any sense to me. I have to assume you mean that the compiler should warn if you take an Unsafe parameter but don't use it to perform any unsafe operations. You'd have a lot of corners to deal with to make that work, starting with bootstrapping the standard library and continuing with satisfying unsafe protocol requirements with safe implementations… but sure.

I don't know what “the marker of unsafe [x]” is. I don't see [x] in the code.

It's a typo, sorry. I meant "the marker of unsafe x[]", which I referred to it as strawman2 in this message.

Is there anything further to discuss about that?

Probably not. But note that if strawman2 is necessary, then the unsafe capability wouldn't be unused anymore. You need one to write strawman2.

Wait a sec, are you actually suggesting that, in a world without strawman2, this should be allowed?

/// Does some amazingly efficient business and returns our the captain's age.
///
/// - Requires: `x` refers to initialized memory.
fun unsafe_business(_ x: Pointer<Int> /*, unsafe?: Unsafe */) -> Int { // <== No `unsafe` capability
  let y = PointerToMutable<Int>.allocate(count: 1)
  unsafe y.initialize_pointee(to: 10)
  return unsafe y[] + x[]
}

This is an unsafe operation that you can call without having the capability; you can't possibly mean you're in favor of that, can you? But I don't know how else to read “the unsafe capability won't be unused anymore.“