I'm reading The Rust Programming Language and found the following passage:

Remember that writing to a struct is not an atomic operation, and many functions like vec.push() can reallocate internally and cause unsafe behavior, so even monotonicity may not be enough to justify UnsafeCell

It just popped out of nowhere in the book and I've had a hard time online trying to find what it exactly means in this context. Too much information is about the concept of "monotonicity" of mathematical functions, which I already knew but is apparently not very helpful.

I only seemed to find this article that talks about it.

Now, in addition to respecting equality in the obvious way, I also include the stipulation that a functional program must respect the monotonicity of observations. What do I mean by this? It must be that once you have observed something at a point in time, then that will not cease to be evident in the future. This is analogous to the monotonicity property in Kripke or Beth semantics.

However this is also quite abstract and I'm not sure it talks about the same thing either.


The author appears to be using the same (general) concept of "monotonicity" as in pure mathematics.

Using the example of a vector, if the size of some particular instance of vector is monotonic, then it would seem reasonable to assume that the memory location of any previously pushed element will not be subsequently modified, and thus that it is safe to directly change the value of that element without having to synchronize with the vector's subsequent push operations.

This assumption seems reasonable for much the same reason why it seems reasonable to assume that the memory location of an element previously pushed onto a (non-circular, array-based, unbounded) stack whose size is strictly increasing will not be affected by a future push operation. This stands in contrast to a stack on which both push and pop operations are being invoked, and so the memory location of a previously pushed element may be "removed" by a pop operation, and thus available to be assigned to once again (i.e. modified) by a subsequent push operation.

The author's point is that this assumption is not correct, since even in a data structure whose size is strictly increasing, future insertions may affect previously inserted elements by triggering an internal reallocation of some sort that is distinct from the "logical" effect of the insertion.

  • $\begingroup$ OK. Seems that I overthought it. Looks like it's not some deep PL theory stuff after all. Guess the way it was suddenly presented in the text without much context rubbed me the wrong way haha. $\endgroup$
    – xji
    Dec 11 '16 at 2:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.