dominique-unruh / scala-isabelle

A Scala library for controlling/interacting with Isabelle
https://dominique-unruh.github.io/scala-isabelle
MIT License
37 stars 7 forks source link

Isabelle process not destroyed #3

Closed dominique-unruh closed 3 years ago

dominique-unruh commented 3 years ago

Albert Jiang reports:

I recently found that there might be a potential bug with scala-isabelle. Although I cannot be sure whether it was a bug or that my execution was faulty.

In the following is a very simple script that initialises an isabelle process and then destroys it.

package pisa.server

import _root_.java.nio.file.Path
import de.unruh.isabelle.control.Isabelle

object TestIsa {
  val setup: Isabelle.Setup = Isabelle.Setup(isabelleHome = Path.of("/Applications/Isabelle2020.app/Isabelle"),
    sessionRoots = Nil,
    userDir = None,
    logic = "HOL",
    workingDirectory = Path.of("./"),
    build=false
  )

  implicit val isabelle: Isabelle = new Isabelle(setup)

  println("Initialised isabelle")
  def main(args: Array[String]): Unit = {
    Thread.sleep(10000)
    isabelle.destroy()
    println("Destroyed isabelle")
    Thread.sleep(100000)
  }
}

However, if you execute the code, you will find that there is a poly process that can be caught by the activity manager to use ~400MB of memory and persists even after isabelle is destroyed or even the scala application terminates. I have to kill the process manually.

I wonder if you think this is a bug? Or is there something I didn't do properly to cause the memory issue?

dominique-unruh commented 3 years ago

I can confirm the problem on Linux.

dominique-unruh commented 3 years ago

First analysis: The Isabelle process started by Java is the root of the following process tree:

bash(471405)───java(471421)─┬─bash_process(471474)───poly(471475)─┬─{poly}(471478)
                            │                                     ├─{poly}(471479)
                            │                                     ├─{poly}(471480)
                            │                                     ├─{poly}(471481)
                            │                                     ├─{poly}(471482)
                            │                                     ├─{poly}(471483)
                            │                                     ├─{poly}(471484)
                            │                                     ├─{poly}(471485)
                            │                                     ├─{poly}(471486)
                            │                                     └─{poly}(471487)
                            ├─{java}(471422)
                            ├─{java}(471423)
                            ├─{java}(471424)
                            ├─{java}(471425)
                            ├─{java}(471426)
                            ├─{java}(471427)
                            ├─{java}(471428)
                            ├─{java}(471429)
                            ├─{java}(471430)
                            ├─{java}(471431)
                            ├─{java}(471432)
                            ├─{java}(471433)
                            ├─{java}(471434)
                            ├─{java}(471435)
                            ├─{java}(471436)
                            ├─{java}(471437)
                            ├─{java}(471448)
                            ├─{java}(471454)
                            ├─{java}(471455)
                            ├─{java}(471456)
                            ├─{java}(471457)
                            ├─{java}(471458)
                            ├─{java}(471459)
                            ├─{java}(471460)
                            ├─{java}(471468)
                            ├─{java}(471476)
                            └─{java}(471477)

Running process.destroy() in Java kills (successfully) the bash process that is the root of this tree. However, the java process invoked by that bash is not destroyed. (But it is destroyed when the Scala process ends. Why is that?)

dominique-unruh commented 3 years ago

Further observations: Sending SIGINT to the bash process kills the whole tree, but Java sends SIGTERM (or SIGKILL?) which does not work. One possibility would be to send a SIGINT via a shell command (kill -INT <pid>) on Linux/Mac (ignoring any errors of that command), and then some seconds later do process.destroy().

However, the fact that the Isabelle process also terminates when the Scala process terminates indicates that there is some other way. Theory: closing the named pipes between Scala and Isabelle makes Isabelle terminate. So maybe we have not closed those pipes.

Probably best strategy: Close all pipes (if this doesn't already happen) and do kill -INT <pid> and invoke process.destroy(). This would maximize the probability that it works on all OSs.

albertqjiang commented 3 years ago

Hi Dominique, did the new commit work for you?

After switching to the development version hooked to the git master branch, I did some further testing.

Under testing I found that for me, both on MacOS and Linux, the poly processes are not killed after running isabelle.destroy() with the same test file above.

@dominique-unruh

dominique-unruh commented 3 years ago

@albertqjiang I assume you used

libraryDependencies += "de.unruh" %% "scala-isabelle" % "master-SNAPSHOT"  // development snapshot

to use the snapshot? Unfortunately, that snapshot is not automatically updated to the git master, I need to manually publish. (Done now.)

Note that sbt might not automatically notice that the snapshot was updated. You can check which revision you have using the file /de/unruh/isabelle/gitrevision.txt inside the scala-isabelle jar. I don't know a command line way to force sbt to re-check for a new version. The only reliable way I found is to delete the file scala-isabelle_*-master-SNAPSHOT* that are somewhere in the sbt/maven/ivy cache on the disk.

I also added some additional code to make sure the process is really killed. (I found some Java API to find child processes.) 79c7311

albertqjiang commented 3 years ago

I see. Adding the line to the build.sbt is indeed what I did. Thank you for manually publishing this!

I can confirm now that the master snapshot does properly kill the process both on MacOS and on Linux, after deleting the cached files. Much appreciated!