[deleted]
SaberVM
11–20 of 21 posts
Re: SaberVM
#12In this post I announce a new abstract machine oriented towards executing functional languages in a memory-safe and portable way.
excellent progress, love to see it. time to retarget an ocamlopt for it yet, or not quite ready for such experimentation?
Definitely not ready for that just yet. I've just started making the project public, it's still a little far from a usable state. I love the energy though! I'll post about my progress along the way.
Re: SaberVM
#13Reminds me of HVM[0] [0] https://github.com/HigherOrderCO/HVM Really interesting to see how new lang concepts and refinements keep popping up this last decade, between Vale, Gleam, Hylo, Austral... Linear types really opened up lots of ways to improve memory management and compilation improvements.
Totally! It's a really exciting time to be in langdev.
Re: SaberVM
#14Earlier quoted context omitted.
Yeah I wrote that targeting a more langdev audience, to be fair. Those are great questions! There’s a lot to answer there so unfortunately my answer is a bit long, I hope that’s ok. 1) Why have regions in the VM instead of compilers that target it? SaberVM does its own analysis of the bytecode given to it to make sure its safe. That way, if you receive SaberVM bytecode, you don't have to trust it blindly. Wasm and th…
> A big difference from [Wasm and the JVM], though, is that SaberVM's analysis includes memory safety, like Rust. For that, it uses regions (as well as Vale's system, which is a big inspiration). What about the verification complexity? The JVM screwed this part up somewhat, from what I understand, while Wasm is carefully designed to be linear to parse and verify throughout. And complex type systems aren’t always triv…
The type system is stolen from some of the work on TAL (typed assembly language), by Greg Morrisett and others. In my implementation at the moment it's linear first in the size of the program and then there's a little more checking that's linear in the number of functions. The design is still settling, and it very well might be just linear in the future.
Your point about garbage collection is very fair. For some reason in my head when I wrote that I thought of null pointer exceptions, but that is indeed a different thing.
Re: SaberVM
#15I'm not a language author, so I'm not getting any lightbulbs about why its nice to build regions into the VM rather than the compiler. I see the appeal of the region thing which reminds me of Vale ( https://verdagon.dev/blog/zero-cost-borrowing-regions-overvi... ). I didn't really get the exceptions thing. What's some stuff you'd like to see in a higher level language that would fit the design nicely? Are those thing…
Yeah I wrote that targeting a more langdev audience, to be fair. Those are great questions! There’s a lot to answer there so unfortunately my answer is a bit long, I hope that’s ok. 1) Why have regions in the VM instead of compilers that target it? SaberVM does its own analysis of the bytecode given to it to make sure its safe. That way, if you receive SaberVM bytecode, you don't have to trust it blindly. Wasm and th…
> Wasm doesn't make any memory safety guarantees about the usage of memory within the Wasm runtime
fyi, that was true for Wasm 1.0, but WasmGC defines managed memory structures (structs with typed fields, arrays with bounds checking, isorecursive subtyping, immutability, etc.) which provide fully verified memory safety.
Re: SaberVM
#16Earlier quoted context omitted.
Yeah I wrote that targeting a more langdev audience, to be fair. Those are great questions! There’s a lot to answer there so unfortunately my answer is a bit long, I hope that’s ok. 1) Why have regions in the VM instead of compilers that target it? SaberVM does its own analysis of the bytecode given to it to make sure its safe. That way, if you receive SaberVM bytecode, you don't have to trust it blindly. Wasm and th…
> The JVM doesn't try to guarantee memory safety, and Wasm guarantees it by sandboxing the runtime from the rest of the computer. However, Wasm doesn't make any memory safety guarantees about the usage of memory within the Wasm runtime. Since SaberVM is trying to be a first-class execution environment like the JVM, instead of an embedded one like Wasm, it has to make guarantees about the usage of memory within the ru…
That's true, mostly because of the JVM's garbage collection. SaberVM also hopes to be a good way to run untrusted code, like the JVM, but it can run much lower level, higher performance code safely, using arenas and the theory powering Vale. AOT compiled SaberVM bytecode can have optimization passes that remove many of the checks, like Vale has now, and that can still be done on the client's computer in a safety-preserving way.
The JVM also comes from an era of OOP being a very pervasive norm, which helped Java's popularity a lot. My impression is that the JVM is seen by many as an annoying bottleneck and massive dependency that's the cost of using Java, a language they enjoy.
Re: SaberVM
#17Earlier quoted context omitted.
Yeah I wrote that targeting a more langdev audience, to be fair. Those are great questions! There’s a lot to answer there so unfortunately my answer is a bit long, I hope that’s ok. 1) Why have regions in the VM instead of compilers that target it? SaberVM does its own analysis of the bytecode given to it to make sure its safe. That way, if you receive SaberVM bytecode, you don't have to trust it blindly. Wasm and th…
> Wasm doesn't make any memory safety guarantees about the usage of memory within the Wasm runtime fyi, that was true for Wasm 1.0, but WasmGC defines managed memory structures (structs with typed fields, arrays with bounds checking, isorecursive subtyping, immutability, etc.) which provide fully verified memory safety.
Wasm has a lot of great proposals that excite me but has other disqualifying factors for me. I don't want to be required to use garbage collector, I'm concerned about how much Wasm is growing in scope with all the proposals, I'm (relatedly) concerned about portability and my ability to write my own runtime for Wasm that stays compatible in the long run, and I want a runtime that isn't browser-first, merely browser-supporting.
Re: SaberVM
#18Earlier quoted context omitted.
Yeah I wrote that targeting a more langdev audience, to be fair. Those are great questions! There’s a lot to answer there so unfortunately my answer is a bit long, I hope that’s ok. 1) Why have regions in the VM instead of compilers that target it? SaberVM does its own analysis of the bytecode given to it to make sure its safe. That way, if you receive SaberVM bytecode, you don't have to trust it blindly. Wasm and th…
> SaberVM is intended to be what functional programmers wish Wasm was: a statically typed runtime system that could be run in the browser but isn’t primarily for that, which could functional languages could easily compile to in a way that preserves the sort of polymorphism-based security reasoning that functional programs depend on. F# in Webassembly via Bolero - https://fsbolero.io How well do you think it succeeds…
Yeah there are a number of successful compilers from functional languages to Wasm. It's definitely doable. I just wanted a backend that was more focused on being a portable target for functional languages. Throughout these comments I list a number of issues I take with Wasm. It's cool and I want a SaberVM->Wasm transpiler soon but the Wasm spec definitely doesn't look like something I want to be tied to in the long run.
To answer your question more specifically, I've heard from a number of people that the structured control flow of Wasm is pretty painful to deal with when writing a compiler. Doing a relooper pass over a CPS or even SSA IR should not be a necessary step. I get the sense that many compromises are made for Wasm to work.
Re: SaberVM
#19This looks like a cool project. It looks like it is up to the host language to compile to bytecode and do all the type analysis before passing that info to the verifier. Looks like there is no VM yet, it just verifies the bytecode and then prints it. But it looks like the host language must also be written in Rust because the main `go` method is expecting rust types. Is that correct?
Re: SaberVM
#20This looks like a cool project. It looks like it is up to the host language to compile to bytecode and do all the type analysis before passing that info to the verifier. Looks like there is no VM yet, it just verifies the bytecode and then prints it. But it looks like the host language must also be written in Rust because the main `go` method is expecting rust types. Is that correct?
Mostly right. We're still in a prototyping phase for sure. The verifier is still in progress, the execution will follow. That said, the main method of the program reads from a file called `bin.svm` which has the bytecode, and which could be generated by any language that can do binary file I/O. There will be more ways to hook into the VM in the future, as well as other SaberVM implementations that compile the bytecode to native binary or Wasm.