JavaLobby and JavaOS

[Dan Lambright]

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
>approaches possible. 
>
>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?