parse modules in parallel (#1103)

* create a flag to parse modules in parallel * better solution for parallel mapping that only parses rules once
runtimeverification · Feb 14, 2020 · 30960d6 · 30960d6
1 parent 4dd4a1c
commit 30960d6
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
@@ -249,7 +249,8 @@ public Definition resolveNonConfigBubbles(Definition defWithConfig, RuleGrammarG
         Module ruleParserModule = gen.getRuleGrammar(defWithConfig.mainModule());
         ParseCache cache = loadCache(ruleParserModule);
         try (ParseInModule parser = RuleGrammarGenerator.getCombinedGrammar(cache.getModule(), isStrict, profileRules, files)) {
-            return DefinitionTransformer.from(m -> this.resolveNonConfigBubbles(m, parser.getScanner(), gen), "parsing rules").apply(defWithConfig);
+            Map<String, Module> parsed = defWithConfig.parMap(m -> this.resolveNonConfigBubbles(m, parser.getScanner(), gen));
+            return DefinitionTransformer.from(m -> Module(m.name(), m.imports(), parsed.get(m.name()).localSentences(), m.att()), "parsing rules").apply(defWithConfig);
         }
     }
 

diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala
@@ -53,6 +53,10 @@ case class Definition(
     case Definition(`mainModule`, `entryModules`, _) => true
     case _ => false
   }
+
+  def parMap(f: Module => Module): java.util.Map[String, Module] = {
+    (entryModules | entryModules.flatMap(_.importedModules)).par.map(f).seq.map(m => m.name -> m).toMap.asJava
+  }
 }
 
 trait Sorting {