Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > linux.debian.maint.java > #8502 > unrolled thread

Packaging Java Pathfinder

Back to article view | Back to linux.debian.maint.java

Contents

  Packaging Java Pathfinder Marko Dimjašević <marko@dimjasevic.net> - 2015-10-23 06:10 +0200
    Re: Packaging Java Pathfinder Emmanuel Bourg <ebourg@apache.org> - 2015-10-23 10:10 +0200
      Re: Packaging Java Pathfinder Marko Dimjašević <marko@dimjasevic.net> - 2015-10-24 08:00 +0200
        Re: Packaging Java Pathfinder Emmanuel Bourg <ebourg@apache.org> - 2015-10-24 15:00 +0200
          Re: Packaging Java Pathfinder tony mancill <tmancill@debian.org> - 2015-10-25 19:00 +0100
    Re: Packaging Java Pathfinder Marko Dimjašević <marko@dimjasevic.net> - 2015-11-15 07:40 +0100
      Re: Packaging Java Pathfinder Emmanuel Bourg <ebourg@apache.org> - 2015-11-15 09:20 +0100
        Re: Packaging Java Pathfinder tony mancill <tmancill@debian.org> - 2015-11-15 17:50 +0100
          Re: Packaging Java Pathfinder Marko Dimjašević <marko@dimjasevic.net> - 2015-11-15 19:40 +0100
            Re: Packaging Java Pathfinder tony mancill <tmancill@debian.org> - 2015-11-16 02:10 +0100
              Re: Packaging Java Pathfinder Marko Dimjašević <marko@dimjasevic.net> - 2015-11-16 05:00 +0100

#8502 — Packaging Java Pathfinder

[Multipart message — attachments visible in raw view] — view raw

Hi all,

Since earlier this year Java Pathfinder [1] (or JPF for short), an
implementation of JVM used for software verification, is free software
and available under the Apache 2.0 license.

I would like to package JPF and I have a basic question. Given that JPF
is a JVM implemented in Java, would it be OK to package JPF such that it
is compiled with GCJ? Otherwise running a Java program in a JVM
implemented in a JVM is a huge resource penalty.

[1] Java Pathfinder: http://babelfish.arc.nasa.gov/trac/jpf


-- 
Kind regards,
Marko Dimjašević
http://dimjasevic.net/marko

[toc] | [next] | [standalone]

#8504

Le 23/10/2015 05:53, Marko Dimjašević a écrit :

> I would like to package JPF and I have a basic question. Given that JPF
> is a JVM implemented in Java, would it be OK to package JPF such that it
> is compiled with GCJ? Otherwise running a Java program in a JVM
> implemented in a JVM is a huge resource penalty.

Hi Marko,

Is the performance that critical for a verification tool? The Hotspot
JIT is rather good nowadays, are you sure using GCJ will significantly
improve the performances? This looks a bit like premature optimization
to me, but feel free to experiment.

Emmanuel Bourg

[toc] | [prev] | [next] | [standalone]

#8506

[Multipart message — attachments visible in raw view] — view raw

On Fri, 2015-10-23 at 10:03 +0200, Emmanuel Bourg wrote:

> Is the performance that critical for a verification tool? The Hotspot
> JIT is rather good nowadays, are you sure using GCJ will significantly
> improve the performances? This looks a bit like premature optimization
> to me, but feel free to experiment.

Well, Java Pathfinder is a model checker, meaning it explores
all/as-many-as-possible execution paths in a program. Given that the
number of paths can easily grow out of hand, I believe every bit of
speed or memory consumption improvement counts, hence I suggested
compiling JPF to native code under the assumption this helps with the
performance.

I don't have numbers myself, but if and when I learn how to package JPF
both as a gcj-package and as a regular Java program, I can do some
benchmarking.

According to the Debian policy for Java [1], "[p]ackages must not ship
gcj-code without the permission of the Java team
(<debian-java@lists.debian.org>)." What would it take to get the
permission from the team to have JPF packaged as a gcj-package?

I have no experience with packaging Java, but I do have experience with
creating a package with Debhelper for a C++ tool. Any pointers to
examples for gcj-packaging JPF would be greatly appreciated.


Cheers,
Marko


[1] https://www.debian.org/doc/packaging-manuals/java-policy/x155.html

[toc] | [prev] | [next] | [standalone]

#8507

Le 24/10/2015 07:50, Marko Dimjašević a écrit :

> According to the Debian policy for Java [1], "[p]ackages must not ship
> gcj-code without the permission of the Java team
> (<debian-java@lists.debian.org>)." What would it take to get the
> permission from the team to have JPF packaged as a gcj-package?

I can't speak for the team, but I feel that if GCJ doesn't improve the
speed by more than 15-20% on amd64/i386 it's probably not worth the trouble.


> I have no experience with packaging Java, but I do have experience with
> creating a package with Debhelper for a C++ tool. Any pointers to
> examples for gcj-packaging JPF would be greatly appreciated.

Sorry I have never used GCJ for a new packages so I can't really help,
but I suggest looking at the few packages depending on gcj-native-helper
(ant, libitext-java and hsqldb1.8.0 for example).

Emmanuel Bourg

[toc] | [prev] | [next] | [standalone]

#8511

[Multipart message — attachments visible in raw view] — view raw

Hello Marko,

This looks like a cool project and a nice addition to Debian.

On 10/24/2015 05:56 AM, Emmanuel Bourg wrote:
> Le 24/10/2015 07:50, Marko Dimjašević a écrit :
> 
>> According to the Debian policy for Java [1], "[p]ackages must not ship
>> gcj-code without the permission of the Java team
>> (<debian-java@lists.debian.org>)." What would it take to get the
>> permission from the team to have JPF packaged as a gcj-package?
> 
> I can't speak for the team, but I feel that if GCJ doesn't improve the
> speed by more than 15-20% on amd64/i386 it's probably not worth the trouble.

I don't recall the specific reasoning behind requiring the permission of
the Java Team in order to ship a gcj-package, but I suspect it's either
because supporting the gij+Classpath runtimes was generally problematic
(when using gcj to compile to bytecode .class files), or because using
gcj to compile directly to native object code won't result in arch:all
packages.

I also agree with Emmanuel that it might be a lot of additional effort
to create a gcj-package that may not provide a lot of performance
benefit.  In fact, I can't imagine that creating an arch:all package
from gcj that are going to perform better than openjdk on the HotSpot
architectures (but that's just a guess on my part).  Compiling directly
to native object code may provide an interesting performance comparison.

>> I have no experience with packaging Java, but I do have experience with
>> creating a package with Debhelper for a C++ tool. Any pointers to
>> examples for gcj-packaging JPF would be greatly appreciated.
> 
> Sorry I have never used GCJ for a new packages so I can't really help,
> but I suggest looking at the few packages depending on gcj-native-helper
> (ant, libitext-java and hsqldb1.8.0 for example).

If there is a significant performance difference, you could ship both an
arch:all binary package that contains bytecode for execution by the JRE
and an arch:any binary package on architectures where the performance
difference matters.  Those binary packages would most likely conflict
with each other because they'd provide the same commands.  Still, users
would have the option of using the native object code version.

Cheers,
tony

[toc] | [prev] | [next] | [standalone]

#8552

[Multipart message — attachments visible in raw view] — view raw

Hi again,

On Thu, 2015-10-22 at 21:53 -0600, Marko Dimjašević wrote:
> Hi all,
> 
> Since earlier this year Java Pathfinder [1] (or JPF for short), an
> implementation of JVM used for software verification, is free software
> and available under the Apache 2.0 license.
> 
> I would like to package JPF and I have a basic question. Given that JPF
> is a JVM implemented in Java, would it be OK to package JPF such that it
> is compiled with GCJ? Otherwise running a Java program in a JVM
> implemented in a JVM is a huge resource penalty.
> 
> [1] Java Pathfinder: http://babelfish.arc.nasa.gov/trac/jpf

Ok, for now I'm giving up on GCJ'ing it as I don't know how to do even
more basic things.

Can someone point me to a package that depends on Java 8? JPF needs
Java 8 to build and I can't figure out how to specify that given that
'default-java' points to Java 8. So I'd like to learn from an example.


-- 
Regards,
Marko
http://dimjasevic.net/marko

[toc] | [prev] | [next] | [standalone]

#8553

Le 15/11/2015 07:38, Marko Dimjašević a écrit :

> Can someone point me to a package that depends on Java 8? JPF needs
> Java 8 to build and I can't figure out how to specify that given that
> 'default-java' points to Java 8. So I'd like to learn from an example.

Hi Marko,

You can get a look at the openjfx package. JAVA_HOME is set this way in
debian/rules:

  DEB_HOST_ARCH ?= $(shell dpkg-architecture -qDEB_HOST_ARCH)
  JAVA_HOME     := /usr/lib/jvm/java-8-openjdk-$(DEB_HOST_ARCH)

Emmanuel Bourg

[toc] | [prev] | [next] | [standalone]

#8554

[Multipart message — attachments visible in raw view] — view raw

On 11/15/2015 12:15 AM, Emmanuel Bourg wrote:
> Le 15/11/2015 07:38, Marko Dimjašević a écrit :
> 
>> Can someone point me to a package that depends on Java 8? JPF needs
>> Java 8 to build and I can't figure out how to specify that given that
>> 'default-java' points to Java 8. So I'd like to learn from an example.
> 
> You can get a look at the openjfx package. JAVA_HOME is set this way in
> debian/rules:
> 
>   DEB_HOST_ARCH ?= $(shell dpkg-architecture -qDEB_HOST_ARCH)
>   JAVA_HOME     := /usr/lib/jvm/java-8-openjdk-$(DEB_HOST_ARCH)

When using this recipe, you should also declare a build-dependency on
either "openjdk-8-jdk" or "default-jdk (>= 2:1.8)".  The first is (just
a tad) more explicit and aligns with the setting of JAVA_HOME.

Cheers,
tony

[toc] | [prev] | [next] | [standalone]

#8555

[Multipart message — attachments visible in raw view] — view raw

On Sun, 2015-11-15 at 08:46 -0800, tony mancill wrote:

> When using this recipe, you should also declare a build-dependency on
> either "openjdk-8-jdk" or "default-jdk (>= 2:1.8)".  The first is (just
> a tad) more explicit and aligns with the setting of JAVA_HOME.

Thank you for this!

I have another question...

So far a user would manually install Java PathFinder, so they would have
to configure it by editing a file ~/.jpf/site.properties, where Java
PathFinder modules (and I intend to package one module later too) would
figure out where on the disk is the main module, that is Java PathFinder
itself. However, now there will be Debian packages for Java PathFinder
and its modules, so the configuration file won't be needed as everything
will be in /usr/share/java, yet my hunch is the modules will still look
for ~/.jpf/site.properties.

Do you have any suggestions on how to handle this? My hunch is I will
have to patch things such that all modules always look for the main
module (and possibly other modules) in a specific place
(i.e. /usr/share/java).


-- 
Regards,
Marko
http://dimjasevic.net/marko

[toc] | [prev] | [next] | [standalone]

#8556

[Multipart message — attachments visible in raw view] — view raw

On 11/15/2015 10:39 AM, Marko Dimjašević wrote:
> On Sun, 2015-11-15 at 08:46 -0800, tony mancill wrote:
> 
>> When using this recipe, you should also declare a build-dependency on
>> either "openjdk-8-jdk" or "default-jdk (>= 2:1.8)".  The first is (just
>> a tad) more explicit and aligns with the setting of JAVA_HOME.
> 
> Thank you for this!
> 
> I have another question...
> 
> So far a user would manually install Java PathFinder, so they would have
> to configure it by editing a file ~/.jpf/site.properties, where Java
> PathFinder modules (and I intend to package one module later too) would
> figure out where on the disk is the main module, that is Java PathFinder
> itself. However, now there will be Debian packages for Java PathFinder
> and its modules, so the configuration file won't be needed as everything
> will be in /usr/share/java, yet my hunch is the modules will still look
> for ~/.jpf/site.properties.
> 
> Do you have any suggestions on how to handle this? My hunch is I will
> have to patch things such that all modules always look for the main
> module (and possibly other modules) in a specific place
> (i.e. /usr/share/java).

I agree that a patch would be the cleanest approach.  Perhaps you could
get away with simply a wrapper script that sets some system properties?
 (I haven't looked at JPF very closely yet.)

You should also consider whether a JPF user might want to use both the
modules provided by Debian and search for modules configured in the
site.properties file.  The question there will be the search order.

In general, anything you can do to ensure that the package works "out of
the box" without manual user configuration (but while still supporting
local configuration if desired) is the preferred approach.

Cheers,
tony

[toc] | [prev] | [next] | [standalone]

#8557

[Multipart message — attachments visible in raw view] — view raw

Hi all,

On Sun, 2015-11-15 at 16:59 -0800, tony mancill wrote:

> I agree that a patch would be the cleanest approach.  Perhaps you could
> get away with simply a wrapper script that sets some system properties?
>  (I haven't looked at JPF very closely yet.)

Keep in mind I'm not a proper Java developer, so I might be missing
quite a few things.

Java Pathfinder as a JVM defines quite a few properties (e.g., a
scheduling choice generator class), including some that are software
verification-specific. By default, these are specified in jpf.properties
in the code base root directory.

The main JAR file is expecting this info to be in one of search paths in
the increasing order of importance: 1) Java classpath (where it should
be in a file jpf.properties), 2) ~/.jpf/site.properties, 3)
jpf.properties in the current directory.

I see how this is done in JPF and I can either put the /usr/share/java
directory to the classpath and put jpf.properties to
/usr/share/java/jpf.properties, or I can easily patch Java Pathfinder
such that it searches for jpf.properties somewhere else, e.g. in
/etc/jpf/.

What do you suggest to do? My hunch is it shouldn't
be /usr/share/java/jpf.properties as there are only JAR files
in /usr/share/java. Also, it shouldn't be ~/.jpf/site.properties as that
is user-specific.


> You should also consider whether a JPF user might want to use both the
> modules provided by Debian and search for modules configured in the
> site.properties file.  The question there will be the search order.

Ok, I'll keep this in mind. For the time being I want to get it working
for a single system-wide installation.


> In general, anything you can do to ensure that the package works "out of
> the box" without manual user configuration (but while still supporting
> local configuration if desired) is the preferred approach.

Thanks for explaining this!


-- 
Regards,
Marko
http://dimjasevic.net/marko

[toc] | [prev] | [standalone]

Back to top | Article view | linux.debian.maint.java

csiph-web