On Tue, Feb 26, 2002 at 11:15:59AM -0800, Hong Zhang wrote: > > >The KVM of Java includes pre-verify info, which serves similar purpose. > The > > >reason behind is Java bytecode verification is (kind of) NP-complete. By > > >using pre-verify info, the problem can be reduced to linear in most case. > (No one > > >prove it mathmatically, but you got the idea.) > > > > Hmmm. Can you trust it? Seems like it wouldn't help drop the time, > > since you'd need to verify the pre-verify info, though I suppose > > verifying the information might be faster than constructing it from > > the bytecode. > > No, I don't trust it. But I can easily verify it. It is just like public key > algorithm. Factoring a real big number is a pain, but verify whether the > (a * b) == c is piece of cake. > > I don't search for the answer , I just verify your answer.
The best description of this that I found when I was digging into it long ago was stuff on "Proof-Carrying Code" from CMU. The analogy is to a complex proof: if someone has written out a proof, then even if you don't trust their proof, it's a lot easier to verify it than to come up with your own. It kind of falls out naturally from the definition of the set NP. NP is the set of problems that have easily verifiable answers. (More formally, verifiable in polynomial time.) NP-complete is sort of the difficult subset of NP, but NP-complete problems are still in NP, so they have to be verifiable in polynomial time. And that description is a good example of how theory can take a question, generalize it, and come up with an answer that is provably correct, can be completely depended upon, and is pretty much worthless for anything practical. :-) Unless we're verifying more than jumps never landing between opcodes or outside of the code segment, it seems to me that we'd still have to linearly scan through the whole code segment to verify the pre-verify info. I assume it would just list the addresses that contain jumps, but you'd still need to check the implicit assertion that no other jumps exist. In order for pre-verify info to be useful, we need to have a superlinear check to optimize.
