Update to match "Making Formulog Fast" artifact (HarvardPL#83)

* Add flag for eager eval; update README; update Boost version.

* Add eager eval codegen to unit testing.

* Add comments.

* Fix some formatting.

* Skip uploading dependency graph in GH Action.

.github/workflows/maven.yml

@@ -35,5 +35,5 @@ jobs:
       run: mvn -B verify --file pom.xml
 
     # Optional: Uploads the full dependency graph to GitHub to improve the quality of Dependabot alerts this repository can receive
-    - name: Update dependency graph
-      uses: advanced-security/maven-dependency-submission-action@571e99aab1055c2e71a1e2309b9691de18d6b7d6
+    # - name: Update dependency graph
+    #   uses: advanced-security/maven-dependency-submission-action@571e99aab1055c2e71a1e2309b9691de18d6b7d6

README.md

@@ -131,8 +131,9 @@ The Formulog interpreter currently provides the following options:
 
 ```
 Usage: formulog [-chV] [--dump-all] [--dump-idb] [--dump-query] [--dump-sizes]
-                [--smt-stats] [--codegen-dir=<codegenDir>] [-D=<outDir>]
-                [-j=<parallelism>] [--smt-solver-mode=<smtStrategy>]
+                [--eager-eval] [--smt-stats] [--codegen-dir=<codegenDir>]
+                [-D=<outDir>] [-j=<parallelism>]
+                [--smt-solver-mode=<smtStrategy>]
                 [--dump=<relationsToPrint>]... [-F=<factDirs>]... <file>
 Runs Formulog.
       <file>         Formulog program file.
@@ -147,6 +148,8 @@ Runs Formulog.
       --dump-idb     Print all IDB relations.
       --dump-query   Print query result.
       --dump-sizes   Print relation sizes.
+      --eager-eval   Use eager evaluation (instead of traditional semi-naive
+                       Datalog evaluation)
   -F, --fact-dir=<factDirs>
                      Directory to look for fact .tsv files (default: '.').
   -h, --help         Show this help message and exit.
@@ -243,12 +246,30 @@ To build the generated code, you must have:
 
 - A C++ compiler that supports the C++17 standard (and OpenMP, if you want to produce a parallelized binary)
 - `cmake` (v3.21+)
-- [`boost`](https://www.boost.org/) (a version compatible with v1.79)
+- [`boost`](https://www.boost.org/) (a version compatible with v1.81)
 - [`oneTBB`](https://oneapi-src.github.io/oneTBB/) (v2021.8.0 is known to work)
 - [`souffle`](https://souffle-lang.github.io/) (v2.3 is known to work)
 
 The Formulog Docker image already has these dependencies installed.
 
+## Eager Evaluation
+
+In addition to traditional semi-naive Datalog evaluation, Formulog supports _eager_ evaluation, a novel concurrent evaluation algorithm for Datalog that is faster than semi-naive evaluation on some Formulog workloads (often because it induces a more favorable distribution of the SMT workload across SMT solvers).
+Whereas semi-naive evaluation batches derived tuples to process them in explicit rounds, eager evaluation eagerly pursues the consequences of each tuple as it is derived.
+
+Using eager evaluation with the Formulog interpreter is easy: just add the `--eager-eval` flag.
+Eager evaluation can also be used with the Formulog compiler, provided you install [our custom version of Souffle](https://github.com/aaronbembenek/souffle).
+When you configure `cmake` on the generated code, you need to add `-DFLG_EAGER_EVAL=On`.
+For example, to build a version of the greeting program that uses eager evaluation, use these commands:
+
+```shellsession
+$ java -jar formulog.jar -c greeting.flg
+$ cd codegen
+$ cmake -B build -S . -DFLG_EAGER_EVAL=On
+$ cmake --build build -j
+$ ./build/flg --dump-idb
+```
+
 ## Writing Formulog programs
 
 See the documentation in `docs/`. Some shortish example programs can be found in

src/main/java/edu/harvard/seas/pl/formulog/Configuration.java

@@ -22,7 +22,11 @@
 import edu.harvard.seas.pl.formulog.ast.Rule;
 import edu.harvard.seas.pl.formulog.db.IndexedFactDb;
 import edu.harvard.seas.pl.formulog.eval.IndexedRule;
-import edu.harvard.seas.pl.formulog.smt.*;
+import edu.harvard.seas.pl.formulog.smt.CheckSatAssumingSolver;
+import edu.harvard.seas.pl.formulog.smt.PushPopSolver;
+import edu.harvard.seas.pl.formulog.smt.SmtLibSolver;
+import edu.harvard.seas.pl.formulog.smt.SmtStatus;
+import edu.harvard.seas.pl.formulog.smt.SmtStrategy;
 import edu.harvard.seas.pl.formulog.symbols.FunctionSymbol;
 import edu.harvard.seas.pl.formulog.symbols.RelationSymbol;
 import edu.harvard.seas.pl.formulog.util.Dataset;
@@ -31,7 +35,13 @@
 import edu.harvard.seas.pl.formulog.util.SharedLong;
 import edu.harvard.seas.pl.formulog.util.Util;
 import java.io.PrintStream;
-import java.util.*;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Map;
 import java.util.Map.Entry;
 import java.util.concurrent.ConcurrentHashMap;
 import java.util.concurrent.atomic.AtomicInteger;
@@ -151,8 +161,9 @@ public static long getSmtTotalTime() {
   public static final String debugStratificationOutDir =
       getStringProp("debugStratificationOutDir", "stratification_graphs");
 
-  public static final boolean testCodegen = propIsSet("testCodegen");
-  public static final boolean keepCodegenTestDirs = propIsSet("keepCodegenTestDirs");
+  public static final boolean testCodeGen = propIsSet("testCodeGen");
+  public static final boolean testCodeGenEager = propIsSet("testCodeGenEager");
+  public static final boolean keepCodeGenTestDirs = propIsSet("keepCodeGenTestDirs");
   public static final String cxxCompiler = getStringProp("cxxCompiler", null);
 
   public static final String souffleInclude = System.getProperty("souffleInclude");

src/main/java/edu/harvard/seas/pl/formulog/Main.java

@@ -19,7 +19,11 @@
  */
 package edu.harvard.seas.pl.formulog;
 
-import edu.harvard.seas.pl.formulog.ast.*;
+import edu.harvard.seas.pl.formulog.ast.BasicProgram;
+import edu.harvard.seas.pl.formulog.ast.BasicRule;
+import edu.harvard.seas.pl.formulog.ast.Program;
+import edu.harvard.seas.pl.formulog.ast.Term;
+import edu.harvard.seas.pl.formulog.ast.UserPredicate;
 import edu.harvard.seas.pl.formulog.codegen.CodeGen;
 import edu.harvard.seas.pl.formulog.eval.Evaluation;
 import edu.harvard.seas.pl.formulog.eval.EvaluationException;
@@ -35,18 +39,32 @@
 import edu.harvard.seas.pl.formulog.types.WellTypedProgram;
 import edu.harvard.seas.pl.formulog.util.Util;
 import edu.harvard.seas.pl.formulog.validating.InvalidProgramException;
-import java.io.*;
+import java.io.File;
+import java.io.FileNotFoundException;
+import java.io.FileReader;
+import java.io.IOException;
+import java.io.PrintStream;
 import java.nio.file.Path;
 import java.nio.file.Paths;
-import java.util.*;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.List;
+import java.util.Set;
 import java.util.concurrent.Callable;
 import java.util.concurrent.Executors;
 import java.util.concurrent.TimeUnit;
 import java.util.stream.Collectors;
 import org.apache.commons.lang3.time.StopWatch;
 import picocli.CommandLine;
-import picocli.CommandLine.*;
+import picocli.CommandLine.Command;
+import picocli.CommandLine.ITypeConverter;
 import picocli.CommandLine.Model;
+import picocli.CommandLine.Option;
+import picocli.CommandLine.ParameterException;
+import picocli.CommandLine.Parameters;
+import picocli.CommandLine.Spec;
 
 @Command(
     name = "formulog",
@@ -65,6 +83,11 @@ public final class Main implements Callable<Integer> {
       converter = SmtModeConverter.class)
   public static SmtStrategy smtStrategy = Configuration.getSmtStrategy();
 
+  @Option(
+      names = "--eager-eval",
+      description = "Use eager evaluation (instead of traditional semi-naive Datalog evaluation)")
+  public static boolean eagerEval = Configuration.eagerSemiNaive;
+
   @Option(
       names = {"-F", "--fact-dir"},
       description = "Directory to look for fact .tsv files (default: '.').")
@@ -188,7 +211,7 @@ private Evaluation setup(WellTypedProgram prog) {
     clock.reset();
     clock.start();
     try {
-      Evaluation eval = SemiNaiveEvaluation.setup(prog, parallelism, Configuration.eagerSemiNaive);
+      Evaluation eval = SemiNaiveEvaluation.setup(prog, parallelism, eagerEval);
       clock.stop();
       System.out.println("Finished rewriting and validating (" + clock.getTime() / 1000.0 + "s)");
       return eval;

src/main/java/edu/harvard/seas/pl/formulog/eval/AbstractStratumEvaluator.java

@@ -41,6 +41,14 @@
 import java.util.Map;
 import java.util.Set;
 
+/**
+ * This class represents an abstract stratum evaluation method (e.g., semi-naive evaluation, eager
+ * evaluation). It includes functionality common to different evaluation techniques. Most notably,
+ * it splits a rule into a prefix (which conceptually contains no loops and can be processed
+ * sequentially) and a suffix (which contains loops that should be parallelized); additionally, it
+ * contains the code for evaluating the suffix of a rule, which is the "hot loop" during Datalog
+ * evaluation.
+ */
 public abstract class AbstractStratumEvaluator implements StratumEvaluator {
 
   protected final Set<IndexedRule> firstRoundRules = new HashSet<>();

src/main/java/edu/harvard/seas/pl/formulog/eval/EagerStratumEvaluator.java

@@ -42,6 +42,14 @@
 import java.util.Iterator;
 import java.util.Set;
 
+/**
+ * This class implements eager evaluation of a stratum, an alternative evaluation strategy to
+ * traditional semi-naive Datalog evaluation. Instead of batching newly derived tuples into explicit
+ * rounds of evaluation (like semi-naive evaluation), eager evaluation eagerly pursues the
+ * consequences of newly derived tuples; this is achieved by immediately submitting work items for
+ * each newly derived tuple to a work-stealing thread pool that selects the next item to evaluate
+ * using the LIFO order.
+ */
 public final class EagerStratumEvaluator extends AbstractStratumEvaluator {
 
   private final SortedIndexedFactDb db;

src/main/java/edu/harvard/seas/pl/formulog/eval/RoundBasedStratumEvaluator.java

@@ -42,6 +42,15 @@
 import java.util.Set;
 import org.apache.commons.lang3.time.StopWatch;
 
+/**
+ * This class implements traditional semi-naive evaluation of a stratum, in which rule atoms refer
+ * to auxiliary relations indexed by round of the fixpoint evaluation. For example, if the predicate
+ * p is recursive in the current stratum, going into round i+1, there will be the relation
+ * delta_i(p) holding the p facts derived in round i, and the relation p_{i+1} holding the entire p
+ * relation at the beginning of round i+1. Unlike some versions of semi-naive evaluation, we do not
+ * use the auxiliary relation p_i (that is, the relation p as it stood at the beginning of the
+ * previous round) when adorning non-linearly recursive rules.
+ */
 public final class RoundBasedStratumEvaluator extends AbstractStratumEvaluator {
 
   private final int stratumNum;

src/main/resources/codegen/CMakeLists.txt

@@ -53,7 +53,7 @@ target_sources(flg PRIVATE
         formulog.cpp
         )
 
-find_package(Boost 1.79 REQUIRED COMPONENTS filesystem system program_options)
+find_package(Boost 1.81 REQUIRED COMPONENTS filesystem system program_options)
 find_package(TBB REQUIRED)
 target_link_libraries(flg PRIVATE ${Boost_LIBRARIES} TBB::tbb)
 

src/test/java/edu/harvard/seas/pl/formulog/codegen/CompiledSemiNaiveTester.java → src/test/java/edu/harvard/seas/pl/formulog/codegen/CodeGenTester.java

@@ -30,7 +30,14 @@
 import edu.harvard.seas.pl.formulog.types.TypeChecker;
 import edu.harvard.seas.pl.formulog.types.WellTypedProgram;
 import edu.harvard.seas.pl.formulog.util.Util;
-import java.io.*;
+import java.io.BufferedReader;
+import java.io.ByteArrayOutputStream;
+import java.io.File;
+import java.io.FileNotFoundException;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.InputStreamReader;
+import java.io.PrintStream;
 import java.net.URL;
 import java.nio.file.Path;
 import java.nio.file.Paths;
@@ -39,9 +46,14 @@
 import java.util.Collections;
 import java.util.List;
 
-public class CompiledSemiNaiveTester implements Tester {
+public class CodeGenTester implements Tester {
 
   private List<String> inputDirs = Collections.emptyList();
+  private final boolean eagerEval;
+
+  public CodeGenTester(boolean eagerEval) {
+    this.eagerEval = eagerEval;
+  }
 
   @Override
   public void test(String file, List<String> inputDirs) {
@@ -78,7 +90,7 @@ public void test(String file, List<String> inputDirs) {
       e.printStackTrace(out);
       fail(baos.toString());
     } finally {
-      if (!Configuration.keepCodegenTestDirs && topPath != null) {
+      if (!Configuration.keepCodeGenTestDirs && topPath != null) {
         Util.clean(topPath.toFile(), true);
       }
     }
@@ -100,6 +112,9 @@ private boolean evaluate(String name, Path topPath, BasicProgram prog) throws Ex
                 "-S",
                 topPath.toString(),
                 "-DCMAKE_BUILD_TYPE=Debug"));
+    if (eagerEval) {
+      cmakeCmds.add("-DFLG_EAGER_EVAL=On");
+    }
     if (Configuration.cxxCompiler != null) {
       cmakeCmds.add("-DCMAKE_CXX_COMPILER=" + Configuration.cxxCompiler);
     }

src/test/java/edu/harvard/seas/pl/formulog/codegen/CompiledEagerEvaluationTest.java

@@ -0,0 +1,59 @@
+/*-
+ * #%L
+ * Formulog
+ * %%
+ * Copyright (C) 2024 President and Fellows of Harvard College
+ * %%
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ * #L%
+ */
+package edu.harvard.seas.pl.formulog.codegen;
+
+/*-
+ * #%L
+ * Formulog
+ * %%
+ * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * %%
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ * #L%
+ */
+
+import edu.harvard.seas.pl.formulog.Configuration;
+import edu.harvard.seas.pl.formulog.eval.CommonEvaluationTest;
+import edu.harvard.seas.pl.formulog.eval.SemiNaiveEvaluation;
+
+public class CompiledEagerEvaluationTest extends CommonEvaluationTest<SemiNaiveEvaluation> {
+
+  static {
+    if (!Configuration.testCodeGenEager) {
+      System.err.println(
+          "WARNING: skipping CompiledEagerEvaluationTest; enable with system property"
+              + " `-DtestCodeGenEager`");
+    }
+  }
+
+  public CompiledEagerEvaluationTest() {
+    super(Configuration.testCodeGenEager ? new CodeGenTester(true) : new NopTester<>());
+  }
+}

src/test/java/edu/harvard/seas/pl/formulog/codegen/CompiledEagerMagicSetTest.java

@@ -0,0 +1,59 @@
+/*-
+ * #%L
+ * Formulog
+ * %%
+ * Copyright (C) 2024 President and Fellows of Harvard College
+ * %%
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ * #L%
+ */
+package edu.harvard.seas.pl.formulog.codegen;
+
+/*-
+ * #%L
+ * Formulog
+ * %%
+ * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * %%
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ * #L%
+ */
+
+import edu.harvard.seas.pl.formulog.Configuration;
+import edu.harvard.seas.pl.formulog.eval.SemiNaiveEvaluation;
+import edu.harvard.seas.pl.formulog.magic.CommonMagicSetTest;
+
+public class CompiledEagerMagicSetTest extends CommonMagicSetTest<SemiNaiveEvaluation> {
+
+  static {
+    if (!Configuration.testCodeGenEager) {
+      System.err.println(
+          "WARNING: skipping CompiledEagerMagicSetTest; enable with system property"
+              + " `-DtestCodeGenEager`");
+    }
+  }
+
+  public CompiledEagerMagicSetTest() {
+    super(Configuration.testCodeGenEager ? new CodeGenTester(true) : new NopTester<>());
+  }
+}