prismmodelchecker / prism

The main development version of the PRISM model checker.
http://www.prismmodelchecker.org/
GNU General Public License v2.0
154 stars 70 forks source link

Nailgun mode fails for Java 19 #221

Open davexparker opened 1 year ago

davexparker commented 1 year ago

Running PRISM in Nailgun server mode (-ng), which is the default for make tests, fails on Java 19:

Exception in thread "NGServer(null, 2113)" java.lang.UnsupportedOperationException: The Security Manager is deprecated and will be removed in a future release
    at java.base/java.lang.System.setSecurityManager(System.java:425)
    at com.martiansoftware.nailgun.NGServer.run(NGServer.java:396)
    at java.base/java.lang.Thread.run(Thread.java:1589)

This is because Nailgun uses Security Manager functionality, which is deprecated from version 19.

The preferred solution will be to upgrade Nailgun (lib/nailgun-server.jar and src/prism/ngprism.c (and src/prism/ng.c.orig)) to a newer version from https://github.com/facebook/nailgun. There is a patch, which is not yet merged.

In the meantime, a temporary fix is to pass -Djava.security.manager=allow to java, e.g., by adding this to bin/prism:

PRISM_JAVA_PARAMS=-Djava.security.manager=allow

But this cannot easily be added to the main version of PRISM because earlier JDKs (11 and earlier) do not support this option.

davexparker commented 8 months ago

Update: Modified versions of Nailgun that remove the Security Manager (e.g., the patch above) will not suffice, since there is then no way to catch Java exiting with an error (which means the Nailgun server closes if PRISM fails).

davexparker commented 8 months ago

There is a fix in b2642c1 that automatically applies the PRISM_JAVA_PARAMS=-Djava.security.manager=allow workaround within prism-auto if Java is newer than version 19. This at least allows regression testing (make tests) to complete with new releases of Java. But callingprism -nailgun directly does not work without a manual fix. And this will need resolving properly (likely finding a replacement for Nailgun) if the Security Manager is properly removed in a later version of Java.