4 ms·

My type safety and confusion guards have nothing to do with colors of any kind. There are no finite colors to run out of. Fil-C totally allows pointer to integ

• woodruffw 2y ago
  > My type safety and confusion guards have nothing to do with colors of any kind. There are no finite colors to run out of. I'm having trouble seeing where the type confusion protection properties come from, then. I read through your earlier (I think?) design that involved isoheaps and it made sense in that context, but the newer stuff (in `gimso_semantics.md` and `invisicap.txt`) seems to mostly be around bounds checking instead. Apologies if I'm missing something obvious. > I’m citing unsafe transmute as something that Fil-C doesn’t prevent. It’s not something that memory safety prevents. I think the phrasing is confusing, because this is what the manifesto says: > No program accepted by the Fil-C compiler can possibly go on to escape out of the Fil-C type system. This to me suggests that Fil-C's type system detects I/O effects, but I take it that wasn't the intended suggestion.
  • pizlonator 2y ago
    Here’s a write up that goes into more detail: https://github.com/pizlonator/llvm-project-deluge/blob/deluge/gimso_semantics.md https://github.com/pizlonator/llvm-project-deluge/blob/delug...
    • woodruffw 2y ago
      I read that, but I'm not seeing where the type is encoded in the capability.
      • pizlonator 2y ago
        Short answer: if you know how CHERI and SoftBound do it, then Fil-C is basically like that. Long answer: let's assume 64-bit (8 byte pointers) without loss of generality. Each capability knows, for each 8 bytes in its allocation, whether those 8 bytes are a pointer, and if so, what that pointer's capability is. Example: char* p = malloc(64); This will allocate 64 bytes. p's capability will know, for each of the 8 8-byte slots, if that slot is a pointer and if so, what it's capability is. Since you just allocated the object, none of them have capabilities. Then if you do: *(int**)(p + 8) = malloc(sizeof(int)); Then p's capability will know that at offset 8, there is a pointer, and it will know that the capability is whatever came out of the malloc. Hence, each capability is dynamically tracking where the pointers are. So it's not a static type but rather something that can change over time. There's a bunch of engineering that goes into this being safe under races (it is) and for supporting pointer atomics (they just work).
      • pizlonator 2y ago
        BTW I wrote another doc to try to explain what's happening. Hope this helps. https://github.com/pizlonator/llvm-project-deluge/blob/deluge/invisicaps_by_example.md https://github.com/pizlonator/llvm-project-deluge/blob/delug...
        • woodruffw 2y ago
          Thank you, I found this very helpful!
        • fweimer 2y ago
          This is helpful as well because it at least alludes to the data structures: https://github.com/pizlonator/llvm-project-deluge/blob/deluge/invisicap.txt https://github.com/pizlonator/llvm-project-deluge/blob/delug... One more thing: I assume the memory allocator has a somewhat efficient way to recover the pointer to the start of the allocation from a pointer inside it, for interoperability with the legacy C world. For recompiled code, this is not used because the capability is either tracked in registers, or loaded from the shadow memory.
          • pizlonator 2y ago
            The GC does marking using the capability pointer, not the pointer's integer value. So, there's no need for a general "hey GC, what object does this point into and where does it start" query. The capability is the start of the allocation most of the time. It might have a bit in it saying that it's an aligned allocation (indicating alignment greater than 16 bytes), in which case there's an alignment hole between the start of what the GC thinks is the allocation and where the capability starts. Also capabilities might be global, meaning that there is no need to mark them. So, to mark a capability (which the runtime calls an "object"), the algorithm is something like: if (object->is_global) return; void* thing_to_mark; if (UNLIKELY(object->is_aligned)) thing_to_mark = object & -object->alignment; else thing_to_mark = object; mark(thing_to_mark);