JavaLobby and JavaOS
dlambright at opengroup.org
Mon Oct 13 10:42:49 PDT 1997
In message <199710131117.HAA03790 at radish.research.att.com>Vijay Saraswat writes
> X-Authentication-Warning: vega.soi.city.ac.uk: lp set sender to owner-kaffe
>@soi.city.ac.uk using -f
>I agree with Sean here. The notion of a strongly-typed,
>dynamically linked language, like Java, makes some fresh
>To go a step beyond what Sean is saying: in fact it is possible
>(the "declarative bytecode verification" approach) to develop
>bytecode verifiers *systematically*, using a first-principles
>approach, from a constraint-based specification of the opcodes
>involved. One can translate an input byte code program, P,
>compositionally (byte-code for byte-code) into a constraint
>program, T(P) which "obviously" states the constraints on the
>run-time type-state of the Java Virtual Machine, which must hold
>for program execution to be type-safe. T(P) is "loop-free" and
>will take time proportional to its length, which is proportional
>to the length of P, to execute. If T(P) does not deadlock or
>produce "false", P is type-safe.
This aproach is taken by Penn State's active network's program for the PLAN
language (which has its roots in ML). I have not seen it applied to Java by
anyone. My group is considering it. A question I have concerns the expressive
power a "loop free" language has to the developer. What can and cannot be
described under such constraints? I would also be interested in what tradeoffs
work well between load-time/verification time and expressability. How large
can a classfile be?
>This approach differs slightly from the one that Sean and
>Javasoft have implemented. In their cases, there are separate
>*byte code verifiers*, usually largish (10-15 page) C programs,
>implementing a "data-flow" analysis, documented by 10-15 pages of
>informal English (I have not seen Sean's documentation yet),
>about whose correctness it is hard to say anything formal.
I have not seen a formal desription of Java's bytecode verifier. I have
emailed Sun and Princeton's SIP group- no reply.. anyone heard of efferts
along these lines?
>In any case, the bottom line for this list should be, I think,
>that one can assume that the subproblem of verifying the
>type-safety of JVM-like bytecode is solved, with of course, one
>important caveat: native code. (A lot of the "core" classes in
>Java in fact contain natively implemented methods, and one has to
>use separate techniques for verifying them.)
Dont download native code unless it is authenticated from someone you trust :-)
Software fault isolation is another avenue to investigate.
>I would not be too surprised if this approach (Java's approach)
>of doing "link-time" (i.e. first-instruction-execution-time)
>type-checking actually resulted in significant performance
>*improvements* over standard OS's. One thing to keep in mind is
>that Java's architecture is such that the bytecode verifier can
>in fact accept some input code *even if it is not type-safe in
>isolation* --- as long as it is type-safe when combined with the
>other classes that are already loaded. That is, there are some
>possibilities of doing inter-classfile optimizations (e.g.
>eliminating some classcasts generated by the compiler) in a
>typesafe way, that can produce even more performance benefits
>than are posible if one does "straight" Java verification, as
>done currently by Sun's Java systems.
How big a win would this be?
More information about the kaffe