4 ms·
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 objec
by 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 agoI 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 agoI don't get this, can you explain?
- pizlonator 2y agoSure. 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 agoThis 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 agoWe'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 agoI think we're saying the same thing