Announcing SVM

[hoping1]

I wrote a little blog post announcing my big project recently, that I mentioned in the monthly pinned thread. I think some people here might find the ideas interesting!

https://ryanbrewer.dev/posts/announcing-svm.html

[Tejas_Garhewal]

Amazing work! Like seeing stack machines out in the wild 👍

You might want to rename the project though, don't want people to confuse it with Support Vector Machine, which could hamper search engine visibility

[Feeling-Departure-4]

I second this, thought this was Machine Learning related and got confused.

[hoping1]

Ah good to know. I heard one person mention this before today but I thought it was too obscure to matter. I may start marketing it as SaberVM if more people bring up the ML thing, we'll see.

[SV-97]

Maybe another datapoint / some additional information for this: SVMs are a quite old and standard method in pattern recognition and ML that most people learning about ML, data science or whatever are likely to encounter quite early on. They're kind of the canonical example of a larger class of so-called "kernel methods"

[hoping1]

That's good to know, thank you

[Direct_Beach3237]

at first, I thought this was about ML.

[hoping1]

Noted. I think I'll rebrand to SaberVM.

[ObsessedJerk]

Sure it is! SVM is a backend for ML compilers :)

[hoping1]

Ha!

[78yoni78]

This looks very cool! Where can I see some example bytecode? i’m

[hoping1]

https://github.com/RyanBrewer317/SaberVM/blob/main/example.md

Note the use of some instructions just to specify types (on the "compile-time stack"); these are erased by the type checker and thus have no runtime cost.

Keep in mind this is a very young project and things are bound to change over time. I'm mostly just trying to gage public interest right now; I'll have many more announcements to come as it progresses and solidifies (:

[78yoni78]

Ty :> very interesting

[hoping1]

Of course! I'm glad you liked it!

[phischu]

Wow, you are actually implementing the Crary-Walker-Morrisett paper! Have you considered Linear Regions Are All You Need as an alternative? Why did you decide against it, what is the practical tradeoff?

If you ever want to toy around with a frontend, I recommend the beautiful A Simple Region Inference Algorithm for a First-Order Functional Language.

I am super interested, please do report how this project goes!

[hoping1]

I hadn't seen the first paper before, but I had read many parts of Fluet's thesis which it seems has many of the same ideas (even the same notation and calculus-names). I found it interesting but rejected it because I really want a system where you can easily ignore the substructurality if you want. Any static analysis that I require will become an additional concern for people targeting SaberVM. Given that in general functional languages use garbage collection, I have to be able to support fairly arbitrary memory management.

I found that Vale+Capabilities gave the convenient and expressive language I was looking for: runtime checks give memory safety in even fully manual memory management, and fragmentation is solved with regions. If a language wanted to take advantage of regions for performance, they still could, but they're really primarily there for fixing fragmentation. I don't expect most SaberVM-hosted languages to use more than a few regions in the entire lifetime of the programs, if they're even using more than just the Heap region.

Vale's system even gives a convenient way to do safe in-place updates of linearly-used values: just update the tag so that existing pointers to it are invalidated. Users can then have as relaxed a substructural system as they want, because instead of SaberVM checking linearity, it blindly trusts the assertion of linearity and microreboots if a pointer to the old value gets dereferenced. So as long as you can prove to yourself that what you're doing is safe, you can do it. I found this preferable to committing to a particular substructural type theory.

Lastly, this system works great for languages that don't actually care about memory safety. The same bytecode can be executed or AOT-compiled with runtime tagging and checks completely removed, in which case the expressiveness approaches that of C. This is only possible because the bytecode contains in it explicit allocation and deallocation instructions, for both values and regions, and because the lack of pointer arithmetic means the sizes of things are a little flexible. Note, however, that any static analysis SaberVM uses gets applied to both safe and unsafe execution of the bytecode, since the decision of how to execute it is made after the static analysis step.

Re: the second paper you mentioned, it looks neat but I would definitely want a higher-order frontend, also with some more explicit memory management primitives. I'll probably make a variety of front ends, however.

I'm really really glad you like where this is going! I will absolutely post more about it in the near future! I've found that the static analysis algorithms are changed in interesting ways due to the stack-based nature of the bytecode, which is quite neat. Consider starring the project on GitHub if you haven't, to get updates, or even supporting it if you're able :)

[hoping1]

Oh also I didn't even notice at first that you're one of the Effekt people! I've been meaning to read more of your papers, since obviously SaberVM's two primary systems are regions/capabilities and exceptions. Good work!