HVM: history and next steps of the massively parallel functional runtime written in Rust
twitter.com/VictorTaelin/status/1588332432587...Posted Nov 4, 2022, 1:40 AM UTC
15847
twitter.com
It always astonishes me how some people can be hyper productive. I just don't understand how all of this has been able to be produced in such a short timespan.
18
tinnitus
19
It always astonishes me how some people can be hyper productive
Motivation. It's motivation. Some people are able to miraculously avoid burnout and demotivation. I have no idea how.
I know that I have a lot of potential because I've made a lot of very significant drive-by contributions but I can just never put that potential to use.
7
I'd say it is more determination, but honestly I'm the perfect storm to be productive. I'm over sensitive to basically any kind of external stimuli - light, sound, smells - so I don't really enjoy going out. And I also find anything that isn't extremely challenging unbearably boring, so I don't even enjoy watching movies, musics, relaxing indoors. So I just spend most of my time programming or gaming. Things are built that way. Don't be harsh with yourself if you're not like that, it is ok to do the things that make you happy. It just happens that the things I enjoy coincide with productive stuff to me.
24
Don't be harsh with yourself if you're not like that, it is ok to do the things that make you happy.
Except I badly want to do things that I don't have the motivation to do (i.e. finish certain projects I abandoned, learn to draw, etc.) and my inability to properly do those things makes me very unhappy.
So you are lucky :)
8
Not being judgemental, but you might look into therapy (depression, anxiety) or ADHD. You can't just blame yourself for not being good enough, find the root cause and fix it in a blameless manner.
5
I feel like I could do it if I gave up on physical exercise and exclusively ate takeout, but my body wouldn't take a week to begin falling apart.
3
Damn this is really interesting. If HVM really can give a linear speed up to CUDA of all things then I am very impressed. In theory could this same logic also be applied to compiling other GPU based programs such as SPIRV/GLSL code?
12
The whole point of HVM-GPU is to let us write shaders (like, 3D renderers, ray tracers, image generators) as high-level functions, and let them run with reasonable performance. For example, imagine writing the following code:
render : State -> Image
render state =
let scene = getScene state
let cam = getCam state
let img = new_image 512 512
map (\ pos -> ray_trace scene cam pos) img
I.e., a pure function that involves recursion, allocation of datatypes, high-order lambdas, and so on... and then compiling it to run on the GPU, rendering a real-time image with zero added effort? That's HVM's goal in that front. That said, it isn't meant to be more performant than hand-written GLSL code, nor will replace it when you need every drop of performance. In short, HVM is about compiling high-level languages to GPUs, not about making GPUs faster.
17
The whole point of HVM-GPU is to let us write shaders (like, 3D renderers, ray tracers, image generators) as high-level functions, and let them run with reasonable performance. For example, imagine writing the following code:
I.e., a pure function that involves recursion, allocation of datatypes, high-order lambdas, and so on... and then compiling it to run on the GPU, rendering a real-time image with zero added effort? That's HVM's goal in that front.
I don't see how this is even possible. You would have had to do so much work here to get this to function that you might has well have written a better imperative shading language than have spent effort on this.
And reasonable performance... that means a lot of things to different people. For example, is optimal stream compaction even possible with this system? Because the difference between non optimal and optimal stream compaction isn't "10%" or even "50%" it's multiple factors. And that's a pretty basic operation on the GPU.
Any time any of these "automatic/easy parallizers" come a long, I roll my eyes. They always seem to come at this from the theoretical and the MIMD/ CPU simple SIMD mindset, and seem to completely forget huge performance multipliers (which are not often functional at all) like subgroup operations, shared memory, forward progress guarantees with atomic flagging, locality atomics, using texture samplers for automatic memory locality and linear interpolation acceleration outside of image data, ILP, simultaneous f16,f32,and i32 etc... Heck models like mesh shading and raytracing pipelines (which if you don't support invalidates any notion of raytracing being reasonable with this system) might even be completely incompatible with this model with out significant effort. Those things are not function.
Honestly, while I'd like all projects like this to succeed, if SYCL can't get this right, I don't understand how this project can.
7
To be fair, we're so close to releasing this that I'd rather show it is possible by just building it
17
There is whole bunch of stuff that shakes out of the term rewriting this system does as it executes. It's mindbending how it works.
3
I see. Thank you for your thoughtful response. I understand it a lot better now.
4
I remember stumbling on this long ago.
One big thing this enables is stream fusion, where you bump into the problem that two chained operations might be more efficient if they happened as one operation in a stream, but fusing them makes the code uglier.
The rewriting and execution system will basically get you stream fusion for free in many cases.
2
HVM is one of those rare developments that sounds too good to be true, but does in fact live up to the hype.
10
Could you expand on how it lives up to the hype?
Maybe I'm a bit too cynic, but I'm weary of projects with such grandiose claims that mainly wield what looks like apples-to-oranges benchmarks. Doubly so if they are mostly single-maintainer projects and haven't seen much outside use or verification of their claims.
The three tweets with graphs look good on first glance, but don't translate to any insight about HVM:
-
HVM vs. GHC - HVM != GHC (only implements a subset of it), and as the author admits, a better optimized GHC program could actually beat it
-
Kind2 vs. other proof assistants - Not sure what scope Kind2 can handle relative to the other proof assistants. Would also be interesting to actually see the performance of Lean (the most recent one with traction) on the charts, since they have been implemented in the benchmark repo
-
Kindela vs. Ethereum - Kindela != Ethereum, and given that you tweak the EVM model to this degree, similar performance has been achieved via many other methods (and isn't usually a limiting factor of an Ethereum-like blockchain that people optimize for)
To me, it gives of the vibe that the author severely downplays (or underestimates) the limitations of HVM, and it looks like other people that tried to use the system share the same sentiment.
This all sounds quite harsh, and if it were more of a hobby project I'm not sure I would have written it.
u/SrPeixinho, given that you are actually trying to build a company around this, I would seriously recommend you to find a real-world validation as fast as possible and don't pour too much time on further proof-of-concepts that are too far removed from real-world usage.
You clearly seem to be talented and it would be a shame to see you get hurt. I'm sure there are companies out there that would pay a good buck for speeding up their Haskell programs, if you are actually able to deliver that for real-world programs. (Hint, since you mentioned it: Elm is a commercial dead-end)
25
Thanks for bringing up these concerns! I'll address them in order.
HVM vs. GHC - HVM != GHC (only implements a subset of it)
That's partially true indeed, but it is not a subset, it is a disjoint union. There are programs that HVM computes that GHC doesn't; arguably more important than the esoteric λ-terms that GHC does. For example, we can have linear normalization-by-evaluation, which is an extremely powerful tool to write interpreters, and isn't even expressive in traditional functional languages. It is just a different model of computation. Also note this is about direct evaluation, HVM is Turing Complete and you can write a full λ-calculus interpreter on it.
and as the author admits, a better optimized GHC program could actually beat it
I think you miss the point here. HVM isn't about achieving maximum possible performance. It is about making massive parallelism trivial. To the programmer, all that matters is the program he wrote, and how fast it ran. So, we compare almost identical inputs given to GHC and HVM. What else would you do?
Kind2 vs. other proof assistants - Not sure what scope Kind2 can handle relative to the other proof assistants.
It does the same thing. Check all the Kind programs and proofs on Wikind, it is quite pretty! It is missing some features for now, like high-order unification and type-classes, that were not included in the benchmarks and do not affect the performance results.
Would also be interesting to actually see the performance of Lean (the most recent one with traction) on the charts, since they have been implemented in the benchmark repo
Sadly, Lean stack overflows or hangs before even the smallest test case on every chart, so it was impossible to show it.
Kindela vs. Ethereum - Kindela != Ethereum, and given that you tweak the EVM model to this degree, similar performance has been achieved via many other methods
That's true for SSTORE, fair point. But not for the gains on functional opcodes, unless you replicate the HVM. This is very relevant to security, which is IMO the main thing people should be improving on blockchains (but nobody cares, until it is too late...).
And it looks like other people that tried to use the system share the same sentiment
That sounds sadly misleading to me. The problem he claims that should be solved, is already solved (since last decade), and I've even shown an example algorithm:
-
Check if the input program is EAL-typeable
-
If yes, compile to HVM directly
-
If not, compile to a full λ-Calculus evaluator on HVM
I really don't get why this point is repeated so often, it is simply not true that one can't compile functional programs to the HVM! The author claims that it is hard to design an expressive checker that detects if a program is safe to compile to the HVM, but that's not surprising, for the same reasons it is hard to make a borrow checker for Rust that detects all programs that are safe. That didn't stop Rust from being widespread, right? You can still start small, be conservative, and slowly make the checker smarter as users complain that certain safe programs were blocked by it.
I also never heard anyone claiming HVM has limitations that prevent it from being used for any of the applications I highlighted in the tweets. If you have one in mind, please let me know what it is?
I would seriously recommend you to find a real-world validation as fast as possible and don't pour too much time on further proof-of-concepts that are too far removed from real-world usage.
What do you suggest us to do, concretely? Compilers and runtimes are the base of every program that runs in every computer, so it looks pretty relevant to real-world applications. But I honestly do not know all the companies using Haskell to perform CPU-bound computations, that would pay to get their back-ends faster. That's actually a valuable information we should be researching, as it could give us such real-world validation. I have no doubt HVM could massively speed up certain Haskell workloads; the main obstacle would be a general GHC-Core -> HVM compiler, but that can be avoided by manually compiling the relevant portions of the specific code we're looking to optimize.
This all sounds quite harsh
Because it is, but it is good to be critical and I welcome that.
24
Glad you are taking it well!
What do you suggest us to do, concretely? Compilers and runtimes are the base of every program that runs in every computer, so it looks pretty relevant to real-world applications.
Yes, compilers and runtimes in general are established to be relevant real-world applications. You just have to show that your compilers/runtimes do.
Where I think the majority of the remaining skepticism lies (like in the GH thread I linked), is whether it's actually feasible to integrate HVM into a general purpose language like Haskell (or alternatively establish your full own language, but that's a much bigger endeavour).
It isn't true that one can't compile a functional language to HVM, and I even shown an example algorithm
I think going ahead and doing that in practice with a language like Haskell would be one of the best validations you could get, and from that point on it should be possible for the HVM-based system to hold up in an apples-to-apples comparison.
Very very concretely (based on what I've seen other startups with similar challenges do) I would go ahead and look for a company that has a problem you are poised to solve well (e.g. big Haskell codebase that could benefit from the optimizations) and get them to pay for a POC for exactly that use-case. Optimally this is able to finance your whole team for the duration of the POC, gives you market validation and gives you time to progress your technology overall. Many bigger companies are surprisingly willing to finance projects like this with the "only" thing they are getting out of it being a better performing system (and the created IP staying with you / being open source).
10
I think going ahead and doing that in practice with a language like Haskell would be one of the best validations you could get, and from that point on it should
The main problem is this is more of a Haskell challenge than an HVM one. GHC Core is huge, and compiling it to anything is hard. GHCJS, for example, was a colossal effort to compile Haskell to JavaScript, and was discontinued for being too complex. Elm, Agda and Idris would be easier to handle, and we're building Kind, which is a Haskell-like language meant to make real world programs. Perhaps what we really should do is compile a pure subset of JavaScript or even Python to the HVM...
Very very concretely I would go ahead and look for a company that has a problem you are poised to solve well and get them to pay for a POC for exactly that use-case.
Yes, that looks like a reasonable route. We'll be considering it.
8
[deleted]
0
I heard about HVM when it was first announced here, and am excited to see what applications it will enable!
9
I've been looking all around for non-GC Haskell or Common Lisp compiler, but all were obsolete or immature, so I settled with the thought Rust is enough even though it isn't strictly functional. Seeing this now gives me new hopes and having it written in Rust is a big bonus to me because I'll be able to contribute without suffering from reading C using all kinds of GCC extension hacks. :D
9
It was from 1997, by Yves Lafont, who attempted to answer that very question with a genius take: the fundamental laws of computation are "commutation and annihilation". From that insight, he derived a new model of computation, the Interaction Net.
This is somewhat subjective, but it feels that these "All of computation boils down to X" models that come from researchers in math-heavy academic backgrounds focus a lot on things like big-O complexity and purity of computation, and ignore the fact that in real-world architecture the big bottleneck isn't computations so much as memory access, which heavily depend on access patterns.
Eg the best data structure for a given task by Big-O notation might be a linked list, while in realistic use-cases it's a VecDequeue because the linked list jumps all over memory while the Vec keeps all data nice and adjacent.
(Functional languages in particular tend to have a tendency to go "let's put everything on the heap, the GC will take care of it, that way we can use cons-lists everywhere and our functions will remain pure!")
This seems especially important for GPU work, where computation is cheap and memory access is super-expensive.
In your experience, is this a problem with interaction nets, and if so how does HVM-GPU handle it?
9
I think you're mostly right, however, much of software development, especially for GPUs and other massively parallel processors involves a lot of effort for very poor utilization of the hardware.
Also this time it's different :)
Looking at the original paper some of the HVM docs, because the order of computation doesn't matter at all, and because it is described at such a high level, an intelligent compiler is free to rearrange the program to optimize for cache/memory and possibly reduce high-latency (IO) operations.
4
"An intelligent compiler"
Many a technology has tanked waiting on a "Sufficiently intelligent compiler". Itanium.
9
Anyone who focuses on Big O probably doesn't even understand the theoreticals, honestly. The fact that Big O only describes scaling, and not baseline speed, is basically the first thing you learn about it. Memory access speed is just yet another constant factor to take into account, so such researchers probably don't even understand what they're doing.
Edit: beyond my comment on your comments regarding researchers focusing too much on things that don't matter as much in the real world, I just took a cursory glance at Interaction Nets and they seem to not really fit your assumption very well. They appear to try to reduce the amount of communication and synchronisation needed, which seems like a good thing for models of computation applied to GPUs.
2
Is there a good dumbed-down explanation of "the interaction net" somewhere, or should I read the original paper?
7
https://github.com/Kindelia/HVM/blob/master/HOW.md is a bit simpler than the original paper
5
The description of the cheap clone system reminds me of that other nascent language posted here that used value-types ( no references ) and under the hood the compiler figured cloning as needed.
2
I swear there's always someone interesting on this sub, I'm so glad I subbed to it.
6
Perhaps there is a relation between Rust being so damn good and people building cool things on it :)
10
Interesting project indeed! Can't say I understand much about the theory behind it, I have some reading to do I suppose. :)
Specifically I don't understand how the cheap, lazy cloning works without using references. Let's say you have a fully evaluated tree structure in memory and then want to create a new modified version. In Haskell that would simply entail cloning the modified tree nodes and otherwise reference nodes from the previous tree (a persistent data type). This means there would be at least two references to some old nodes, which in turn would require a GC (for example ref counting) to free the data when both references are free'd. How does HVM solve this case without GC?
And what about arrays? Does HVM support them, or can they be added to the calculus? Performing parallel operations on arrays is by far the most efficient way to utilize current hardware (CPU's, GPU's and tensor chips). For example, for efficiency reasons you will not use a simple tree structure, but rather something like Scala's Vector type.
4
As for persistent data types, lazy duplications work exactly like references in that case, because the cloning is triggered only for the branches that are needed, so the tree structure isn't touched. For example, if you have (in Rust dialect):
fn foo(i: u32, map: Map) -> u32 {
if ...base_case... {
return map.get(...key...);
} else {
let map = map.insert(...key..., ...val...);
return foo(i * 2, map.clone()) + foo(i * 2 + 1, map.clone());
}
}
Suppose this function recurses 16 times, so, there are 65536 invocations to the base case. It would look like map is cloned more than 65536 times, but since clones are lazy, each base case only generates the branch it need. For example, on the i=0 base case, we would clone the branch 0, and collect (i.e., not even generate) the branches 1..65536. And so on. Ultimately, the amount of work is the same as you'd have with references.
And what about arrays? Does HVM support them, or can they be added to the calculus? Performing parallel operations on arrays is by far the most efficient way to utilize current hardware (CPU's, GPU's and tensor chips).
No, HVM avoids arrays at all costs, since they don't mix well with lazy duplications. That is why HVM will never outperform a hand-optimized parallel program that makes extensive use of mutability! But it does give you massive parallelism for free, which is what makes it so cool. And, of course, a HVM hardware wouldn't have that problem, as the interaction net model would enable on-chip optimizations that'd, in theory, let it compensate for the lack of mutable arrays.
6
It would look like map is cloned more than 65536 times, but since clones are lazy, each base case only generates the branch it need.
Yes, I understand that part. What I don't understand is how you implement lazy clones without keeping a reference/pointer to the thing to clone inside the lazy clone.
3
Reading your twitter thread, and the HOW.md doc, my mind swims with use cases in distributed data analysis (sending computation to data in a vast data lake) or in generating shader programs for massively parallel FPGA / GPU operations for AI.
In both cases, though, they need to operate on vast vectors, tables, and matrices of data. You mention that HVM avoids arrays. Is there some mechanism for efficiently packing and unpacking matrices or other densely formatted data? Would this be a case where HVM would defer to some "external" API for executing these "impure" array operations? Similar, maybe, to how Haskell shunted IO off to the side for years.
3
This reminds me of an (abandoned) attempt at a very parallelizable language called flowlang. It never quite got an MVP finished, but it had a different approach at the same problem.
2
I remember stumbling on this guy's stuff long ago. Pretty cool.
1
Unrolled version for people that aren't a fan of the Twitter format: https://threadreaderapp.com/thread/1588332432587005952.html
If that doesn't work for some reason, you can go to the base Thread Reader App site and plug in the Twitter link.
Hopefully, with the things going on with twitter rigth now, people move to a platform that actually is designed for longer form content.
I'm looking for a good place to blog that looks serious, is based on markdown, is lightweight and doesn't take much effort to maintain. I have a profound hatred for Medium. Not only the editor is terrible (I want to use VIM, not a shitty UI), but the business model where they paywall my own article is creepy as hell.
I recommend you buy a domain, then use a static site generator + GitHub Actions to regenerate and deploy your site on git push. You own your content (it's in a Git repo) and if you stop liking GitHub you own the domain too so you can migrate hosting companies
Paywall is opt-in. You can have as many free articles as you like, open to everyone.
They used to have annoying popups but even those are completely gone now.
Lack of markdown support is admittedly a drawback.
Does it need to be a third party? Personally, I'd just use a static site generator and host it on github pages. You can still use something like twitter/reddit/whatever to share a link to the blog for discoverability.
If you really want rust to generate the site, look into https://github.com/getzola/zola which is markdown based and would work perfectly well for this use case.
Speaking as a person who has written several well read Twitter threads and exactly one article, whose mental norms are extremely adjusted away from being able to regularly write long form content, I really hope that another microblogging platform emerges.