From 5a218a6eb6abbd5f1b55e3761e8b5512e3f3ca88 Mon Sep 17 00:00:00 2001 From: draco Date: Sun, 21 Jan 2024 23:49:20 +0800 Subject: [PATCH] Support skip history generation and load elle history Signed-off-by: draco --- src/main/java/Main.java | 61 ++-- src/main/java/checker/PolySI/PolySI.java | 10 +- src/main/java/config/Config.java | 5 + .../exceptions/NotImplementedException.java | 4 + src/main/java/history/History.java | 10 + .../history/loader/ElleHistoryLoader.java | 293 ++++++++++++++++++ src/main/java/util/HistoryLoaderFactory.java | 18 ++ .../java/util/HistorySerializerFactory.java | 18 ++ src/main/java/util/TriFunction.java | 6 + 9 files changed, 398 insertions(+), 27 deletions(-) create mode 100644 src/main/java/exceptions/NotImplementedException.java create mode 100644 src/main/java/history/loader/ElleHistoryLoader.java create mode 100644 src/main/java/util/HistoryLoaderFactory.java create mode 100644 src/main/java/util/HistorySerializerFactory.java create mode 100644 src/main/java/util/TriFunction.java diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 22cf6b6..5c7210a 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -2,6 +2,8 @@ import collector.Collector; import config.Config; import generator.general.GeneralGenerator; +import history.History; +import util.HistoryLoaderFactory; import history.serializer.TextHistorySerializer; import lombok.SneakyThrows; import lombok.extern.slf4j.Slf4j; @@ -10,10 +12,7 @@ import picocli.CommandLine; import picocli.CommandLine.Command; import picocli.CommandLine.Parameters; -import util.ConfigParser; -import util.Profiler; -import util.RuntimeDataSerializer; -import util.RuntimeInfoRecorder; +import util.*; import java.io.FileInputStream; import java.io.IOException; @@ -26,8 +25,6 @@ import java.util.Set; import java.util.concurrent.Callable; import java.util.concurrent.atomic.AtomicInteger; -import java.util.function.BiFunction; -import java.util.function.Function; @Slf4j @Command(name = "DBTest", mixinStandardHelpOptions = true, version = "DBTest 0.1", description = "Test database isolation level.") @@ -84,27 +81,38 @@ public void run(Properties config) { var enableProfile = Boolean.parseBoolean(config.getProperty(Config.PROFILER_ENABLE)); var profiler = Profiler.getInstance(); - int nHist = Integer.parseInt(config.getProperty(Config.WORKLOAD_HISTORY)); + var skipGeneration = Boolean.parseBoolean(config.getProperty(Config.WORKLOAD_SKIP_GENERATION)); + int historyNum = 1; + if (!skipGeneration) { + historyNum = Integer.parseInt(config.getProperty(Config.WORKLOAD_HISTORY)); + } int nBatch = 1; AtomicInteger bugCount = new AtomicInteger(); if (enableProfile) { profiler.startTick("run_total_time"); } - BiFunction runOneShot = (Integer currentBatch, Integer totalBatch) -> { + TriFunction runOneShot = (Integer currentBatch, Integer totalBatch, Integer nHist) -> { for (int i = 1; i <= nHist; i++) { - // generate history - log.info("Start workload generation {} of {}", i + nHist * currentBatch, nHist * totalBatch); - var history = new GeneralGenerator(config).generate(); - - // collect result - log.info("Start history collection"); - try { - var collectorInstance = collector.getDeclaredConstructor(Properties.class).newInstance(config); - history = collectorInstance.collect(history); - collectorInstance.close(); - } catch (InstantiationException | InvocationTargetException | NoSuchMethodException | - IllegalAccessException e) { - throw new RuntimeException(e); + History history = null; + if (!skipGeneration) { + // generate history + log.info("Start workload generation {} of {}", i + nHist * currentBatch, nHist * totalBatch); + history = new GeneralGenerator(config).generate(); + + // collect result + log.info("Start history collection"); + try { + var collectorInstance = collector.getDeclaredConstructor(Properties.class).newInstance(config); + history = collectorInstance.collect(history); + collectorInstance.close(); + } catch (InstantiationException | InvocationTargetException | NoSuchMethodException | + IllegalAccessException e) { + throw new RuntimeException(e); + } + } else { + var historyPath = config.getProperty(Config.HISTORY_PATH).toLowerCase(); + var historyType = config.getProperty(Config.HISTORY_TYPE).toLowerCase(); + history = HistoryLoaderFactory.getHistoryLoader(historyType).loadHistory(historyPath); } // verify history @@ -114,6 +122,7 @@ public void run(Properties config) { } boolean result; try { + // TODO: ww edge in elle history? var checkerInstance = checker.getDeclaredConstructor(Properties.class).newInstance(config); result = checkerInstance.verify(history); if (enableProfile) { @@ -129,7 +138,9 @@ public void run(Properties config) { } catch (IOException e) { } - new TextHistorySerializer().serializeHistory(history, Paths.get(bugDir.toString(), "bug_hist.txt").toString()); + if (!skipGeneration) { + new TextHistorySerializer().serializeHistory(history, Paths.get(bugDir.toString(), "bug_hist.txt").toString()); + } checkerInstance.outputDotFile(Paths.get(bugDir.toString(), "conflict.dot").toString()); } else { log.info("NO BUG"); @@ -153,14 +164,14 @@ public void run(Properties config) { var value = valueList[i]; config.setProperty(variable, value); log.info("Run one shot {} = {}", variable, value); - runOneShot.apply(i, nBatch); + runOneShot.apply(i, nBatch, historyNum); var avgTime = profiler.getAvgTime(checker.getName()); var maxMemory = profiler.getMemory(checker.getName()); Profiler.appendToCSV(value, avgTime, maxMemory); profiler.removeTag(checker.getName()); } } else { - runOneShot.apply(0, nBatch); + runOneShot.apply(0, nBatch, historyNum); } if (enableProfile) { @@ -181,7 +192,7 @@ public void run(Properties config) { // output to the specific dir var outputPath = config.getProperty(Config.OUTPUT_PATH, Config.DEFAULT_OUTPUT_PATH); - RuntimeDataSerializer.getInstance(outputPath).outputToPath(nHist * nBatch, bugCount.get(), config, enableProfile); + RuntimeDataSerializer.getInstance(outputPath).outputToPath(historyNum * nBatch, bugCount.get(), config, enableProfile); } @SneakyThrows diff --git a/src/main/java/checker/PolySI/PolySI.java b/src/main/java/checker/PolySI/PolySI.java index 21df39a..518ba3d 100644 --- a/src/main/java/checker/PolySI/PolySI.java +++ b/src/main/java/checker/PolySI/PolySI.java @@ -8,7 +8,6 @@ import history.History; import util.Profiler; -import java.nio.file.Paths; import java.util.Properties; public class PolySI implements Checker { @@ -25,14 +24,21 @@ public class PolySI implements Checker { public static final String NAME = "PolySI"; public static IsolationLevel ISOLATION_LEVEL; + private final Properties config; + public PolySI(Properties config) { + this.config = config; ISOLATION_LEVEL = IsolationLevel.valueOf(config.getProperty(Config.CHECKER_ISOLATION)); assert ISOLATION_LEVEL == IsolationLevel.SNAPSHOT_ISOLATION; } @Override public boolean verify(History history) { - history.addInitSession(); + if (config.getProperty(Config.HISTORY_TYPE).equals("elle")) { + history.addInitSessionElle(); + } else { + history.addInitSession(); + } Pruning.setEnablePruning(!noPruning); SIVerifier.setCoalesceConstraints(!noCoalescing); diff --git a/src/main/java/config/Config.java b/src/main/java/config/Config.java index af60aef..c44257b 100644 --- a/src/main/java/config/Config.java +++ b/src/main/java/config/Config.java @@ -21,6 +21,11 @@ public class Config { public static final String WORKLOAD_KEY = "workload.key"; public static final String WORKLOAD_DISTRIBUTION = "workload.distribution"; public static final String WORKLOAD_VARIABLE = "workload.variable"; + public static final String WORKLOAD_SKIP_GENERATION = "workload.skipgeneration"; + + // user history configs + public static final String HISTORY_PATH = "history.path"; + public static final String HISTORY_TYPE = "history.type"; // checker configs public static final String CHECKER_ISOLATION = "checker.isolation"; diff --git a/src/main/java/exceptions/NotImplementedException.java b/src/main/java/exceptions/NotImplementedException.java new file mode 100644 index 0000000..85670af --- /dev/null +++ b/src/main/java/exceptions/NotImplementedException.java @@ -0,0 +1,4 @@ +package exceptions; + +public class NotImplementedException extends RuntimeException { +} diff --git a/src/main/java/history/History.java b/src/main/java/history/History.java index bbf9b7c..78efdea 100644 --- a/src/main/java/history/History.java +++ b/src/main/java/history/History.java @@ -1,5 +1,6 @@ package history; +import history.loader.ElleHistoryLoader; import javafx.util.Pair; import lombok.Data; @@ -78,6 +79,15 @@ public void addInitSession() { initTransaction.setSuccess(true); } + public void addInitSessionElle() { + Session initSession = addSession(-1); + Transaction initTransaction = addTransaction(initSession, -1); + for (var i : keySet) { + addOperation(initTransaction, Operation.Type.WRITE, i, (ValType) new ElleHistoryLoader.ElleValue(null, null)); + } + initTransaction.setSuccess(true); + } + public void removeInitSession() { sessions.remove(-1L); } diff --git a/src/main/java/history/loader/ElleHistoryLoader.java b/src/main/java/history/loader/ElleHistoryLoader.java new file mode 100644 index 0000000..d515643 --- /dev/null +++ b/src/main/java/history/loader/ElleHistoryLoader.java @@ -0,0 +1,293 @@ +package history.loader; + +import history.History; +import history.Operation; +import lombok.AllArgsConstructor; +import lombok.Data; +import lombok.EqualsAndHashCode; +import lombok.SneakyThrows; +import org.apache.commons.lang3.tuple.Triple; + +import java.io.BufferedReader; +import java.io.FileReader; +import java.nio.CharBuffer; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.function.BiFunction; +import java.util.regex.Pattern; + +import static java.util.Map.entry; + +@Data +public class ElleHistoryLoader implements HistoryLoader { + private Map sessionIdMap = new HashMap<>(); + private Integer minSessionId = 0; + + @Override + @SneakyThrows + public History loadHistory(String path) { + try (var in = new BufferedReader(new FileReader(path))) { + return parseFile(in); + } + } + + private History parseFile(BufferedReader reader) { + var history = new History(); + reader.lines().forEachOrdered(line -> parseLine(history, CharBuffer.wrap(line))); + return history; + } + + private void parseLine(History history, CharBuffer line) { + // todo: Handle timeout + assertEq(line.charAt(0), '{'); + advance(line, 1); + + var keyRegex = Pattern.compile(":\\w+"); + + ArrayList> txnValue = null; + Integer txnProcess = null; + LogType type = null; + while (line.charAt(0) != '}') { + var result = keyRegex.matcher(line.duplicate()); + + if (!result.lookingAt()) { + throw new RuntimeException(String.format("No match in \"%s\"", line)); + } + skipCommaAndSpace(advance(line, result.group().length())); + + switch (result.group()) { + case ":type": + type = parseType(line); + if (type != LogType.OK && type != LogType.FAIL) { + return; + } + break; + case ":f": + parseF(line); + break; + case ":value": + txnValue = parseValue(line); + break; + case ":time": + parseLong(line); + break; + case ":process": + var sessionId = parseInt(line); + if (sessionIdMap.containsKey(sessionId)) { + txnProcess = sessionIdMap.get(sessionId); + } else { + txnProcess = minSessionId; + minSessionId++; + sessionIdMap.put(sessionId, txnProcess); + } + break; + case ":index": + parseInt(line); + break; + case ":error": + parseErrorList(line); + break; + default: + throw new RuntimeException(String.format("Unknown key \"%s\"", result.group())); + } + + skipCommaAndSpace(line); + } + + if (txnProcess == null || txnValue == null) { + throw new RuntimeException(String.format("Missing :process or :value in \"%s\"", line.clear())); + } + + if (type == LogType.FAIL) { + txnValue.stream(). + filter(v -> v.getLeft().equals(Operation.Type.WRITE)) + .forEach(v -> history.addAbortedWrite(v.getMiddle(), v.getRight())); + return; + } + + var session = history.getSession(txnProcess); + if (session == null) { + session = history.addSession(txnProcess); + } + + var txnId = history.getTransactions().size(); + var txn = history.addTransaction(session, txnId); + + txnValue.forEach(v -> history.addOperation(txn, v.getLeft(), v.getMiddle(), v.getRight())); + } + + private LogType parseType(CharBuffer s) { + var typeMap = Map.ofEntries( + entry(":invoke", LogType.INVOKE), + entry(":ok", LogType.OK), + entry(":fail", LogType.FAIL), + entry(":info", LogType.INFO) + ); + + for (var e : typeMap.entrySet()) { + if (startsWith(s, e.getKey())) { + advance(s, e.getKey().length()); + return e.getValue(); + } + } + + throw new RuntimeException(String.format("Unknown :type in \"%s\"", s)); + } + + private void parseF(CharBuffer s) { + if (!startsWith(s, ":txn")) { + throw new RuntimeException(String.format("Unknown :f in \"%s\"", s)); + } + + advance(s, ":txn".length()); + } + + private ArrayList> parseValue(CharBuffer s) { + assertEq(s.charAt(0), '['); + advance(s, 1); + + var events = new ArrayList>(); + while (true) { + skipCommaAndSpace(s); + if (s.charAt(0) == ']') { + advance(s, 1); + break; + } + events.add(parseEvent(s)); + } + + return events; + } + + private Triple parseEvent(CharBuffer s) { + assertEq(s.charAt(0), '['); + advance(s, 1); + + Triple result; + if (startsWith(s, ":r ")) { + advance(s, ":r ".length()); + var key = parseInt(s); + skipCommaAndSpace(s); + var list = parseList(s); + result = Triple.of(Operation.Type.READ, key, + new ElleValue(list.isEmpty() ? null : list.get(list.size() - 1), list)); + } else if (startsWith(s, ":append ")) { + advance(s, ":append ".length()); + var key = parseInt(s); + skipCommaAndSpace(s); + var value = parseInt(s); + result = Triple.of(Operation.Type.WRITE, key, new ElleValue(value, null)); + } else { + throw new RuntimeException(String.format("Unknown event in \"%s\"", s)); + } + + assertEq(s.charAt(0), ']'); + advance(s, 1); + return result; + } + + private T parseIntegerType(CharBuffer s, BiFunction parser) { + int i = 0; + while (Character.isDigit(s.charAt(i))) { + i++; + } + + var result = parser.apply(s, i); + advance(s, i); + return result; + } + + private Integer parseInt(CharBuffer s) { + return parseIntegerType(s, (cs, i) -> Integer.parseInt(cs, 0, i, 10)); + } + + private Long parseLong(CharBuffer s) { + return parseIntegerType(s, (cs, i) -> Long.parseLong(cs, 0, i, 10)); + } + + private List parseList(CharBuffer s) { + if (startsWith(s, "nil")) { + advance(s, "nil".length()); + return List.of(); + } + + assertEq(s.charAt(0), '['); + advance(s, 1); + + var list = new ArrayList(); + while (true) { + skipCommaAndSpace(s); + if (s.charAt(0) == ']') { + advance(s, 1); + break; + } + list.add(parseInt(s)); + } + + return list; + } + + private void parseErrorList(CharBuffer s) { + assertEq(s.charAt(0), '['); + advance(s, 1); + + while (s.charAt(0) != ']') { + advance(s, 1); + } + advance(s, 1); + } + + private void assertEq(char a, char b) { + if (a != b) { + throw new AssertionError(); + } + } + + private CharBuffer skipCommaAndSpace(CharBuffer s) { + int i = 0; + while (s.charAt(i) == ',' || s.charAt(i) == ' ') { + i++; + } + + return advance(s, i); + } + + private CharBuffer advance(CharBuffer s, int length) { + return s.position(s.position() + length); + } + + private boolean startsWith(CharSequence a, CharSequence b) { + for (int i = 0; i < b.length(); i++) { + if (a.charAt(i) != b.charAt(i)) { + return false; + } + } + + return true; + } + + private enum LogType { + INVOKE, OK, FAIL, INFO + } + + @Data + @EqualsAndHashCode(onlyExplicitlyIncluded = true) + @AllArgsConstructor + public static class ElleValue { + @EqualsAndHashCode.Include + Integer lastElement; + + List list; + + @Override + public String toString() { + if (list == null) { + return String.format("ElleAppend(%d)", lastElement); + } else { + return String.format("ElleList(%s)", list); + } + } + } +} diff --git a/src/main/java/util/HistoryLoaderFactory.java b/src/main/java/util/HistoryLoaderFactory.java new file mode 100644 index 0000000..bc663a6 --- /dev/null +++ b/src/main/java/util/HistoryLoaderFactory.java @@ -0,0 +1,18 @@ +package util; + +import history.loader.ElleHistoryLoader; +import history.loader.HistoryLoader; +import history.loader.TextHistoryLoader; + +public class HistoryLoaderFactory { + public static HistoryLoader getHistoryLoader(String type) { + switch (type) { + case "text": + return new TextHistoryLoader(); + case "elle": + return new ElleHistoryLoader(); + default: + throw new RuntimeException("Unknown history type"); + } + } +} diff --git a/src/main/java/util/HistorySerializerFactory.java b/src/main/java/util/HistorySerializerFactory.java new file mode 100644 index 0000000..fecd1fe --- /dev/null +++ b/src/main/java/util/HistorySerializerFactory.java @@ -0,0 +1,18 @@ +package util; + +import exceptions.NotImplementedException; +import history.serializer.HistorySerializer; +import history.serializer.TextHistorySerializer; + +public class HistorySerializerFactory { + public static HistorySerializer getHistorySerializer(String type) { + switch (type) { + case "text": + return new TextHistorySerializer(); + case "elle": + throw new NotImplementedException(); + default: + throw new RuntimeException("Unknown history type"); + } + } +} diff --git a/src/main/java/util/TriFunction.java b/src/main/java/util/TriFunction.java new file mode 100644 index 0000000..db7c42c --- /dev/null +++ b/src/main/java/util/TriFunction.java @@ -0,0 +1,6 @@ +package util; + +@FunctionalInterface +public interface TriFunction { + R apply(A a, B b, C c); +}