Added Logika branch parallelization prediction options.

sireum · Jan 14, 2025 · 1c7023a · 1c7023a
1 parent 11de84c
commit 1c7023a
Show file tree

Hide file tree

Showing 6 changed files with 48 additions and 8 deletions.
diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala
@@ -99,7 +99,9 @@ object LogikaTest {
       rwTrace = T,
       rwMax = 100,
       rwPar = T,
-      rwEvalTrace = T
+      rwEvalTrace = T,
+      branchParPredNum = 2,
+      branchParPredComp = 10
     )
 
   lazy val isInGithubAction: B = Os.env("GITHUB_ACTION").nonEmpty

diff --git a/shared/src/main/scala/org/sireum/logika/Config.scala b/shared/src/main/scala/org/sireum/logika/Config.scala
@@ -70,7 +70,9 @@ import org.sireum._
                        val rwTrace: B,
                        val rwMax: Z,
                        val rwPar: B,
-                       val rwEvalTrace: B) {
+                       val rwEvalTrace: B,
+                       val branchParPredNum: Z,
+                       val branchParPredComp: Z) {
 
   @memoize def fingerprint: U64 = {
     return ops.StringOps(string).sha3U64(T, T)

diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -4393,12 +4393,12 @@ import Util._
       }
 
       @pure def shouldPar: B = {
-        if (branches.size > 2) {
-          return T
-        }
         if (branches.size == 1) {
           return F
         }
+        if (branches.size >= config.branchParPredNum) {
+          return T
+        }
 
         var compNum = 0
         for (b <- branches) {
@@ -4408,7 +4408,7 @@ import Util._
           }
         }
 
-        if (compNum < 10) {
+        if (compNum < config.branchParPredComp) {
           return F
         }
 

diff --git a/shared/src/main/scala/org/sireum/logika/cli.scala b/shared/src/main/scala/org/sireum/logika/cli.scala
@@ -148,6 +148,12 @@ object cli {
         Opt(name = "branchParReturn", longKey = "par-branch-return", shortKey = None(),
           tpe = Type.Flag(F),
           description = "Only use branch parallelization if all branches return"),
+        Opt(name = "branchPredNum", longKey = "par-branch-pred-num", shortKey = None(),
+          tpe = Type.Num(sep = None(), default = 2, min = Some(2), max = None()),
+          description = "Branch parallelization prediction minimum number of branches"),
+        Opt(name = "branchPredComplexity", longKey = "par-branch-pred-complexity", shortKey = None(),
+          tpe = Type.Num(sep = None(), default = 10, min = Some(0), max = None()),
+          description = "Branch parallelization prediction statement complexity"),
         Opt(name = "rwPar", longKey = "par-rw", shortKey = None(),
           tpe = Type.Flag(T),
           description = "Enable rewriting parallelization")

diff --git a/shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala b/shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala
@@ -92,6 +92,8 @@ object OptionsCli {
     val par: Option[Z],
     val branchPar: B,
     val branchParReturn: B,
+    val branchPredNum: Z,
+    val branchPredComplexity: Z,
     val rwPar: B,
     val dontSplitFunQuant: B,
     val splitAll: B,
@@ -256,6 +258,12 @@ import OptionsCli._
           |                           100; default is 100)
           |    --par-branch         Enable branch parallelization
           |    --par-branch-return  Only use branch parallelization if all branches return
+          |    --par-branch-pred-num
+          |                          Enable branch parallelization (expects an integer;
+          |                           min is 2; default is 2)
+          |    --par-branch-pred-complexity
+          |                          Enable branch parallelization (expects an integer;
+          |                           min is 0; default is 10)
           |    --par-rw             Enable rewriting parallelization
           |
           |Path Splitting Options:
@@ -322,6 +330,8 @@ import OptionsCli._
     var par: Option[Z] = None()
     var branchPar: B = false
     var branchParReturn: B = false
+    var branchPredNum: Z = 2
+    var branchPredComplexity: Z = 10
     var rwPar: B = true
     var dontSplitFunQuant: B = false
     var splitAll: B = false
@@ -538,6 +548,18 @@ import OptionsCli._
              case Some(v) => branchParReturn = v
              case _ => return None()
            }
+         } else if (arg == "--par-branch-pred-num") {
+           val o: Option[Z] = parseNum(args, j + 1, Some(2), None())
+           o match {
+             case Some(v) => branchPredNum = v
+             case _ => return None()
+           }
+         } else if (arg == "--par-branch-pred-complexity") {
+           val o: Option[Z] = parseNum(args, j + 1, Some(0), None())
+           o match {
+             case Some(v) => branchPredComplexity = v
+             case _ => return None()
+           }
          } else if (arg == "--par-rw") {
            val o: Option[B] = { j = j - 1; Some(!rwPar) }
            o match {
@@ -661,7 +683,7 @@ import OptionsCli._
         isOption = F
       }
     }
-    return Some(LogikaOption(help, parseArguments(args, j), background, manual, smt2Caching, transitionCaching, infoFlow, charBitWidth, fpRounding, useReal, intBitWidth, interprocedural, interproceduralContracts, strictPureMode, line, loopBound, callBound, patternExhaustive, pureFun, sat, skipMethods, skipTypes, logPc, logPcLines, logRawPc, logVc, logVcDir, logDetailedInfo, logAtRewrite, stats, par, branchPar, branchParReturn, rwPar, dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwMax, rwTrace, rwEvalTrace, elideEncoding, rawInscription, rlimit, sequential, simplify, smt2SatConfigs, smt2ValidConfigs, satTimeout, timeout, searchPC))
+    return Some(LogikaOption(help, parseArguments(args, j), background, manual, smt2Caching, transitionCaching, infoFlow, charBitWidth, fpRounding, useReal, intBitWidth, interprocedural, interproceduralContracts, strictPureMode, line, loopBound, callBound, patternExhaustive, pureFun, sat, skipMethods, skipTypes, logPc, logPcLines, logRawPc, logVc, logVcDir, logDetailedInfo, logAtRewrite, stats, par, branchPar, branchParReturn, branchPredNum, branchPredComplexity, rwPar, dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwMax, rwTrace, rwEvalTrace, elideEncoding, rawInscription, rlimit, sequential, simplify, smt2SatConfigs, smt2ValidConfigs, satTimeout, timeout, searchPC))
   }
 
   def parseArguments(args: ISZ[String], i: Z): ISZ[String] = {

diff --git a/shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala b/shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala
@@ -176,7 +176,9 @@ object OptionsUtil {
       rwTrace = o.rwTrace,
       rwMax = o.rwMax,
       rwPar = o.rwPar,
-      rwEvalTrace = o.rwEvalTrace
+      rwEvalTrace = o.rwEvalTrace,
+      branchParPredNum = o.branchPredNum,
+      branchParPredComp = o.branchPredComplexity
     )
     return Either.Left(config)
   }
@@ -337,6 +339,12 @@ object OptionsUtil {
       if (config.rwEvalTrace != defaultConfig.rwEvalTrace) {
         r = r :+ "--rw-eval-trace"
       }
+      if (config.branchParPredNum != defaultConfig.branchParPredNum) {
+        r = r ++ ISZ[String]("--par-branch-pred-num", config.branchParPredNum.string)
+      }
+      if (config.branchParPredComp != defaultConfig.branchParPredComp) {
+        r = r ++ ISZ[String]("--par-branch-pred-complexity", config.branchParPredComp.string)
+      }
     }
     config.background match {
       case Config.BackgroundMode.Type => r = r ++ ISZ[String]("--background", "type")