From 6aea23f23f7df9544380b0b32d7422bcd107a128 Mon Sep 17 00:00:00 2001 From: Marco Antognini <antognini.marco@gmail.com> Date: Wed, 27 Sep 2017 11:55:28 +0200 Subject: [PATCH 1/4] Quick'n'dirty fix for SimplifierWithPC This ensures that the trait is thread safe. Ideally, it's internal state shouldn't be mutable and/or the critical section should be reduced to its minimal size for better thoughput efficiency. --- src/main/scala/inox/transformers/SimplifierWithPC.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala index 9d3322b2d..1f96df28b 100644 --- a/src/main/scala/inox/transformers/SimplifierWithPC.scala +++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala @@ -216,11 +216,11 @@ trait SimplifierWithPC extends TransformerWithPC { self => } } - def isPure(e: Expr, path: CNFPath): Boolean = simplify(e, path)._2 + def isPure(e: Expr, path: CNFPath): Boolean = synchronized { simplify(e, path)._2 } private val simplifyCache = new LruCache[Expr, (CNFPath, Expr, Boolean)](100) - def simplify(e: Expr, path: CNFPath): (Expr, Boolean) = e match { + private def simplify(e: Expr, path: CNFPath): (Expr, Boolean) = e match { case e if path contains e => (BooleanLiteral(true), true) case e if path contains not(e) => (BooleanLiteral(false), true) @@ -423,7 +423,7 @@ trait SimplifierWithPC extends TransformerWithPC { self => (re, pe) } - override protected def rec(e: Expr, path: CNFPath): Expr = { + override protected def rec(e: Expr, path: CNFPath): Expr = synchronized { stack = if (stack.isEmpty) Nil else (stack.head + 1) :: stack.tail val (re, pe) = simplify(e, path) purity = if (stack.isEmpty) purity else pe :: purity -- GitLab From 73aafe29aa32d7f66f495f2813db09132f7d1498 Mon Sep 17 00:00:00 2001 From: Marco Antognini <antognini.marco@gmail.com> Date: Wed, 27 Sep 2017 18:20:06 +0200 Subject: [PATCH 2/4] Use thread local variables instead of heavy locks --- .../inox/transformers/SimplifierWithPC.scala | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala index 1f96df28b..789c4e7a9 100644 --- a/src/main/scala/inox/transformers/SimplifierWithPC.scala +++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala @@ -4,6 +4,8 @@ package inox package transformers import utils._ + +import scala.util.DynamicVariable import scala.collection.mutable.{Map => MutableMap} trait SimplifierWithPC extends TransformerWithPC { self => @@ -170,8 +172,8 @@ trait SimplifierWithPC extends TransformerWithPC { self => // (since aggressive caching of cnf computations is taking place) def initEnv: CNFPath = CNFPath.empty - private[this] var stack: List[Int] = Nil - private[this] var purity: List[Boolean] = Nil + private[this] var dynStack: DynamicVariable[List[Int]] = new DynamicVariable(Nil) + private[this] var dynPurity: DynamicVariable[List[Boolean]] = new DynamicVariable(Nil) private val pureCache: MutableMap[Identifier, Boolean] = MutableMap.empty @@ -216,7 +218,7 @@ trait SimplifierWithPC extends TransformerWithPC { self => } } - def isPure(e: Expr, path: CNFPath): Boolean = synchronized { simplify(e, path)._2 } + def isPure(e: Expr, path: CNFPath): Boolean = simplify(e, path)._2 private val simplifyCache = new LruCache[Expr, (CNFPath, Expr, Boolean)](100) @@ -407,12 +409,12 @@ trait SimplifierWithPC extends TransformerWithPC { self => } case _ => - stack = 0 :: stack + dynStack.value = 0 :: dynStack.value val re = super.rec(e, path) - val (rpure, rest) = purity.splitAt(stack.head) + val (rpure, rest) = dynPurity.value.splitAt(dynStack.value.head) val pe = rpure.foldLeft(opts.assumeChecked || !isImpureExpr(re))(_ && _) - stack = stack.tail - purity = rest + dynStack.value = dynStack.value.tail + dynPurity.value = rest (re, pe) } @@ -423,10 +425,10 @@ trait SimplifierWithPC extends TransformerWithPC { self => (re, pe) } - override protected def rec(e: Expr, path: CNFPath): Expr = synchronized { - stack = if (stack.isEmpty) Nil else (stack.head + 1) :: stack.tail + override protected def rec(e: Expr, path: CNFPath): Expr = { + dynStack.value = if (dynStack.value.isEmpty) Nil else (dynStack.value.head + 1) :: dynStack.value.tail val (re, pe) = simplify(e, path) - purity = if (stack.isEmpty) purity else pe :: purity + dynPurity.value = if (dynStack.value.isEmpty) dynPurity.value else pe :: dynPurity.value re } } -- GitLab From 786ab00ccf8d5c4331d464c9aa7a667bd25e48a3 Mon Sep 17 00:00:00 2001 From: Marco Antognini <antognini.marco@gmail.com> Date: Thu, 28 Sep 2017 10:28:41 +0200 Subject: [PATCH 3/4] Further improve thread safety of SimplifierWithPC --- .../inox/transformers/SimplifierWithPC.scala | 32 ++++++++++--------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala index 789c4e7a9..a4813b3dc 100644 --- a/src/main/scala/inox/transformers/SimplifierWithPC.scala +++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala @@ -177,24 +177,26 @@ trait SimplifierWithPC extends TransformerWithPC { self => private val pureCache: MutableMap[Identifier, Boolean] = MutableMap.empty - private def isPureFunction(id: Identifier): Boolean = opts.assumeChecked || (pureCache.get(id) match { - case Some(b) => b - case None => - val fd = getFunction(id) - if (transitivelyCalls(fd, fd)) { - pureCache += id -> false - false - } else { - pureCache += id -> true - if (isPure(fd.fullBody, CNFPath.empty)) { - true - } else { + private def isPureFunction(id: Identifier): Boolean = opts.assumeChecked || synchronized { + pureCache.get(id) match { + case Some(b) => b + case None => + val fd = getFunction(id) + if (transitivelyCalls(fd, fd)) { pureCache += id -> false - transitiveCallers(fd).foreach(fd => pureCache += fd.id -> false) false + } else { + if (isPure(fd.fullBody, CNFPath.empty)) { + pureCache += id -> true + true + } else { + pureCache += id -> false + transitiveCallers(fd) foreach { pureCache += _.id -> false } + false + } } - } - }) + } + } private def isInstanceOf(e: Expr, tpe: ADTType, path: CNFPath): Option[Boolean] = { val tadt = tpe.getADT -- GitLab From fd14dde0ecc81ec35ef6d9223d7fac987e1c612a Mon Sep 17 00:00:00 2001 From: Marco Antognini <antognini.marco@gmail.com> Date: Thu, 28 Sep 2017 14:28:41 +0200 Subject: [PATCH 4/4] Update SimplifierWithPC.isPureFunction --- .../inox/transformers/SimplifierWithPC.scala | 41 ++++++++++--------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala index a4813b3dc..6c10d4ca6 100644 --- a/src/main/scala/inox/transformers/SimplifierWithPC.scala +++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala @@ -175,27 +175,28 @@ trait SimplifierWithPC extends TransformerWithPC { self => private[this] var dynStack: DynamicVariable[List[Int]] = new DynamicVariable(Nil) private[this] var dynPurity: DynamicVariable[List[Boolean]] = new DynamicVariable(Nil) - private val pureCache: MutableMap[Identifier, Boolean] = MutableMap.empty - - private def isPureFunction(id: Identifier): Boolean = opts.assumeChecked || synchronized { - pureCache.get(id) match { - case Some(b) => b + private sealed abstract class PurityCheck + private case object Pure extends PurityCheck + private case object Impure extends PurityCheck + private case object Checking extends PurityCheck + + private[this] val pureCache: MutableMap[Identifier, PurityCheck] = MutableMap.empty + + private def isPureFunction(id: Identifier): Boolean = { + opts.assumeChecked || + synchronized(pureCache.get(id) match { + case Some(Pure) => true + case Some(Impure) => false + case Some(Checking) => + // Function is recursive and cycles were not pruned by the simplifier. + // No need to update pureCache here as the update will take place in the next branch. + false case None => - val fd = getFunction(id) - if (transitivelyCalls(fd, fd)) { - pureCache += id -> false - false - } else { - if (isPure(fd.fullBody, CNFPath.empty)) { - pureCache += id -> true - true - } else { - pureCache += id -> false - transitiveCallers(fd) foreach { pureCache += _.id -> false } - false - } - } - } + pureCache += id -> Checking + val p = isPure(getFunction(id).fullBody, CNFPath.empty) + pureCache += id -> (if (p) Pure else Impure) + p + }) } private def isInstanceOf(e: Expr, tpe: ADTType, path: CNFPath): Option[Boolean] = { -- GitLab