Comment by repolfx | Hacker News Reader

Comment by repolfx | Hacker News Reader

Parent Full thread

Neither the JVM or the CLR provide such a sandbox for code that uses pointers. LLVM IR is not portable, is not sandboxed and is always in flux.

Actually, the CLR supports pointers and the JVM can run arbitrary LLVM bitcode (so C, C++, Rust etc) in a memory safe way with bounds checking and garbage collection these days. Check out Sulong and Safe Sulong:

http://ssw.jku.at/General/Staff/ManuelRigger/ASPLOS18.pdf

JVMs can also manually allocate memory using the Unsafe class, I suppose if you wanted WASM like protection semantics that API could be constrained to a particular memory region and become "SortaUnsafe" for example. You could then compile C to such a dialect. The LLVM bitcode on Graal approach is likely to work better though,.

However, realistically most new software is not being written in C or even C++ for that matter. Most developers use managed languages. And the JVM can do a much better job of that than WASM can.

A flaw is a feature that cannot be supported, even in principle.

This is a fascinating definition of flaw that I haven't previously encountered.

In what sense does the JVM not do "full verification at runtime"? Also if you have some more material on which bits of the JVM bytecode set aren't formally verified I'd like to read that. I can imagine, that the latest features may not have been done, but the older JVM bytecode sets were formally verified at least.

> Actually, the CLR supports pointers

I said it doesn't provide a sandbox for pointers. CLR pointers can corrupt your whole VM instance. WASM's lightweight bytecode with no runtime can support in-process heap isolation.

> JVM can run arbitrary LLVM bitcode (so C, C++, Rust etc) in a memory safe way with bounds checking and garbage collection these days. Check out Sulong and Safe Sulong:

Nice find. Still, look to be interpreted though.

> In what sense does the JVM not do "full verification at runtime"?

The last report of a formalized semantics for verification that I saw was over 10 years old:

https://repositories.lib.utexas.edu/handle/2152/2763

The JVM bytecode has significant verification challenges as discussed in this paper and by Leroy in the other papers I linked. The Joe-E papers I linked also discuss the problems of targeting the JVM at length.

As I linked in my other comment, WASM was built with mechanized proofs nearly from the outset. They learned from the mistakes made in the CLR and JVM.

Nice find. Still, look to be interpreted though.

It gets JIT compiled to native code that runs (for some code shapes yadda yadda usual story) about 10% slower than gcc, if I recall correctly. Without the safety aspect it can run as fast as GCC for some benchmarks.

As I linked in my other comment, WASM was built with mechanized proofs nearly from the outset. They learned from the mistakes made in the CLR and JVM.

But so did the CLR and JVM designers.

The paper you link to says the hard part of JVM bytecode verification is the jsr "subroutine" control flow instruction. This instruction has been phased out, bytecode version 51+ doesn't allow it anymore. Whilst a JVM may well support verification of older bytecode formats, and that verification is still safe and sound, you can implement the latest version of the spec and avoid that entire design error.

Given that, and given that the JVM type system has been proven sound despite being significantly more powerful than WASM's, I'm not really certain how this is meant to prove that WASM is better.

> But so did the CLR and JVM designers.

No they weren't. Formalization and verification of the IR came much later in both cases.

> Given that, and given that the JVM type system has been proven sound despite being significantly more powerful than WASM's, I'm not really certain how this is meant to prove that WASM is better.

"Significantly more powerful" is way overstating the case. In fact, I'd hazard that it's flat out wrong. You can easily express some patterns in JVM bytecode, but other patterns not at all.

Secondly, WASM's primitives types are much more flexible than those available on the JVM. For instance, unsigned types.

Finally, the JVM carries a lot of baggage, a) in terms of backwards compatibility as you briefly mention, b) in terms of unnecessary control flow instructions which unnecessarily complicate verification (like exceptions), c) unconfigurable runtime that's poorly suited to some programs, d) an overly complicated security model that's an impediment more than a help, etc. I could probably come up with a dozen more reasons, but that's just off the top of my head.

> Actually, the CLR supports pointers and the JVM can run arbitrary LLVM bitcode (so C, C++, Rust etc) in a memory safe way with bounds checking and garbage collection these days. Check out Sulong and Safe Sulong:

AFAIK there is no Java-Bytecode involved for this and to optimize the AST-interpreter to something faster you need the Graal-Compiler, most JVMs can't do this. There is no C++/LLVM/Rust to Java-Bytecode compiler that is widely used, while this exists for WASM. Even a huge Codebase like AutoCAD was compiled for the Web. Java-Bytecode wasn't designed for this, you could theoretically do the same with Java-Bytecode but it would probably be much slower. Simply because Java-Bytecode wasn't designed for this purpose.

Java-Bytecode is notoriously hard to verify, WASM is more strict and therefore verification is easier. (With verification I mean the process in the Browser/JVM that checks if the bytecode is actually valid). WASM only allows structured control flow, no arbitrary gotos like Java. This makes the compilers job much easier, many JVMs actually just bail out on irreducible loops and therefore such code might not get optimized. OTOH WASM-Bytecode wasn't designed for interpretation.

I don't know why there is this heated discussion. WASM had the chance to learn from the mistakes in Java's Bytecode and both bytecodes were designed for different purposes after all. Java Bytecode was designed for Java, WASM for being a language-agnostic compilation target. Supporting GC in Java-Bytecode for example is much easier than having a similar thing in WASM.

Reply on news.ycombinator.com