5 ms·

True. I do think the ideal kind of memory safe language either has no "unsafe", or has an "unsafe" feature that only needs to be used in super rare an obscure

True. I do think the ideal kind of memory safe language either has no "unsafe", or has an "unsafe" feature that only needs to be used in super rare an obscure cases (Java is like that, sort of). Fil-C has no "unsafe", so in that sense Fil-C is safer than Rust. You don't need an escape hatch if the memory safety guarantees are dialed in just right.

titzer 2y ago
In Virgil, native targets have a couple of unsafe operations available, one of which is to be able to forge a closure from a pair of a code pointer and an object reference. This is used, e.g. to implement Wizard's JIT and fast interpreter, which generate new machine code at runtime. I can't imagine the level of proof necessary to make that safe--and not just the safety of the generated machine code, but it often lacks bounds checks because it relies on running verified Wasm bytecode, which cannot go out of bounds. So the proof would have to include a complete proof of correctness for the code validation algorithm (i.e. part of Wizard itself).
- pizlonator 2y ago
  I dream of a JIT API that lets you propose machine code that is checked using an abstract interpreter to ensure that you have adequate checks to stay within the host language's type system. Someday, man
  - porridgeraisin 2y ago
    I don't get this, can you explain?
    - pizlonator 2y ago
      Sure. If I told you that I have a snippet of machine code that: - obeys the ABI of your safe language (ie it has exactly the calling convention that safe language uses) - corresponds exactly to a function body whose signature is T->U (or whatever, different safe languages have different function type syntax) - obeys the language’s type system. Then you could run an abstract interpreter to check that the machine code follows that type system. Simple example: given the above claims, if we further assume that the host language impl puts argument one into register 5, and the first argument’s type is “pointer to an array of bytes”, and we know that arrays have a 64-bit length prefixed to the start, then the abstract interpreter would just need to check that any deref of register 5 is preceded by a bounds check on whatever was loaded at offset -8 from register 5. And so on, for every possible thing you can do in the language. Then the JIT would just have to make sure it puts checks in all of the places that the absint expects them. If the absint fails, then the machine code is rejected.
  - titzer 2y ago
    This will kill baseline JIT performance. I am trying out a couple of new directions, e.g. generating more of the tiers from a more abstract description, constantly shrinking the amount of hand-written compiler/interpreter code. My hard requirement is the end result has to be pretty darn close to what I'd write by hand. One thing I am thinking about now is how to make more use of the implementation language's (e.g. Virgil) compiler to be able to paste together machine code templates gotten from writing in the implementation language. Think copy-and-patch compilation, but as language primitive. E.g. "please emit an inlined copy of the machine code for this function (first-class ref to said function) into memory here, under this ABI".
    - pizlonator 2y ago
      > This will kill baseline JIT performance. You say that and then you describe exactly what I would have used as a solution: copy and patch. Just have the checker check the templates that the baseline JIT is stitching together and then have a safe way to ask for the prechecked templates to be stitched together. Bunch of details in getting that right obviously, but it doesn’t seem impossible.
      - titzer 2y ago
        We're not that far off from each other. > Just have the checker check the templates that the baseline JIT is stitching together Sure, from my second paragraph, the templates it's using could be opaque things it got from requesting the static compiler generate a template from a first class function ref (at compile time), in which case the verification has already been done.
        pizlonator 2y ago
        I think we're saying the same thing
hotjump 2y ago
The problem of C code migration to memory safe languages is that legacy C projects aim for extremely high performance. Garbage-collecting languages would also be safe in any situation, but I want to note that the recent tendency toward Rust derives from its type-system based approach that imposes very few runtimes checks such as bound checking. I myself hope something like F* gets more attraction in the industry.
- pizlonator 2y ago
  I hear the perf claim a lot and yet most of the time when I write C/C++ code it's not because it's the most performant. It's either because I'm editing a codebase that's already in C/C++, or I'm using libraries whose best (or only) bindings are C/C++, or because I want to make syscalls (and safe languages don't expose those as nicely as C).
  - rrrix1 2y ago
    For desktop, server, web, mobile, etc. This holds true. Not so much for embedded systems, anything with unnatractive memory capacity or processor performance. Rust is starting to make it's way in, but C and even assembly is still king AFAIK.
    - pizlonator 2y ago
      And yet there are embedded systems running JavaScript and Python.
      - kv85s 2y ago
        Are there any real-world, production systems based on JavaScript and Python? Toy systems, yes. Hey, I too, think CircuitPython is really neat. But I'm skeptical someone would base a PLC (or similar) on it.
        ckcheng 2y ago
        Above was talking about embedded systems, and I really don’t know if the James Webb Space Telescope counts, but… The James Webb Space Telescope runs JavaScript, apparently [1]. [1]: https://www.theverge.com/2022/8/18/23206110/james-webb-space-telescope-javascript-jwst-instrument-control https://www.theverge.com/2022/8/18/23206110/james-webb-space...
amluto 2y ago
I think there’s a sense in which Rust is safer than Fil-C, though: Rust allows abstractions with little to do with memory safety but that still can’t be broken without 'unsafe'. So a struct called EvenNumber can fairly strongly guarantee that it contains an even number. But Fil-C objects (at least for now?) only seem to allow one single capability type, and that capability grants unrestricted read/write access to the object’s bytes. I wonder if one could build a handle system in Fil-C that would allow this to be extended. Or if a different variant of a Fil-C-like system could distinguish between pointers with different access levels to an object and could allow only the correct piece of trusted code to increase the permission of a pointer.
- pizlonator 2y ago
  I’ve thought about adding such things to Fil-C but have held off on going there because it feels like a bridge too far. What I mean by that is: the memory safety issues of C are a total dumpster fire, while whether a number is even or not (and whether you can prove that) is maybe like icing on the dumpster fire. It just doesn’t matter by comparison. So I want to decisively fix the memory safety issues and not lose focus.
imtringued 2y ago
Have you thought about building a C verification framework around Fil-C? Fil-C doesn't necessarily have to run in production. It just needs to catch the bugs, e.g. by making it easy to fuzz C code compiled via Fil-C.
- pizlonator 2y ago
  I think you should run Fil-C in production.
  - transpute 2y ago
    Why not both?

titzer 2y ago

In Virgil, native targets have a couple of unsafe operations available, one of which is to be able to forge a closure from a pair of a code pointer and an object reference. This is used, e.g. to implement Wizard's JIT and fast interpreter, which generate new machine code at runtime. I can't imagine the level of proof necessary to make that safe--and not just the safety of the generated machine code, but it often lacks bounds checks because it relies on running verified Wasm bytecode, which cannot go out of bounds. So the proof would have to include a complete proof of correctness for the code validation algorithm (i.e. part of Wizard itself).

pizlonator 2y ago
I dream of a JIT API that lets you propose machine code that is checked using an abstract interpreter to ensure that you have adequate checks to stay within the host language's type system. Someday, man
- porridgeraisin 2y ago
  I don't get this, can you explain?
  - pizlonator 2y ago
    Sure. If I told you that I have a snippet of machine code that: - obeys the ABI of your safe language (ie it has exactly the calling convention that safe language uses) - corresponds exactly to a function body whose signature is T->U (or whatever, different safe languages have different function type syntax) - obeys the language’s type system. Then you could run an abstract interpreter to check that the machine code follows that type system. Simple example: given the above claims, if we further assume that the host language impl puts argument one into register 5, and the first argument’s type is “pointer to an array of bytes”, and we know that arrays have a 64-bit length prefixed to the start, then the abstract interpreter would just need to check that any deref of register 5 is preceded by a bounds check on whatever was loaded at offset -8 from register 5. And so on, for every possible thing you can do in the language. Then the JIT would just have to make sure it puts checks in all of the places that the absint expects them. If the absint fails, then the machine code is rejected.
- titzer 2y ago
  This will kill baseline JIT performance. I am trying out a couple of new directions, e.g. generating more of the tiers from a more abstract description, constantly shrinking the amount of hand-written compiler/interpreter code. My hard requirement is the end result has to be pretty darn close to what I'd write by hand. One thing I am thinking about now is how to make more use of the implementation language's (e.g. Virgil) compiler to be able to paste together machine code templates gotten from writing in the implementation language. Think copy-and-patch compilation, but as language primitive. E.g. "please emit an inlined copy of the machine code for this function (first-class ref to said function) into memory here, under this ABI".
  - pizlonator 2y ago
    > This will kill baseline JIT performance. You say that and then you describe exactly what I would have used as a solution: copy and patch. Just have the checker check the templates that the baseline JIT is stitching together and then have a safe way to ask for the prechecked templates to be stitched together. Bunch of details in getting that right obviously, but it doesn’t seem impossible.
    - titzer 2y ago
      We're not that far off from each other. > Just have the checker check the templates that the baseline JIT is stitching together Sure, from my second paragraph, the templates it's using could be opaque things it got from requesting the static compiler generate a template from a first class function ref (at compile time), in which case the verification has already been done.
      - pizlonator 2y ago
        I think we're saying the same thing

hotjump 2y ago

The problem of C code migration to memory safe languages is that legacy C projects aim for extremely high performance. Garbage-collecting languages would also be safe in any situation, but I want to note that the recent tendency toward Rust derives from its type-system based approach that imposes very few runtimes checks such as bound checking. I myself hope something like F* gets more attraction in the industry.

pizlonator 2y ago
I hear the perf claim a lot and yet most of the time when I write C/C++ code it's not because it's the most performant. It's either because I'm editing a codebase that's already in C/C++, or I'm using libraries whose best (or only) bindings are C/C++, or because I want to make syscalls (and safe languages don't expose those as nicely as C).
- rrrix1 2y ago
  For desktop, server, web, mobile, etc. This holds true. Not so much for embedded systems, anything with unnatractive memory capacity or processor performance. Rust is starting to make it's way in, but C and even assembly is still king AFAIK.
  - pizlonator 2y ago
    And yet there are embedded systems running JavaScript and Python.
    - kv85s 2y ago
      Are there any real-world, production systems based on JavaScript and Python? Toy systems, yes. Hey, I too, think CircuitPython is really neat. But I'm skeptical someone would base a PLC (or similar) on it.
      - ckcheng 2y ago
        Above was talking about embedded systems, and I really don’t know if the James Webb Space Telescope counts, but… The James Webb Space Telescope runs JavaScript, apparently [1]. [1]: https://www.theverge.com/2022/8/18/23206110/james-webb-space-telescope-javascript-jwst-instrument-control https://www.theverge.com/2022/8/18/23206110/james-webb-space...

amluto 2y ago

I think there’s a sense in which Rust is safer than Fil-C, though: Rust allows abstractions with little to do with memory safety but that still can’t be broken without 'unsafe'. So a struct called EvenNumber can fairly strongly guarantee that it contains an even number. But Fil-C objects (at least for now?) only seem to allow one single capability type, and that capability grants unrestricted read/write access to the object’s bytes. I wonder if one could build a handle system in Fil-C that would allow this to be extended. Or if a different variant of a Fil-C-like system could distinguish between pointers with different access levels to an object and could allow only the correct piece of trusted code to increase the permission of a pointer.

pizlonator 2y ago
I’ve thought about adding such things to Fil-C but have held off on going there because it feels like a bridge too far. What I mean by that is: the memory safety issues of C are a total dumpster fire, while whether a number is even or not (and whether you can prove that) is maybe like icing on the dumpster fire. It just doesn’t matter by comparison. So I want to decisively fix the memory safety issues and not lose focus.

imtringued 2y ago

Have you thought about building a C verification framework around Fil-C? Fil-C doesn't necessarily have to run in production. It just needs to catch the bugs, e.g. by making it easy to fuzz C code compiled via Fil-C.

pizlonator 2y ago
I think you should run Fil-C in production.
- transpute 2y ago
  Why not both?