Coding 2025-01-17
So, my focus has been questionable at best, but I am still considering how to prevent undefined behavior in a flexible way.
My hope is that I can attach a lot of information to the underlying address range, and some to individual pointers, using some kind of giant predicate that gets processed specifically with linear logic.
Let's imagine the simplest scenario that I suspect could totally muck this up:
We have two pointers to distinct address ranges, called a and b. a is stored in a third pointer, x, which has two copies. Next, b is stored in x. As a result, a is no longer accessible, and by extension, whatever it pointed to is no longer accessible. Conversely, b is accessible in its original location, as well as in both locations that x is accessible from.
One of the challenges I have to face is figuring out just how general I can make the general case. The idea I have is, it should be possible to take a pointer that nothing else knows about, stick it in a wrapper that provides desired guarantees and usage patterns, and then just go. Naturally, that bit requires substructural stuff to guarantee that the pointer can thereafter only be accessed through the wrapper. The whole point of such wrappers is that they provide different interfaces, so I suppose the design would be "there's no baseline behavior, rather a set of requirements from the various LLVM intrinsics, and implementing a wrapper requires somehow proving that you've satisfied those requirements". Requirements I have in mind include:
- The pointer is based on the address range. (Okay.)
- The address range is live. (All right.)
- The pointer has the required permissions. (Should be straightforward.)
- In the absence of synchronization, a pointer shared between threads can only be read. (... Oh no.)
- Some stuff about aliasing in the context of single-threaded code as well? Like, sometimes, we'd actually like to have funky behavior from passing the same pointer twice, and sometimes we'd like to be prevented from doing so.
Thinking about this, it's possible that I've been misinterpreting the meaning of "synchronization" just enough to freak myself out. I'll have to look over the LLVM docs some more later. For now, I really should get to bed.
Good night.