OOM error

[aaronbembenek]

Hi there,

I tried running the attached program through Basil (commit 95d40e0), and it seems like Basil gets stuck in some sort of loop, eventually resulting in an out-of-memory error:

./mill run --input Problem01_label50_false-unreach-call/Problem01_label50_false-unreach-call.-O2.gts --relf Problem01_label50_false-unreach-call/Problem01_label50_false-unreach-call.-O2.relf --output Problem01_label50_false-unreach-call/Problem01_label50_false-unreach-call.-O2.bpl --simplify --dsa=  --dsa-split --dsa-checks --memory-transform --noif
WARNING: A restricted method in java.lang.System has been called
WARNING: java.lang.System::load has been called by mill.launcher.JLineNativeLoader in an unnamed module (file:/Users/abembenek/.cache/mill/download/1.0.3)
WARNING: Use --enable-native-access=ALL-UNNAMED to avoid a warning for callers in this module
WARNING: Restricted methods will be blocked in a future release unless native access is enabled

[279/279] run
[279] WARNING: A terminally deprecated method in sun.misc.Unsafe has been called
[279] WARNING: sun.misc.Unsafe::objectFieldOffset has been called by scala.runtime.LazyVals$ (file:/Users/abembenek/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala3-library_3/3.3.7/scala3-library_3-3.3.7.jar)
[279] WARNING: Please consider reporting this to the maintainers of class scala.runtime.LazyVals$
[279] WARNING: sun.misc.Unsafe::objectFieldOffset will be removed in a future release
[279] [INFO]   Basil
[279]          Version: 0.1.2-alpha-1097-g95d40e0e9
[279]          Commit:  95d40e0e9a3f3e2f60c64878379d678621c34714
[279] [INFO]   [!] Loading Program
[279] [INFO]   [!] Using ELF data from relf: Problem01_label50_false-unreach-call/Problem01_label50_false-unreach-call.-O2.relf
[279] [INFO]   [!] Removed all PC-related statements
[279] [INFO]   [!] Typecheck Passed
[279] [INFO]   [!] Removing external function calls
[279] [INFO]   [!] Removed unreachable blocks
[279] [INFO]   [!] Typecheck Passed
[279] [INFO]   [!] Running Simplify
[279] [INFO]   [!] Simplify :: DynamicSingleAssignment
[279] [INFO]   Copyprop Start
[279] [INFO]   Simplify:: Copyprop iteration 0
[279] [INFO]   [!] Simplify :: Expr/Copy-prop Transform
[279] [INFO]   [!] Simplify :: Dead variable elimination
[279] [INFO]   [!] Simplify :: Merge empty blocks
[279] [INFO]   Simplify:: Copyprop iteration 1
[279] [INFO]   [!] Simplify :: Expr/Copy-prop Transform
[279] [INFO]   [!] Simplify :: Dead variable elimination
[279] [INFO]   [!] Simplify :: Merge empty blocks
[279] [INFO]   Stopped at copyprop iteration bound: 2
[279] [INFO]   CopyProp 31622 ms
[279] [INFO]   [!] Simplify :: finished
[279] Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
[279]   at scala.collection.immutable.BitmapIndexedMapNode.copyAndSetValue(HashMap.scala:964)
[279]   at scala.collection.immutable.BitmapIndexedMapNode.updated(HashMap.scala:755)
[279]   at scala.collection.immutable.HashMap.updated(HashMap.scala:152)
[279]   at scala.collection.immutable.HashMap.updated(HashMap.scala:39)
[279]   at scala.collection.immutable.MapOps.updatedWith(Map.scala:121)
[279]   at scala.collection.immutable.MapOps.updatedWith$(Map.scala:115)
[279]   at scala.collection.immutable.HashMap.updatedWith(HashMap.scala:157)
[279]   at scala.collection.immutable.HashMap.updatedWith(HashMap.scala:39)
[279]   at analysis.data_structure_analysis.SymbolicValueAnalysis$package$.mapMerge$$anonfun$2(SymbolicValueAnalysis.scala:17)
[279]   at analysis.data_structure_analysis.SymbolicValueAnalysis$package$$$Lambda/0x000007ff0132d3c0.applyVoid(Unknown Source)
[279]   at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
[279]   at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
[279]   at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:619)
[279]   at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:617)
[279]   at scala.collection.AbstractIterable.foreach(Iterable.scala:935)
[279]   at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:905)
[279]   at analysis.data_structure_analysis.SymbolicValueAnalysis$package$.mapMerge(SymbolicValueAnalysis.scala:16)
[279]   at analysis.data_structure_analysis.SymValSetDomain.join(SymbolicValueAnalysis.scala:233)
[279]   at analysis.data_structure_analysis.SymValuesDomain.joinHelper$$anonfun$1(SymbolicValueAnalysis.scala:430)
[279]   at analysis.data_structure_analysis.SymValuesDomain$$Lambda/0x000007ff0132ca28.apply(Unknown Source)
[279]   at analysis.data_structure_analysis.SymbolicValueAnalysis$package$.mapMerge$$anonfun$2$$anonfun$1(SymbolicValueAnalysis.scala:19)
[279]   at analysis.data_structure_analysis.SymbolicValueAnalysis$package$$$Lambda/0x000007ff0132d7d8.apply(Unknown Source)
[279]   at scala.collection.immutable.MapOps.updatedWith(Map.scala:117)
[279]   at scala.collection.immutable.MapOps.updatedWith$(Map.scala:115)
[279]   at scala.collection.immutable.HashMap.updatedWith(HashMap.scala:157)
[279]   at scala.collection.immutable.HashMap.updatedWith(HashMap.scala:39)
[279]   at analysis.data_structure_analysis.SymbolicValueAnalysis$package$.mapMerge$$anonfun$2(SymbolicValueAnalysis.scala:17)
[279]   at analysis.data_structure_analysis.SymbolicValueAnalysis$package$$$Lambda/0x000007ff0132d3c0.applyVoid(Unknown Source)
[279]   at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
[279]   at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
[279]   at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:619)
[279]   at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:617)

Thanks!

Problem01_label50_false-unreach-call.zip

[l-kent]

This seems to just be a scaling issue rather than an infinite loop - it is making progress in the symbolic value analysis, but that is just too memory intensive to handle this case that has a very high amount of branching. It may be possible to optimise the memory usage of the analysis to improve its ability to handle this case, but this would take some significant work.

[aaronbembenek]

Okay, makes sense - thanks for looking into this!

[agle]

Some quick ideas on how we could address this in future:

I'm assuming the OOM is due to the branching requiring loads of "phi nodes" which means there's ~10k indices for each register and just a lot of values in the state domain, expensive joins, etc. Some things that might help:

• leverage the precision provided by the DSA form by implementing a flow-sensitive solver that store only one abstract state for the whole procedure, and only tracks per-block whether the last transfer function was fixed for the current value of the state domain. This type of solver could be factored out of the 'OffsetProp' analysis.
• OR restrict state domain to live variables at each block begin/end ; e.g. as is hacked in here https://github.com/UQ-PAC/BASIL/blob/main/src/main/scala/ir/transforms/Simp.scala#L45, this means you can only query the result at points where the variables are live but should be fine in practice for a flow-sensitive analysis.
  • the worklist solver used here also caches duplicates of the state between blocks in straight line sequences (i.e. a record for before the successor as well as after the predecessor) - relaxing the requirement that calls terminate blocks and coalescing straight line sequences could avoid this, or it could be handled in the solver itself

[l-kent]

I'm assuming the OOM is due to the branching requiring loads of "phi nodes" which means there's ~10k indices for each register and just a lot of values in the state domain, expensive joins, etc.

Yes, this is exactly where the the symbolic value analysis falls over - it ends up with thousands of phi nodes in one procedure and then runs out of memory computing joins.

the worklist solver used here also caches duplicates of the state between blocks in straight line sequences (i.e. a record for before the successor as well as after the predecessor)

I'm not sure how much difference this would make with the way that Scala handles immutable maps, if these two states are the same map and it was copied from one to the other, then I don't think it exists separately in memory?

The other suggestions all seem worthy of further investigation, thanks.