logoalt Hacker News

bangaladorelast Wednesday at 11:41 PM1 replyview on HN

A SAFETY comment is supposed to justify why the unsafe code is sound. Here it justified the wrong thing. Ownership was not the problem, concurrent mutation was. That is exactly the kind of gap a SAFETY comment can hide by giving a false sense that the hard parts were already considered.

The fact that this survived review is the worrying part. Unsafe blocks are intentionally small and localized in Rust precisely so the safety argument can be checked. If the stated safety argument is incomplete and still passes review, that suggests reviewers are relying on the comment as the proof, rather than rederiving the invariants themselves. Unless of course the wrong people are reviewing these changes. Why rewrite in Rust if we don't apply extreme scrutiny to the tiny subset (presumably) that should be scrutinized.

To be clear, I think this is a failure of process, not Rust of course.


Replies

aw1621107yesterday at 2:52 AM

> Ownership was not the problem, concurrent mutation was.

I think the safety comment might have been more on-point than you think. If you look at the original code, it did something like:

- Take a lock - Swap a `Node`'s `death_list` (i.e., a list of `NodeDeath`s) with an empty one - Release the lock - Iterate over the taken `death_list`

While in another thread, you have a `NodeDeath`:

- Take a lock - Get its parent's `death_list` - Remove itself from said list. - Release the lock

The issue is what happens when a `NodeDeath` from the original list tries to remove itself after the parent Node swapped its `death_list`. In that case, the `NodeDeath` grabs the replacement list from its parent node, and the subsequent attempt to remove itself from the replacement list violates the precondition in the safety comment.

> Why rewrite in Rust if we don't apply extreme scrutiny to the tiny subset (presumably) that should be scrutinized.

That "extreme scrutiny" was applied does not guarantee that all possible bugs will be found. Humans are only human, after all.