I took a different approach with this JavaCard VM I've been working on, first I had Claude implement the VM from the spec and then I had it implement a proof generator (also from the spec) so an identical bug would have to exist in both of them to make it through. Worked pretty well, the JCVM and bytecode verifier are both statically verified using ESBMC (which found a few bugs in that project so, win, win).
Now I have it working on a verifier for the bytecode transformations the optimizer uses, also using the static verification approach, to discover them all and ensure they are all valid. This one is seeming to be on track to making it fast enough to work on a real grammar as opposed to the 'academic grammars' the literature typically uses to prove the lemmas. Claude seems to be fighting this and has been working on the same refactor for over a week now so, we'll see...
Yeah, the more ambitious I get the more Claude doesn't follow the plan and just makes up random stuff to get the tests to pass instead of following the design...
> Which makes me wonder: what’s the appeal of PEGs or parser generators now?
I just had the robots write a PEG parser generator...
Which can do analysis on the grammars which, I suspect, a hand (or LLM) written one can't do so you don't end up chasing infinite recursion, dead rules and whatnot. It also got shoehorned into the regex engine (https://arxiv.org/abs/1210.4992) for my toy Java 1.0 compiler to loop back to TFA.
For my APL interpreter they had to do the 'handwritten' parser (a Pratt parser a sibling comment brings up) as you need to combine parsing and evaluation since there's no way for the parser to tell what it's looking at because APL syntax is just weird.
I'd like to see the UCLA study which showed that in states that legalized marijuana, bankruptcies and credit card delinquencies increased about 25%.
Admittedly, I didn't read the whole article but I didn't see anything about banning social media and/or putting pot stores on every corner to compete with the liquor/tobacco stores. Seems like something they would have put in the beginning to draw the reader in, dunno?
What I do know from living on this planet for over half a century is that gambling and alcohol and certain drugs are very addictive and have the tendency of ruining people's lives. Pretty much common knowledge at this point, one would have thought...
The problem I've been having is the LLM's are super dodgy, not even ten minutes ago the 'solution' to a proof failing was to disable that check in the static analysis harness so the tests pass since their first try (with a counter example and lemma from the literature in hand) didn't fix the issue.
Maybe it's an issue because it controls both sides of the fence and can change things willy-nilly when it thinks I'm just watching the youtubes but I haven't been able to find a another way to do this so, here we are...
I've been poking at a C version of this (https://github.com/dan-eicher/javelina) which would be interesting to benchmark against as it does a similar tail-calling dispatch mechanism. Plus copy-and-patch JIT but that probably only works on x86-64 as that's the only place I've ever tested it. The main differences from a brief skim of TFA is mine doesn't have any fallback (so non-tail calls will blow up the C stack) and the function calls always go through the trampoline so the VM doesn't have to care if it's calling JIT or interpreted code which, I'm assuming, your function pointer embedding thing is designed to optimize away.
And the JavaCard firewall algorithm would be an interesting non-spec addition to a wasm VM which is running code you really, really don't want to escape the sandbox. Something to look into for inspiration on the subject, perhaps? Not sure if there's any sort of proposal for sandboxing these things as I just took the spec file and implemented it using the dodgy weasels where it was mainly to see how far they've come with no real plan to use it for anything so kept it strictly to what the spec said a wasm interpreter needs to do.
Anyhoo, didn't really realize there were so many different projects doing the same thing, kind of interesting, actually...
If you think that your Wasm interpreter is stable and kinda production ready enough, you might want to file a PR to the wasmi-benchmarks repo to add support for your Wasm runtime.
Would certainly be another great addition to have it.
This would allow comparing your engine to all the others.
>> I was curious why you swapped over to a register based VM
Not the OP but there are real performance benefits, I've been poking at a wasm VM and it has two jit backends where one is pure copy-and-patch while the other caches the locals in registers using the function args + copy-and-patch and there is a significant performance gain just from that alone. A push/pop from a stack is fairly expensive while the register caching keeps things in the CPU's happy place. The smallest gain was ~2x over the interpreter on memory bound tasks while the largest was ~20x on math heave kernels. Admittedly, the interpreter isn't the fastest thing ever as its one and only goal is conformance with the spec to use for differential testing but the difference between the the two jit levels are somewhere in the neighborhood of 1.5-5x depending what the code is up to.
The three biggest performance gains, from the random benchmarks, are quality of the bytecode out of the compiler, the jit itself and register caching from what I can tell from the fancy chart I had Claude make and a good squint. Tail-calling would be somewhere on that list too but I can't measure that as all the opcode do the tail-calls between each other as that's just how it was all put together, the code the interpreter runs is the same code the copy-and-patch jit stitches together as they are both generated from the same DSL. Which is also the biggest cost with the register caching as the code template file grew from tens of kilobytes for the 407(?) wasm opcodes to ~3MB for all the specialized ones to pass the locals in eight args but that's really just a binary size thing, the stitched together functions just pick and chose the ones they need.
Long winded way to say CPUs like when you keep things in registers, I suppose...
I thought this was just a thing until I moved from Cal to Arizona and people would get really mad about it until I asked someone at work and learned it's illegal.
My first motorcycle was fast enough to get out of the way of stupid drivers (and be fun) while my last one was so fast it still amazes me to this day that I'm still alive. Apparently it was amateur raced with all the things that entails, which is probably why I didn't die as it was so obnoxiously loud people knew there was a motorcycle around them so I couldn't really hide in their blind spots, not that I would ever do that because that's a quick way to get a free ride to the ER.
$2500 for a vehicle which could most likely top out around 200 mph probably wasn't the smartest purchasing decision I've ever made. The only smart thing I ever did was there was always something suitably wrong with it I never took it out into the desert to see what the real top speed was.
My Fiat 500 has the same size engine and keeps me out of trouble. And around the same MPG...
Yeah, that only works if they follow the plan (they don't), actually write the tests first (they don't) and don't silently defer anything which doesn't have a test written as "speculative without a use case".
Or just write tests to match the buggy code after you call them out for not writing tests.
I mean, the struggle is real...
No matter how weasel-proof you make the plans they are much better weasels and just do as little as possible and "the test not written is the test which never fails." There's a certain amount of zen to them.
Now I have it working on a verifier for the bytecode transformations the optimizer uses, also using the static verification approach, to discover them all and ensure they are all valid. This one is seeming to be on track to making it fast enough to work on a real grammar as opposed to the 'academic grammars' the literature typically uses to prove the lemmas. Claude seems to be fighting this and has been working on the same refactor for over a week now so, we'll see...