Comment by Animats
2 days ago
The "flight pointer" looks an awful lot like a fat pointer. See the diagram at "The intuition of inviscaps" in [1]. A "flight pointer" has a pointer to the beginning of the buffer, which they call the "lower bound ptr", and a pointer to someplace within the buffer, which they call the "integer ptr". The pointer to the beginning of the buffer lets the checker find the size of the buffer, which is stored preceding the buffer. The compiler has to arrange things so that the lower bound ptr is carried around wherever a "flight pointer" goes. This is supposed to be invisible to the programmer.
other implementations of fat pointers (that I’m aware of) have no distinction between flight and rest; they store what I call flight pointers in memory literally.
The closest technique to invisicaps is softbound, but that has issues that invisicaps resolve (better story for races, more comprehensive safety for all of the C and C++ languages, no need for large virtual memory reservations, and lock freedom)