Memory leaks in Silicon

[fpoli]

Calling Silicon::verify multiple times (sequentially) on the same verifier instance leaks memory, which is freed only when the verifier is destructed. In other words, there is some state that is not cleaned by Silicon's private reset method. In Prusti, this causes our prusti-server to go OOM after a while when verifying large programs, because we try to reuse the same verifier instance for multiple verification requests.

The memory leak can be debugged in VisualVM by inspecting the diff between heap dumps taken at different times after a manual GC run. To give an example, here is one of the paths from the verifier to one of the leaked viper.silicon.state.terms.Less instances:

this     - value: viper.silicon.state.terms.Less #1
 <- head     - class: scala.collection.immutable.$colon$colon, value: viper.silicon.state.terms.Less #1
  <- equalityDefiningMembers     - class: viper.silicon.state.terms.And, value: scala.collection.immutable.$colon$colon #3843
   <- body     - class: viper.silicon.state.terms.Let, value: viper.silicon.state.terms.And #1
    <- body     - class: viper.silicon.state.terms.Quantification, value: viper.silicon.state.terms.Let #1
     <- [0]     - class: java.lang.Object[], value: viper.silicon.state.terms.Quantification #1
      <- prefix1     - class: scala.collection.immutable.Vector1, value: java.lang.Object[] #6000
       <- postConditionAxioms     - class: viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$, value: scala.collection.immutable.Vector1 #16
        <- functionsSupporter$module     - class: viper.silicon.verifier.DefaultMasterVerifier, value: viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$ #1
         <- verifier (JNI local)     - class: viper.silicon.Silicon, value: viper.silicon.verifier.DefaultMasterVerifier #1

For this particular instance, it seems that postConditionAxioms in functionsSupporter keeps growing.

Another example, for a viper.silicon.state.terms.Trigger instance:

this     - value: viper.silicon.state.terms.Trigger #5
 <- head     - class: scala.collection.immutable.$colon$colon, value: viper.silicon.state.terms.Trigger #5
  <- triggers     - class: viper.silicon.state.terms.Quantification, value: scala.collection.immutable.$colon$colon #4167
   <- [1]     - class: java.lang.Object[], value: viper.silicon.state.terms.Quantification #5
    <- prefix1     - class: scala.collection.immutable.Vector1, value: java.lang.Object[] #5985
     <- emittedFunctionAxioms     - class: viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$, value: scala.collection.immutable.Vector1 #8
      <- head     - class: scala.collection.immutable.$colon$colon, value: viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$ #1
       <- next     - class: scala.collection.immutable.$colon$colon, value: scala.collection.immutable.$colon$colon #254
        <- next     - class: scala.collection.immutable.$colon$colon, value: scala.collection.immutable.$colon$colon #253
         <- next     - class: scala.collection.immutable.$colon$colon, value: scala.collection.immutable.$colon$colon #252
          <- next     - class: scala.collection.immutable.$colon$colon, value: scala.collection.immutable.$colon$colon #251
           <- next     - class: scala.collection.immutable.$colon$colon, value: scala.collection.immutable.$colon$colon #250
            <- next     - class: scala.collection.immutable.$colon$colon, value: scala.collection.immutable.$colon$colon #249
             <- next     - class: scala.collection.immutable.$colon$colon, value: scala.collection.immutable.$colon$colon #248
              <- symbolDeclarationOrder     - class: viper.silicon.verifier.DefaultMasterVerifier, value: scala.collection.immutable.$colon$colon #247
               <- verifier (JNI local)     - class: viper.silicon.Silicon, value: viper.silicon.verifier.DefaultMasterVerifier #1

I probably can find many more cases, if I keep looking at the heap dumps.

[fpoli]

Using a new verifier for each verification the memory leak almost disappears. There are still Z3ProverStdIO instances that cannot be garbage collected. After verifying programs for 20 minutes (the Prusti test suite takes 1 hour to run) there are about 10'000 of such instances and their retained size is 85 MB, which is 75% of the memory used by the JVM after a manual GC run, and it grows with time. @ArquintL I expect that the Viper server should be affected by this too.

The reason why Z3ProverStdIO instances cannot be garbage collected is probably this Runtime.getRuntime.addShutdownHook (explanation):

silicon/src/main/scala/decider/Z3ProverStdIO.scala

Lines 95 to 99 in ebd845c

	Runtime.getRuntime.addShutdownHook(new Thread {
	override def run(): Unit = {
	process.destroy()
	}
	})

We could converted that cleanup code to a stop method. I'll give it a try.

Path from a GC root to a Z3ProverStdIO instance:

this     - value: viper.silicon.decider.Z3ProverStdIO$$anon$1 #19
 <- [48]     - class: java.lang.Object[], value: viper.silicon.decider.Z3ProverStdIO$$anon$1 #19
  <- table     - class: java.util.IdentityHashMap, value: java.lang.Object[] #5224
   <- hooks (sticky class)     - class: java.lang.ApplicationShutdownHooks, value: java.util.IdentityHashMap #3

[Aurel300]

@fpoli Is this fixed with the merged PR?

[fpoli]

When using a new verifier for each verification requests, yes. However, the stop method of the API still has other kinds of memory leaks. I think there are two alternative ways to close this issue:

1. We declare (e.g. in the doc comment) that verifier instances are never meant to be reused, or "bad stuff" happens (e.g. memory leaks).
2. We fix the memory leaks and let frontends reuse verifier instances.

In practice, all frontends seem to assume (1).