Typechecking JVML
In Java 6 (Mustang) we will be
releasing a new version of the byte code verifier. For those of you living in blessed ignorance, the verifier is in essence a typechecker for machine language of the JVM, which I will refer to as JVML below.
So why are we doing this? To make verification faster, simpler and more adaptable. The existing verifier performs type inference (more precisely,
type reconstruction). In JVML, types are declared for fields, formal parameters of methods and method return types - but not for local variables or the
operand stack.
Hence, the verifier must infer the types of local variables and the operand stack based on how they are used. This is slow, memory intensive and very complicated.
The new scheme is rooted in research done by Eva Rose for her master's thesis a few years back.
The new verifier requires additional type declarations for local variables and the operand stack in JVML. As a consequence of this and other detailed changes,
it doesn't need to infer them, and is about twice as fast,
uses a fraction of the memory and is vastly simpler than the old
verifier.
So increased speed and reduced space are obviously good. Simplicity is also obviously good, but looking at the software industry, it's clear that it worships complexity. An appreciation of simplicity for its own sake is sorely lacking. Most people need very concrete examples before
they are willing to invest any effort for the sake of simplicity.
Here is one example of why this simplification might be useful. Let's imagine that at some point in time, it might be plausible (in terms of compatibility) to reify generics.
Among many other issues, this entails verification of generics.
It will be relatively straightforward to extend the new verifier to typecheck generics. Anyone who would seek to get the old verifier to do this is probably in need of clinical assistance.
In Mustang, javac will generate the necessary type information in the class files it produces. It won't generate code using jsr and ret either (nor will other tools Sun releases). Other vendors may need more time to catch up, which is why we will fall back to the old verifier for a while.
The spec for all this is being worked out as part of JSR202 where you can get a draft spec. You can also get more detail on practicalities in Wei Tao's article on the
typechecking verifier. Obviously, the verifier is critical to the security and integrity ofthe Java platform. Because of this, we'd like to get the community involved in banging on
both the spec and the implementation. If there are any holes, we want to find them
before the release.
To that end, Sun is asking for knowledgable people to have a go at
cracking the new verification scheme. If you find a hole in the spec, you'll get recognized at the JavaOne 2006 conference.
Honorable mention for finding holes in the implementation. Details should be available soon at the Crack the Verifier
Initiative web
page.
Posted at 06:00PM Oct 30, 2005 by gbracha in Java | Comments[62]