[verdagon]

Hey all, this is a post explaining a new memory safety model by my friend Nick Smith (original proposal at https://gist.github.com/nmsmith/cdaa94aa74e8e0611221e65db8e4...)

It was interesting enough that I knew I had to write a post about it. Happy to answer any questions!

[wpollock]

> But... we humans can easily conclude this is safe. After the evaluation of list_ref_a.push(5), my_list is still there, and it's still in a valid state. So there is no risk of memory errors when evaluating the second call to push.

Is the always true? What with piplining, branch prediction, and maybe asymmetrical NUMA , isn't out of order instructions possible? If so, don't you still need locks or memory barriers to ensure safety?

(I am most definitely not an expert, just curious.)

[nmsmith]

Hardware-based instruction reordering always preserves the behaviour of the original program. (Assuming the original program is valid.)

For example, an Intel CPU won't reorder `x += 1` and `x *= 2`.

[titzer]

Thanks for the detailed writeup, that must have been a lot of work.

I think you guys should check out Verona (https://www.microsoft.com/en-us/research/project/project-ver...).

[verdagon]

Big fan of Verona, I love their memory safety approach as well. I wrote a bit about it in the Grimoire [0] too. IIRC they plan for the user to specify whether a region is backed by an arena allocator or GC, which sounds pretty nice. It's kind of hard to track down details though, most of my knowledge comes from reading David Chisnall's comments on lobste.rs.

[0] https://verdagon.dev/grimoire/grimoire