SaberVM(ryanbrewer.dev)
ryanbrewer.dev
SaberVM
https://ryanbrewer.dev/posts/announcing-svm.html
6 comments
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 the JVM both do this as well, for the same reason. A big difference from those projects, 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). 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 runtime, and therefore uses regions (in tandem with something like Vale's generational references).
2) I don’t really get the exceptions thing
The exceptions thing is meant to be a lightweight way of getting the reliability of Erlang's BEAM VM, using a common approach to exceptions in CPS-based compilation. Having a built-in notion of exceptions means that whenever an instruction fails, it can jump to the exception handler instead of crashing. That way parts of the program can be cleaned up and even restarted during the execution, instead of just crashing.
3) What features could a higher-level language have that would make the most of SaberVM’s unique characteristics?
A higher level language that compiles to SaberVM bytecode might give more control over memory management than existing functional languages. Things like support for stack allocation, arena allocation, in-place mutation of values that are used linearly, and unboxed, nonuniform memory representations of values. I might also use an actor system for concurrency, since the CPS style makes stackless coroutines trivial to implement and the exception system and parallelism instructions should be able to do a good enough job at something BEAM-like. Lastly, I would definitely surface the exception system as a feature of the language, for the sake of writing your own exception handlers.
4) Are those features really hard to implement in Wasm?
Unfortunately Wasm isn’t a great target for functional programming at the moment. It uses structured control flow as a big part of its security, with ifs and loops and whatnot. Functional languages, on the other hand, use recursion for loops, so they often use jumps for function calls, or else they’d likely run into stack overflows. Very recently, Wasm added “tail calls,” that is, when a function returns the result of another function, that function can use the stack space of the current function, essentially freeing that space early. Wasm added this mostly to support functional languages better, since it saves stack space quite a lot. I intend to write a transpiler from SaberVM to Wasm at some point in the near future, that uses the new tail call feature. But even then, functional languages use polymorphism for their security, not structured control flow, and there’s just a number of philosophical differences that make compiling to Wasm a pain for functional languages. And lastly, Wasm doesn’t have any way to do the things the BEAM is known for, namely, massive parallelism with extremely resilient concurrency. I know there are proposals on parallelism but given the fact that Wasm is meant to run in the browser first and foremost, this will never be a big goal for it.
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.
5) Conclusion :)
As you can see from my discussion of this stuff, these ideas all precede me. My region analysis is from a Krary, Walker, and Morrisett paper. I use something like generational references from Vale. I'm taking significant inspiration from the JVM, Wasm, and the BEAM. My only contribution here is figuring out how to put these pieces together into a tight, portable little system.
And in the interest of executing things without a VM, I'm thinking a lot about AOT-compiling the bytecode to native binaries as well.
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 the JVM both do this as well, for the same reason. A big difference from those projects, 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). 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 runtime, and therefore uses regions (in tandem with something like Vale's generational references).
2) I don’t really get the exceptions thing
The exceptions thing is meant to be a lightweight way of getting the reliability of Erlang's BEAM VM, using a common approach to exceptions in CPS-based compilation. Having a built-in notion of exceptions means that whenever an instruction fails, it can jump to the exception handler instead of crashing. That way parts of the program can be cleaned up and even restarted during the execution, instead of just crashing.
3) What features could a higher-level language have that would make the most of SaberVM’s unique characteristics?
A higher level language that compiles to SaberVM bytecode might give more control over memory management than existing functional languages. Things like support for stack allocation, arena allocation, in-place mutation of values that are used linearly, and unboxed, nonuniform memory representations of values. I might also use an actor system for concurrency, since the CPS style makes stackless coroutines trivial to implement and the exception system and parallelism instructions should be able to do a good enough job at something BEAM-like. Lastly, I would definitely surface the exception system as a feature of the language, for the sake of writing your own exception handlers.
4) Are those features really hard to implement in Wasm?
Unfortunately Wasm isn’t a great target for functional programming at the moment. It uses structured control flow as a big part of its security, with ifs and loops and whatnot. Functional languages, on the other hand, use recursion for loops, so they often use jumps for function calls, or else they’d likely run into stack overflows. Very recently, Wasm added “tail calls,” that is, when a function returns the result of another function, that function can use the stack space of the current function, essentially freeing that space early. Wasm added this mostly to support functional languages better, since it saves stack space quite a lot. I intend to write a transpiler from SaberVM to Wasm at some point in the near future, that uses the new tail call feature. But even then, functional languages use polymorphism for their security, not structured control flow, and there’s just a number of philosophical differences that make compiling to Wasm a pain for functional languages. And lastly, Wasm doesn’t have any way to do the things the BEAM is known for, namely, massive parallelism with extremely resilient concurrency. I know there are proposals on parallelism but given the fact that Wasm is meant to run in the browser first and foremost, this will never be a big goal for it.
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.
5) Conclusion :)
As you can see from my discussion of this stuff, these ideas all precede me. My region analysis is from a Krary, Walker, and Morrisett paper. I use something like generational references from Vale. I'm taking significant inspiration from the JVM, Wasm, and the BEAM. My only contribution here is figuring out how to put these pieces together into a tight, portable little system.
And in the interest of executing things without a VM, I'm thinking a lot about AOT-compiling the bytecode to native binaries as well.
> 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 trivial to even check types in.
> The JVM doesn't try to guarantee memory safety
Wait, what? I always thought that (barring JNI and so on) Java bytecode was completely memory-safe (having been intended to run mutually suspicious code in the first place), it’s just that this is accomplished at the cost of pervasive tracing GC and bounds checks everywhere.
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 trivial to even check types in.
> The JVM doesn't try to guarantee memory safety
Wait, what? I always thought that (barring JNI and so on) Java bytecode was completely memory-safe (having been intended to run mutually suspicious code in the first place), it’s just that this is accomplished at the cost of pervasive tracing GC and bounds checks everywhere.
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.
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.
> 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 runtime, and therefore uses regions (in tandem with something like Vale's generational references).
This "deficiency" doesn't appear to have held back the JVM from being wildly successful. To what extent do you think it matters then?
This "deficiency" doesn't appear to have held back the JVM from being wildly successful. To what extent do you think it matters then?
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.
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.
> 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 in meeting functional programmers' expectations?
F# in Webassembly via Bolero - https://fsbolero.io
How well do you think it succeeds in meeting functional programmers' expectations?
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.
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.
> 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.
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.
Just realized I misspelled Karl Crary's last name! It should be Crary, not Krary. Embarrassing!
In 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.
This 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.
[deleted]
Reminds 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.
[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.
What's some stuff you'd like to see in a higher level language that would fit the design nicely?
Are those things really hard to implement on top of WebAssembly?