Re: [rvm-research] Jikes RVM and Java Runtime library

On 3/3/2014 12:59 PM, Pascal Kesseli wrote:

> I’m a DPhil freshman at Oxford University and have joined the Software Verification group there.
> We’re trying to extend our bounded model checker CBMC by a Java frontend. Obviously there are a lot
> of things to be considered before this can work, and one of those would be how to model native
> operations in the Java Runtime library.
>
> An obvious choice would be to model them using JNI and the JDK source code. However, I was wondering
> whether the Jikes research VM could provide a different approach. Does Jikes feature Java
> implementations of all these operations? It said in the FAQ that uses GNU classpath, which seemed to
> be a clear no to me, but I wanted to shout out this post just to get feedback from you guys as well.

All JVMs ultimately must make system calls, etc., so if you want to model
the overall effect, you will drag in a substantial piece of OS semantics.

One advantage Jikes RVM may have is that some parts are expressed in terms
of so-called "VM magics". These look like Java methods (and have Java stubs
that might lead you to *think* that they are implemented in Java), but are
implemented by the compilers.  So these are not, strictly speaking, natives,
but more appropriately thought of as *intrinsics*, similar to the way in
which Fortran (say) includes a raft of mathematical functions and conversions
as intrinsics.  However, magics can also do some kinds of things that are
unsafe and similar in effect and intent to some of the methods of Oracle's
Unsafe class, which is implemented mostly by natives.

In your position I would be tempted to write my own specifications for
natives and to prove the Java side assuming those specifications are
correct, and then consider doing what I could to prove the C/C++ side
that is suppose to meet the specification.

Overall, you probably need to proceed using an appropriately chosen
and justified subset :-) ...

Regards -- Eliot Moss

------------------------------------------------------------------------------
Subversion Kills Productivity. Get off Subversion & Make the Move to Perforce.
With Perforce, you get hassle-free workflows. Merge that actually works. 
Faster operations. Version large binaries.  Built-in WAN optimization and the
freedom to use Git, Perforce or both. Make the move to Perforce.
http://pubads.g.doubleclick.net/gampad/clk?id=122218951&iu=/4140/ostg.clktrk