Out of memory error for property "Deserializing a serialized IR produces an equivalent IR"

[shonfeder]

A unit test failed in commit https://github.com/informalsystems/apalache/commit/9efb01fb85d9dda0f0730810b4e01e0e6b91fd11 during evaluation of a generate module:

 [info] - Deserializing a serialized IR produces an equivalent IR *** FAILED *** (26 minutes, 52 seconds)
[info]   OutOfMemoryError was thrown during property evaluation.
[info]     Message: Java heap space
[info]     Occurred when passed generated values (
[info]       arg0 = TlaModule(sfOdC) {
[info]   TlaOperDecl(y53io5fv,List(OperParam(i9gyw,0), OperParam(kXw8,0)),LET rV5oZ ≜ Nat IN BOOLEAN)
[info]   TlaAssumeDecl(y53io5fv(LET ycv ≜ FALSE eWeJ ≜ "yeI5r" IN y53io5fv, "nOmF" = (y53io5fv(y53io5fv([(♢-2147483648 .. ♢Int) → y53io5fv], "rAx3"), y53io5fv))))
[info]   TlaAssumeDecl(Nat)
[info]   TlaOperDecl(lX,List(),∀BOOLEAN ∈ Seq(ASSUME493131 ≤ 2135197868) ∈ (LET l ≜ ASSUME492229 y(k, g) ≜ Int IN y53io5fv < TRUE): ¬LET m ≜ y53io5fv iu(w, g) ≜ ASSUME492229 IN SUBSET BOOLEAN)
[info]   TlaConstDecl(g)
[info]   TlaAssumeDecl(ASSUME492229)
[info]   TlaAssumeDecl(LET d(u, iC, p) ≜ TRUE IN ASSUME493131())
[info]   TlaConstDecl(gV)
[info]   TlaOperDecl(b,List(),968044777)
[info]   }
[info]     )

(source in CI logs)

This is a non-deterministic failure, and the build is not broken ,but probably work investigating at some point to see if we hit an interesting edge case.

FYI @thpani and @Kukovec, who have both touched this test (not to say it's your responsibility or fix it, or even that it deserves the attention to fix atm ;) ).

[konnov]

Can it be related to #1906?

[shonfeder]

Iiuc, #1906 was merged in after the failure showed up on unstable?

[Kukovec]

I don't recall doing any work on those tests, so if I appear in git blame it's probably some renaming propagation. Also, as an unintended side-effect, the code in #1906 probably strictly better-performant.

[thpani]

There's ~90 lines of

[warn] In the last 10 seconds, 5.231 (56.2%) were spent in GC. [Heap: 0.02GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.

in the logs before that exception is thrown. So it could be that the actual bug is somewhere else and only lead to manifest in an OutOfMemoryError at this specific unit test.

[shonfeder]

We got another one at https://github.com/informalsystems/apalache/actions/runs/3297326043/jobs/5438010088#step:6:114 on commit https://github.com/informalsystems/apalache/pull/2244/commits/901be0195ad25d78fadbfea487f8b1d8a791f045

``` [info] done compiling [warn] In the last 10 seconds, 5.606 (56.1%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 7.697 (99.4%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 10 seconds, 9.963 (99.8%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 10 seconds, 12.098 (124.9%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 18.835 (244.6%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 8.09 (102.1%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 7.924 (101.6%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 18.934 (239.3%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 9 seconds, 10.217 (118.0%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 23.987 (306.6%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [info] - no duplicate definitions after incremental renaming *** FAILED *** (6 minutes, 2 seconds) [info] OutOfMemoryError was thrown during property evaluation. [info] Message: Java heap space [info] Occurred when passed generated values ( [info] [info] ) [info] - Deserializing a serialized IR produces an equivalent IR *** FAILED *** (5 minutes, 49 seconds) [info] OutOfMemoryError was thrown during property evaluation. [info] Message: Java heap space [info] Occurred when passed generated values ( [info] arg0 = TlaModule(k) { [info] TlaOperDecl(eJ8k,List(),LET r ≜ LET k(q, r, h) ≜ <2016095090>_"hj" IN k guERM ≜ UNCHANGED TRUE IN ♢r() * -LET c(g, ubt) ≜ Nat pOU(p) ≜ 0 IN pOU) [info] TlaAssumeDecl(LET mydDT(s, qUNR) ≜ eJ8k() IN mydDT) [info] TlaAssumeDecl(LET h6I(dL6py, n, u) ≜ LET c(m, c) ≜ Seq(ASSUME309178) b(o, fik, m) ≜ LET s(g) ≜ ASSUME309178 h(d, x) ≜ TRUE IN s IN b(Nat, eJ8k, c) IN "udKq") [info] TlaAssumeDecl(BOOLEAN ≤ (ASSUME310189 ∉ (ASSUME309178() ⇝ (BOOLEAN // Nat)))) [info] TlaAssumeDecl(LET p(j) ≜ "q" IN ASSUME310189() = LET hD(nD) ≜ BOOLEAN x(sG, i8) ≜ ASSUME310189 IN ASSUME310378) [info] TlaAssumeDecl(ASSUME310189) [info] TlaOperDecl(a,List(OperParam(r,0), OperParam(q,0)),"u") [info] TlaConstDecl(r) [info] } [info] ) [warn] In the last 9 seconds, 5.372 (66.3%) were spent in GC. [Heap: 0.02GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 9 seconds, 8.214 (97.8%) were spent in GC. [Heap: 0.01GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 9 seconds, 7.948 (98.8%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 9 seconds, 5.464 (67.0%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 7.859 (99.8%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 5.357 (67.1%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 9 seconds, 13.851 (164.2%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 5.001 (66.3%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 5.224 (66.7%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 5.051 (66.6%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 5.268 (66.4%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 5.152 (65.8%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 7.898 (99.8%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. [warn] In the last 8 seconds, 84.415 (1087.5%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. Exception: java.lang.OutOfMemoryError thrown from the UncaughtExceptionHandler in thread "classloader-cache-cleanup-0" [warn] In the last 11 seconds, 222.243 (2025.9%) were spent in GC. [Heap: 0.00GB free of 1.00GB, max 1.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance. Error: Exception in thread "pool-11-thread-6" java.lang.OutOfMemoryError: Java heap space Reporter completed abruptly with an exception after receiving event: TestFailed(Ordinal(0, 383),OutOfMemoryError was thrown during property evaluation. Message: Java heap space Occurred when passed generated values ( arg0 = <<{ ghAAg: Set(Real), osid: (Bool -> Int), uV: <>, z }, Set(Seq(b)), ({ eX: b, nky: V, h } -> b), b({ d }) | cy({ b: b, oA: Real, s }) | jw({ iKKc: Bool, pA: W, m }) | rlRCA({ c: (() => Real), s: [d: Bool], q }) | xj({ rAC: Str, z: b, j }) | v, { d: Seq(Bool), f: ((N -> b) -> Seq(b)), p: bdB({ s }) | jEOJ({ e }) | uL({ tt: Int, e }) | w, tRNh: (b -> Bool), v: c({ w }) | jmOE({ t }) | v, m }, f({ c: Set((| f: Set(j({ q: K, y }) | x6({ r }) | i) | r: (| u |) | y: (| f |) | j |)), nqH: ((Int) => b), u: <>, x8O5: <>, f }) | k({ a: b, y: Int, i }) | sQsXD({ nqlD: Int, q: Str, y }) | w({ eca: (() => Int), jMl: Set(Real), m: Seq(Int), oNHo: { qN: Bool, f }, j }) | yv({ cvf: <>, n: <>, nwq: (| s |), t: q({ f: Bool, t: b, a }) | wO({ a }) | zey({ j: Str, i }) | c, j }) | o>> ),TestDefaultType1Parser,at.forsyte.apalache.tla.typecheck.TestDefaultType1Parser,Some(at.forsyte.apalache.tla.typecheck.TestDefaultType1Parser),parse recursive types,parse recursive types,Vector(),Vector(),Some(org.scalatest.exceptions.GeneratorDrivenPropertyCheckFailedException: OutOfMemoryError was thrown during property evaluation. Message: Java heap space Occurred when passed generated values ( arg0 = <<{ ghAAg: Set(Real), osid: (Bool -> Int), uV: <>, z }, Set(Seq(b)), ({ eX: b, nky: V, h } -> b), b({ d }) | cy({ b: b, oA: Real, s }) | jw({ iKKc: Bool, pA: W, m }) | rlRCA({ c: (() => Real), s: [d: Bool], q }) | xj({ rAC: Str, z: b, j }) | v, { d: Seq(Bool), f: ((N -> b) -> Seq(b)), p: bdB({ s }) | jEOJ({ e }) | uL({ tt: Int, e }) | w, tRNh: (b -> Bool), v: c({ w }) | jmOE({ t }) | v, m }, f({ c: Set((| f: Set(j({ q: K, y }) | x6({ r }) | i) | r: (| u |) | y: (| f |) | j |)), nqH: ((Int) => b), u: <>, x8O5: <>, f }) | k({ a: b, y: Int, i }) | sQsXD({ nqlD: Int, q: Str, y }) | w({ eca: (() => Int), jMl: Set(Real), m: Seq(Int), oNHo: { qN: Bool, f }, j }) | yv({ cvf: <>, n: <>, nwq: (| s |), t: q({ f: Bool, t: b, a }) | wO({ a }) | zey({ j: Str, i }) | c, j }) | o>> )),Some(833318),Some(IndentedText(- parse recursive types,parse recursive types,0)),Some(SeeStackDepthException),Some(at.forsyte.apalache.tla.typecheck.TestDefaultType1Parser),None,pool-11-thread-4-ScalaTest-running-TestDefaultType1Parser,1666355593599). java.lang.InterruptedException at java.base/java.util.concurrent.locks.ReentrantLock$Sync.lockInterruptibly(ReentrantLock.java:159) at java.base/java.util.concurrent.locks.ReentrantLock.lockInterruptibly(ReentrantLock.java:372) at java.base/java.util.concurrent.LinkedBlockingQueue.put(LinkedBlockingQueue.java:332) at org.scalatest.LinkedBlockingQueue.put(JavaClassesWrappers.scala:43) at org.scalatest.DispatchReporter.apply(DispatchReporter.scala:300) at org.scalatest.tools.SuiteSortingReporter.handleTestEvents(SuiteSortingReporter.scala:161) at org.scalatest.tools.SuiteSortingReporter.doApply(SuiteSortingReporter.scala:80) at org.scalatest.CatchReporter.apply(CatchReporter.scala:36) at org.scalatest.CatchReporter.apply$(CatchReporter.scala:34) at org.scalatest.tools.SuiteSortingReporter.apply(SuiteSortingReporter.scala:26) at org.scalatest.tools.Framework$SbtReporter.apply(Framework.scala:1184) at org.scalatest.WrapperCatchReporter.doApply(CatchReporter.scala:70) at org.scalatest.CatchReporter.apply(CatchReporter.scala:36) at org.scalatest.CatchReporter.apply$(CatchReporter.scala:34) at org.scalatest.WrapperCatchReporter.apply(CatchReporter.scala:63) at org.scalatest.Suite$.reportTestFailed(Suite.scala:1635) at org.scalatest.SuperEngine.runTestImpl(Engine.scala:347) at org.scalatest.funsuite.AnyFunSuiteLike.runTest(AnyFunSuiteLike.scala:236) at org.scalatest.funsuite.AnyFunSuiteLike.runTest$(AnyFunSuiteLike.scala:218) at org.scalatest.funsuite.AnyFunSuite.runTest(AnyFunSuite.scala:1563) at org.scalatest.funsuite.AnyFunSuiteLike.$anonfun$runTests$1(AnyFunSuiteLike.scala:269) at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413) at scala.collection.immutable.List.foreach(List.scala:333) at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401) at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396) at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475) at org.scalatest.funsuite.AnyFunSuiteLike.runTests(AnyFunSuiteLike.scala:269) at org.scalatest.funsuite.AnyFunSuiteLike.runTests$(AnyFunSuiteLike.scala:268) at org.scalatest.funsuite.AnyFunSuite.runTests(AnyFunSuite.scala:1563) at org.scalatest.Suite.run(Suite.scala:1112) at org.scalatest.Suite.run$(Suite.scala:1094) at org.scalatest.funsuite.AnyFunSuite.org$scalatest$funsuite$AnyFunSuiteLike$$super$run(AnyFunSuite.scala:1563) at org.scalatest.funsuite.AnyFunSuiteLike.$anonfun$run$1(AnyFunSuiteLike.scala:273) at org.scalatest.SuperEngine.runImpl(Engine.scala:535) at org.scalatest.funsuite.AnyFunSuiteLike.run(AnyFunSuiteLike.scala:273) at org.scalatest.funsuite.AnyFunSuiteLike.run$(AnyFunSuiteLike.scala:272) at org.scalatest.funsuite.AnyFunSuite.run(AnyFunSuite.scala:1563) at org.scalatest.tools.Framework.org$scalatest$tools$Framework$$runSuite(Framework.scala:318) at org.scalatest.tools.Framework$ScalaTestTask.execute(Framework.scala:513) at sbt.TestRunner.runTest$1(TestFramework.scala:146) at sbt.TestRunner.run(TestFramework.scala:161) at sbt.TestFramework$$anon$3$$anonfun$$lessinit$greater$1.$anonfun$apply$1(TestFramework.scala:329) at sbt.TestFramework$.sbt$TestFramework$$withContextLoader(TestFramework.scala:289) at sbt.TestFramework$$anon$3$$anonfun$$lessinit$greater$1.apply(TestFramework.scala:329) at sbt.TestFramework$$anon$3$$anonfun$$lessinit$greater$1.apply(TestFramework.scala:329) at sbt.TestFunction.apply(TestFramework.scala:341) at sbt.Tests$.$anonfun$toTask$1(Tests.scala:435) at sbt.std.Transform$$anon$3.$anonfun$apply$2(Transform.scala:46) at sbt.std.Transform$$anon$4.work(Transform.scala:68) at sbt.Execute.$anonfun$submit$2(Execute.scala:282) at sbt.internal.util.ErrorHandling$.wideConvert(ErrorHandling.scala:23) at sbt.Execute.work(Execute.scala:291) at sbt.Execute.$anonfun$submit$1(Execute.scala:282) at sbt.ConcurrentRestrictions$$anon$4.$anonfun$submitValid$1(ConcurrentRestrictions.scala:265) at sbt.CompletionService$$anon$2.call(CompletionService.scala:64) at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264) at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:539) at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264) at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136) at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635) at java.base/java.lang.Thread.run(Thread.java:833) java.lang.OutOfMemoryError: Java heap space ```

[Kukovec]

It's weird, because the two failing tests are wildly different in what they test.

[thpani]

The Github macOS VMs have 14GB of RAM, we could start by increasing the heap size via -Xmx as the error message indicates.