diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 9ffb2c2e..9c874fee 100644 --- a/.github/workflows/gradle.yml +++ b/.github/workflows/gradle.yml @@ -1,67 +1,266 @@ -# This workflow uses actions that are not certified by GitHub. -# They are provided by a third-party and are governed by -# separate terms of service, privacy policy, and support -# documentation. -# This workflow will build a Java project with Gradle and cache/restore any dependencies to improve the workflow execution time -# For more information see: https://docs.github.com/en/actions/automating-builds-and-tests/building-and-testing-java-with-gradle +# Faithful GitHub Actions port of .gitlab-ci.yml. +# +# GitLab runs the pipeline on the `master` branch; GitHub runs it on `main`. +# Both branches are listed in the triggers/conditions below so the pipeline +# behaves identically on either platform without further edits. +# +# This workflow uses actions provided by a third-party (gradle/actions); they +# are governed by separate terms of service, privacy policy and support docs. -name: Java CI with Gradle +name: JMC CI on: push: - branches: [ "master" ] + branches: [ "main", "master" ] pull_request: - branches: [ "master" ] + branches: [ "main", "master" ] + +# Cancel superseded runs for the same ref to save runner minutes. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +# Mirrors the GitLab `before_script` exports so the JavaSMT / Z3 native +# libraries are found at runtime. The paths are where apt installs libz3. +env: + JAVA_TOOL_OPTIONS: "-Djava.library.path=/usr/lib:/usr/lib/x86_64-linux-gnu:/usr/lib/x86_64-linux-gnu/jni" + LD_LIBRARY_PATH: "/usr/lib:/usr/lib/x86_64-linux-gnu:/usr/lib/x86_64-linux-gnu/jni" jobs: - build: + # --------------------------------------------------------------------------- + # stage: build + # --------------------------------------------------------------------------- + # GitLab `check` job. rules: merge_request_event only -> pull_request only. + checkstyle: + if: github.event_name == 'pull_request' runs-on: ubuntu-latest - permissions: - contents: read + steps: + - uses: actions/checkout@v4 + - name: Set up JDK 17 + uses: actions/setup-java@v4 + with: + java-version: '17' + distribution: 'temurin' + - name: Install Z3 native libraries + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends z3 libz3-dev libz3-java zip + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v4 + - name: Checkstyle + run: ./gradlew checkstyleMain checkstyleTest + # GitLab `compile-agent` / `compile-core` / `compile-integration-test`. + # No rules in GitLab -> runs on every pipeline (pushes and pull requests). + compile: + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + task: + - ":agent:compileJava" + - ":core:compileJava" + - ":integration-test:compileTestJava" steps: - - uses: actions/checkout@v4 - - name: Set up JDK 17 - uses: actions/setup-java@v4 - with: - java-version: '17' - distribution: 'temurin' + - uses: actions/checkout@v4 + - name: Set up JDK 17 + uses: actions/setup-java@v4 + with: + java-version: '17' + distribution: 'temurin' + - name: Install Z3 native libraries + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends z3 libz3-dev libz3-java zip + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v4 + - name: Compile ${{ matrix.task }} + run: ./gradlew ${{ matrix.task }} - # Configure Gradle for optimal use in GiHub Actions, including caching of downloaded dependencies. - # See: https://github.com/gradle/actions/blob/main/setup-gradle/README.md - - name: Setup Gradle - uses: gradle/actions/setup-gradle@417ae3ccd767c252f5661f1ace9f835f9654f2b5 # v3.1.0 + # --------------------------------------------------------------------------- + # stage: test + # --------------------------------------------------------------------------- - - name: Build with Gradle Wrapper - run: ./gradlew build + # GitLab `test` job. rules: merge_request_event only -> pull_request only. + test: + if: github.event_name == 'pull_request' + needs: [ checkstyle, compile ] + runs-on: ubuntu-latest + # Hard backstop above the in-script 3h budget (TOTAL_BUDGET below); the extra + # ~10 min lets the summary print and catches a wedged Gradle teardown. + timeout-minutes: 190 + steps: + - uses: actions/checkout@v4 + - name: Set up JDK 17 + uses: actions/setup-java@v4 + with: + java-version: '17' + distribution: 'temurin' + - name: Install Z3 native libraries + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends z3 libz3-dev libz3-java zip + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v4 + - name: Run JMC tests (one method per invocation) + run: | + set -eu + TEST_FILES=$(find integration-test/src/test/java -name "*Test.java" \ + -exec grep -l -E "^[[:space:]]*@JmcCheck|^[[:space:]]*@Test" {} + \ + | sort) + if [ -z "$TEST_FILES" ]; then + echo "No test classes found under integration-test/src/test/java." + exit 0 + fi + TEST_METHODS=$(for FILE in $TEST_FILES; do + CLASS_NAME=$(printf "%s" "$FILE" | sed 's|integration-test/src/test/java/||; s|/|.|g; s|\.java$||') + awk -v className="$CLASS_NAME" ' + BEGIN { in_block=0; want=0; disabled=0 } + { + line=$0 + if (in_block) { + if (line ~ /\*\//) { sub(/^.*\*\//, "", line); in_block=0 } else { next } + } + if (line ~ /\/\*/) { in_block=1; sub(/\/\*.*$/, "", line) } + sub(/^[[:space:]]+/, "", line) + if (line ~ /^\/\// || line == "") { next } + } + /^[[:space:]]*@Disabled/ { disabled=1; next } + /^[[:space:]]*@JmcCheck/ { want=1; next } + /^[[:space:]]*@Test/ { want=1; next } + want && $0 ~ /void[[:space:]]+[[:alnum:]_]+[[:space:]]*\(/ { + if (!disabled) { + line=$0 + sub(/^.*void[[:space:]]+/, "", line) + sub(/[[:space:]]*\(.*/, "", line) + print className "." line + } + want=0 + disabled=0 + } + ' "$FILE" + done) + if [ -z "$TEST_METHODS" ]; then + echo "No test methods found under integration-test/src/test/java." + exit 0 + fi + # Per-method wall-clock hang guard (default 600s = 10 min) plus an overall + # budget for the whole stage (default 10800s = 3h). Override via the + # PER_TEST_TIMEOUT / TOTAL_BUDGET environment variables on the job/workflow. + # A stuck test is killed (SIGTERM, then SIGKILL 30s later). Once the 3h + # budget is gone no further tests start, and a test near the boundary is + # capped so the stage stays within budget. Timed-out, failed, and + # budget-skipped tests are summarised at the end; the job fails if any test + # timed out or failed. + PER_TEST_TIMEOUT="${PER_TEST_TIMEOUT:-600}" + TOTAL_BUDGET="${TOTAL_BUDGET:-10800}" + TIMED_OUT="" + FAILED="" + NOT_RUN="" + # $SECONDS = elapsed wall-clock seconds since this shell started. + for TEST_METHOD in $TEST_METHODS; do + remaining=$(( TOTAL_BUDGET - SECONDS )) + if [ "$remaining" -le 0 ]; then + echo ">>> budget (${TOTAL_BUDGET}s) exhausted; not running: $TEST_METHOD" + NOT_RUN="${NOT_RUN}${NOT_RUN:+ }$TEST_METHOD" + continue + fi + this_to="$PER_TEST_TIMEOUT" + clamped=0 + if [ "$this_to" -gt "$remaining" ]; then + this_to="$remaining" + clamped=1 + fi + echo ">>> running $TEST_METHOD (timeout ${this_to}s; ${remaining}s left in budget)" + rc=0 + timeout -k 30s "${this_to}s" \ + ./gradlew --no-daemon :integration-test:test --tests "$TEST_METHOD" || rc=$? + if [ "$rc" -eq 124 ] || [ "$rc" -eq 137 ]; then + if [ "$clamped" -eq 1 ]; then + echo ">>> BUDGET CUTOFF (ran ${this_to}s, 3h budget reached): $TEST_METHOD" + NOT_RUN="${NOT_RUN}${NOT_RUN:+ }$TEST_METHOD" + else + echo ">>> TIMEOUT after ${this_to}s: $TEST_METHOD" + TIMED_OUT="${TIMED_OUT}${TIMED_OUT:+ }$TEST_METHOD" + fi + elif [ "$rc" -ne 0 ]; then + echo ">>> FAILED (exit $rc): $TEST_METHOD" + FAILED="${FAILED}${FAILED:+ }$TEST_METHOD" + fi + done + echo "===================== test summary (elapsed ${SECONDS}s) =====================" + if [ -n "$TIMED_OUT" ]; then + echo "Timed out (> ${PER_TEST_TIMEOUT}s):" + for t in $TIMED_OUT; do echo " - $t"; done + fi + if [ -n "$FAILED" ]; then + echo "Failed:" + for t in $FAILED; do echo " - $t"; done + fi + if [ -n "$NOT_RUN" ]; then + echo "Not run / cut short (3h budget):" + for t in $NOT_RUN; do echo " - $t"; done + fi + if [ -n "$TIMED_OUT" ] || [ -n "$FAILED" ]; then + exit 1 + fi + echo "All executed tests passed within ${PER_TEST_TIMEOUT}s each (total ${SECONDS}s)." + # GitLab `artifacts: reports: junit:` equivalent. + - name: Upload JUnit results + if: always() + uses: actions/upload-artifact@v4 + with: + name: junit-test-results + path: integration-test/build/test-results/test/**/TEST-*.xml + if-no-files-found: warn - # NOTE: The Gradle Wrapper is the default and recommended way to run Gradle (https://docs.gradle.org/current/userguide/gradle_wrapper.html). - # If your project does not have the Gradle Wrapper configured, you can use the following configuration to run Gradle with a specified version. - # - # - name: Setup Gradle - # uses: gradle/actions/setup-gradle@417ae3ccd767c252f5661f1ace9f835f9654f2b5 # v3.1.0 - # with: - # gradle-version: '8.5' - # - # - name: Build with Gradle 8.5 - # run: gradle build + # --------------------------------------------------------------------------- + # stage: deploy + # --------------------------------------------------------------------------- - dependency-submission: + # GitLab `publish` job. rules: $CI_COMMIT_BRANCH == "main" + # (extended to master so it also publishes from the GitLab default branch). + publish: + if: github.event_name == 'push' && (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/master') + needs: [ compile ] + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Set up JDK 17 + uses: actions/setup-java@v4 + with: + java-version: '17' + distribution: 'temurin' + - name: Install Z3 native libraries + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends z3 libz3-dev libz3-java zip + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v4 + - name: Publish + run: bash ./scripts/publish.sh + - name: Upload distribution archives + uses: actions/upload-artifact@v4 + with: + name: jmc-distributions + path: | + build/jmc-agent/jmc-agent.zip + build/jmc/jmc.zip + # Retained from the original GitHub starter workflow: generates and submits a + # dependency graph, enabling Dependabot alerts. Runs only on the main branches. + dependency-submission: + if: github.event_name == 'push' && (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/master') runs-on: ubuntu-latest permissions: contents: write - steps: - - uses: actions/checkout@v4 - - name: Set up JDK 17 - uses: actions/setup-java@v4 - with: - java-version: '17' - distribution: 'temurin' - - # Generates and submits a dependency graph, enabling Dependabot Alerts for all project dependencies. - # See: https://github.com/gradle/actions/blob/main/dependency-submission/README.md - - name: Generate and submit dependency graph - uses: gradle/actions/dependency-submission@417ae3ccd767c252f5661f1ace9f835f9654f2b5 # v3.1.0 + - uses: actions/checkout@v4 + - name: Set up JDK 17 + uses: actions/setup-java@v4 + with: + java-version: '17' + distribution: 'temurin' + - name: Generate and submit dependency graph + uses: gradle/actions/dependency-submission@v4 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a0acba75..ee6d0586 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -59,6 +59,9 @@ compile-integration-test: test: stage: test + # Hard backstop above the in-script 3h budget (TOTAL_BUDGET below); the extra + # ~10 min lets the summary print and catches a wedged Gradle teardown. + timeout: 3h 10m script: - | set -eu @@ -101,9 +104,66 @@ test: echo "No test methods found under integration-test/src/test/java." exit 0 fi + # Per-method wall-clock hang guard (default 600s = 10 min) plus an overall + # budget for the whole stage (default 10800s = 3h). Override with the + # PER_TEST_TIMEOUT / TOTAL_BUDGET CI/CD variables. A stuck test is killed + # (SIGTERM, then SIGKILL 30s later). Once the 3h budget is gone no further + # tests start, and a test near the boundary is capped so the stage stays + # within budget. Timed-out, failed, and budget-skipped tests are summarised + # at the end; the job fails if any test timed out or failed. + PER_TEST_TIMEOUT="${PER_TEST_TIMEOUT:-600}" + TOTAL_BUDGET="${TOTAL_BUDGET:-10800}" + TIMED_OUT="" + FAILED="" + NOT_RUN="" + # $SECONDS = elapsed wall-clock seconds since this shell started. for TEST_METHOD in $TEST_METHODS; do - ./gradlew --no-daemon :integration-test:test --tests "$TEST_METHOD" + remaining=$(( TOTAL_BUDGET - SECONDS )) + if [ "$remaining" -le 0 ]; then + echo ">>> budget (${TOTAL_BUDGET}s) exhausted; not running: $TEST_METHOD" + NOT_RUN="${NOT_RUN}${NOT_RUN:+ }$TEST_METHOD" + continue + fi + this_to="$PER_TEST_TIMEOUT" + clamped=0 + if [ "$this_to" -gt "$remaining" ]; then + this_to="$remaining" + clamped=1 + fi + echo ">>> running $TEST_METHOD (timeout ${this_to}s; ${remaining}s left in budget)" + rc=0 + timeout -k 30s "${this_to}s" \ + ./gradlew --no-daemon :integration-test:test --tests "$TEST_METHOD" || rc=$? + if [ "$rc" -eq 124 ] || [ "$rc" -eq 137 ]; then + if [ "$clamped" -eq 1 ]; then + echo ">>> BUDGET CUTOFF (ran ${this_to}s, 3h budget reached): $TEST_METHOD" + NOT_RUN="${NOT_RUN}${NOT_RUN:+ }$TEST_METHOD" + else + echo ">>> TIMEOUT after ${this_to}s: $TEST_METHOD" + TIMED_OUT="${TIMED_OUT}${TIMED_OUT:+ }$TEST_METHOD" + fi + elif [ "$rc" -ne 0 ]; then + echo ">>> FAILED (exit $rc): $TEST_METHOD" + FAILED="${FAILED}${FAILED:+ }$TEST_METHOD" + fi done + echo "===================== test summary (elapsed ${SECONDS}s) =====================" + if [ -n "$TIMED_OUT" ]; then + echo "Timed out (> ${PER_TEST_TIMEOUT}s):" + for t in $TIMED_OUT; do echo " - $t"; done + fi + if [ -n "$FAILED" ]; then + echo "Failed:" + for t in $FAILED; do echo " - $t"; done + fi + if [ -n "$NOT_RUN" ]; then + echo "Not run / cut short (3h budget):" + for t in $NOT_RUN; do echo " - $t"; done + fi + if [ -n "$TIMED_OUT" ] || [ -n "$FAILED" ]; then + exit 1 + fi + echo "All executed tests passed within ${PER_TEST_TIMEOUT}s each (total ${SECONDS}s)." cache: key: "$CI_COMMIT_REF_NAME" policy: push @@ -134,5 +194,5 @@ publish: - build/jmc-agent/jmc-agent.zip - build/jmc/jmc.zip rules: - - if: $CI_COMMIT_BRANCH == "main" + - if: $CI_COMMIT_BRANCH == "main" || $CI_COMMIT_BRANCH == "master" when: on_success \ No newline at end of file diff --git a/README.md b/README.md index ff83648c..36cf7968 100644 --- a/README.md +++ b/README.md @@ -75,9 +75,39 @@ The `random` strategy explores thread interleavings with a randomized approach, `random` is the default strategy in `JmcCheckConfiguration`, so you do not need to specify it explicitly. +#### PCT + +The `pct` strategy implements Probabilistic Concurrency Testing (PCT) [5], a randomized, priority-based scheduler that provides a probabilistic guarantee of finding a bug in every run. Unlike `random`, which makes a fresh random choice at every scheduling point, PCT randomizes sparingly: it assigns each thread a random priority and always runs the enabled thread with the highest priority, inserting only a small number of random priority-change points at which it demotes the running thread to force a preemption. + +PCT characterizes a bug by its *depth* `d`, the minimum number of ordering constraints between instructions required to trigger it. Many common concurrency bugs have a small depth: ordering errors are typically depth 1, while atomicity violations and circular-lock deadlocks are typically depth 2. For a program that runs at most `n` threads and `k` scheduling steps, a single run of PCT finds a bug of depth `d` with probability at least `1 / (n · k^(d-1))`. Running more iterations increases the probability of finding the bug to any desired level. + +You select the target depth with the `bugDepth` parameter (default `3`); PCT then places `d - 1` priority-change points. The step bound `k` is learned automatically across iterations, so you do not need to provide it. To use the `pct` strategy, specify it in the `JmcCheckConfiguration` annotation: + +```java +@JmcCheck +@JmcCheckConfiguration(numIterations = 100, strategy = "pct", bugDepth = 2) +void testCounter() { + // ... same code as above +} +``` + +#### Fair-PCT + +The `fair-pct` strategy is a fair variant of `pct`. Because pure PCT is a strict priority scheduler, a high-priority thread that busy-waits on a value produced by a lower-priority thread can starve it and prevent the run from terminating. To guarantee progress, `fair-pct` schedules with PCT priorities for a bounded prefix of each run and then switches to uniform-random ("fair") scheduling for the remainder. This preserves PCT's bug-finding ability over the prefix while ensuring the run makes progress. + +The switch point is controlled by the `pctFairBound` parameter. A positive value sets an explicit number of priority-controlled scheduling decisions before the switch; the default (`0`) selects automatic mode, in which the bound is the largest number of decisions seen in any previous run, so that only an abnormally long run — the signature of a spin-loop livelock — switches to the fair suffix. To use the `fair-pct` strategy, specify it in the `JmcCheckConfiguration` annotation: + +```java +@JmcCheck +@JmcCheckConfiguration(numIterations = 100, strategy = "fair-pct", bugDepth = 2) +void testCounter() { + // ... same code as above +} +``` + ### Systematic Exploration -The `systematic` strategy explores all of the necessary and sufficient interleavings to find every existing bug. It uses dynamic partial-order reduction (DPOR) to reduce the exhaustive search space to a minimal set of interleavings, none of which is equivalent to another, and thus guarantees that all bugs are found. Expect a longer execution time than with `random`, especially for tests with a large state space. +The `systematic` strategy explores all the necessary and sufficient interleavings to find every existing bug. It uses dynamic partial-order reduction (DPOR) to reduce the exhaustive search space to a minimal set of interleavings, none of which is equivalent to another, and thus guarantees that all bugs are found. Expect a longer execution time than with `random`, especially for tests with a large state space. #### Trust @@ -324,6 +354,8 @@ See the [User Guide](https://jmc.mpi-sws.org/user_guide/) for a comprehensive in [4] A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, and Minjian Zhang. "State Space Estimation for DPOR-based Model Checkers." arXiv e-prints (2025): arXiv-2512. +[5] Sebastian Burckhardt, Pravesh Kothari, Madanlal Musuvathi, and Santosh Nagarakatte. "A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs." In Proceedings of the 15th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2010), pp. 167–178. + ## License Apache License 2.0 \ No newline at end of file diff --git a/core/src/main/java/org/mpi_sws/jmc/annotations/JmcCheckConfiguration.java b/core/src/main/java/org/mpi_sws/jmc/annotations/JmcCheckConfiguration.java index 7dd2c309..a1d98c74 100644 --- a/core/src/main/java/org/mpi_sws/jmc/annotations/JmcCheckConfiguration.java +++ b/core/src/main/java/org/mpi_sws/jmc/annotations/JmcCheckConfiguration.java @@ -23,6 +23,10 @@ * * * @@ -71,5 +75,29 @@ int budget() default 2; + /** + * The target bug depth {@code d} for the PCT strategies (pct, fair-pct). + * + *

PCT installs {@code d - 1} priority change points and finds a bug of depth {@code d} with + * probability at least {@code 1 / (n * k^(d-1))} per iteration. Must be at least 1; the default + * (3) targets bugs of depth up to 3. Ignored by non-PCT strategies. + * + * @return the target bug depth + */ + int bugDepth() default 3; + + /** + * The fair-suffix bound for the fair-pct strategy: the number of priority-controlled + * scheduling decisions before switching to a uniform-random ("fair") suffix. + * + *

A value {@code <= 0} (the default) selects automatic mode, in which the bound for each + * iteration is the largest number of decisions seen in any previous run — so normal-length runs + * stay entirely under PCT and only an abnormally long run (a spin-loop livelock) switches to the + * fair suffix. Ignored by strategies other than fair-pct. + * + * @return the fair-suffix bound, or a non-positive value for automatic mode + */ + int pctFairBound() default 0; + long timeout() default -1L; } diff --git a/core/src/main/java/org/mpi_sws/jmc/checker/JmcCheckerConfiguration.java b/core/src/main/java/org/mpi_sws/jmc/checker/JmcCheckerConfiguration.java index 16b8906c..251abdf5 100644 --- a/core/src/main/java/org/mpi_sws/jmc/checker/JmcCheckerConfiguration.java +++ b/core/src/main/java/org/mpi_sws/jmc/checker/JmcCheckerConfiguration.java @@ -37,6 +37,10 @@ public class JmcCheckerConfiguration { private int budget; + private int bugDepth; + + private int pctFairBound; + private String reportPath; private Duration timeout; @@ -99,6 +103,24 @@ public int getBudget() { return budget; } + /** + * Returns the target bug depth {@code d} used by the PCT strategies. + * + * @return the bug depth + */ + public int getBugDepth() { + return bugDepth; + } + + /** + * Returns the fair-suffix bound used by the {@code fair-pct} strategy. + * + * @return the fair bound; a value {@code <= 0} means automatic mode + */ + public int getPctFairBound() { + return pctFairBound; + } + /** * Sets the seed for the checker. * @@ -143,7 +165,13 @@ public TrustStrategy.SchedulingPolicy getSchedulingPolicy() { public JmcRuntimeConfiguration toRuntimeConfiguration() throws JmcInvalidStrategyException { SchedulingStrategy strategy; SchedulingStrategyConfiguration.Builder strategyConfigurationBuilder = - new SchedulingStrategyConfiguration.Builder().seed(seed).budget(budget).solver(solver).trustSchedulingPolicy(schedulingPolicy); + new SchedulingStrategyConfiguration.Builder() + .seed(seed) + .budget(budget) + .solver(solver) + .trustSchedulingPolicy(schedulingPolicy) + .bugDepth(bugDepth) + .pctFairBound(pctFairBound); if (debug) { strategyConfigurationBuilder.debug(); strategyConfigurationBuilder.reportPath(reportPath); @@ -185,6 +213,8 @@ public static JmcCheckerConfiguration fromAnnotation(JmcCheckConfiguration annot .reportPath(annotation.reportPath()) .seed(annotation.seed()) .budget(annotation.budget()) + .bugDepth(annotation.bugDepth()) + .pctFairBound(annotation.pctFairBound()) .timeout(annotation.timeout()) .schedulingPolicy(annotation.schedulingPolicy()) .build(); @@ -212,6 +242,10 @@ public static class Builder { private int budget; + private int bugDepth; + + private int pctFairBound; + private TrustStrategy.SchedulingPolicy schedulingPolicy; public Builder() { @@ -223,6 +257,8 @@ public Builder() { this.solver = "off"; this.seed = System.nanoTime(); this.budget = 2; + this.bugDepth = 3; + this.pctFairBound = 0; this.timeout = null; } @@ -267,6 +303,16 @@ public Builder budget(int budget) { return this; } + public Builder bugDepth(int bugDepth) { + this.bugDepth = bugDepth; + return this; + } + + public Builder pctFairBound(int pctFairBound) { + this.pctFairBound = pctFairBound; + return this; + } + public Builder timeout(Duration timeout) { this.timeout = timeout; return this; @@ -301,6 +347,8 @@ public JmcCheckerConfiguration build() throws JmcInvalidConfigurationException { config.solver = solver; config.seed = seed; config.budget = budget; + config.bugDepth = bugDepth; + config.pctFairBound = pctFairBound; config.timeout = timeout; config.schedulingPolicy = schedulingPolicy; return config; diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/HaltCheckerException.java b/core/src/main/java/org/mpi_sws/jmc/runtime/HaltCheckerException.java index 87e03ea4..687aefdb 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/HaltCheckerException.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/HaltCheckerException.java @@ -2,15 +2,31 @@ /** Exception thrown to halt execution of the current and all subsequent executions. */ public class HaltCheckerException extends RuntimeException { + /** Whether the exploration stopped successfully without any error. */ private boolean okay = false; + /** Whether the exploration was halted because of a timeout. */ private boolean timeout = false; + /** + * Constructs a new {@link HaltCheckerException} with explicit success and timeout flags. + * + * @param ok whether the exploration stopped successfully + * @param message the exception message + * @param timeout whether the exploration was halted due to a timeout + */ private HaltCheckerException(boolean ok, String message, boolean timeout) { super(message); this.okay = ok; this.timeout = timeout; } + /** + * Constructs a new {@link HaltCheckerException} from an error message and cause. The success and + * timeout flags are both set to {@code false}. + * + * @param message the error message + * @param cause the underlying cause + */ private HaltCheckerException(String message, Throwable cause) { super(message, cause); this.okay = false; diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/HaltExecutionException.java b/core/src/main/java/org/mpi_sws/jmc/runtime/HaltExecutionException.java index b97308dc..2b528bf3 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/HaltExecutionException.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/HaltExecutionException.java @@ -5,6 +5,7 @@ */ public class HaltExecutionException extends RuntimeException { + /** The reason this execution was halted. */ private final Type type; /** @@ -29,27 +30,49 @@ public static HaltExecutionException ok() { return new HaltExecutionException(Type.ALL_OK, "All OK"); } + /** + * Constructs a new {@link HaltExecutionException} signalling that the current iteration must be + * discarded and re-executed. + * + * @return the re-execution exception + */ public static HaltExecutionException reexecutionNeeded() { return new HaltExecutionException(Type.REEXECTION_NEEDED, "Re-execution needed"); } + /** + * Returns whether this exception requests re-execution of the current iteration. + * + * @return {@code true} if the type is {@link Type#REEXECTION_NEEDED} + */ public boolean isReexecutionNeeded() { return type == Type.REEXECTION_NEEDED; } + /** + * Returns the reason this execution was halted. + * + * @return the halt {@link Type} + */ public Type getType() { return type; } /** - * Exception type when the model checker stops the execution. + * The reason the model checker stopped the current execution (iteration). */ public enum Type { + /** The program under test raised an error. */ PROGRAM_ERROR, + /** A consistency (memory model) violation was detected. */ CONSISTENCY_VIOLATION, + /** A deadlock was detected. */ DEADLOCK, + /** A race condition was detected. */ RACE_CONDITION, + /** The current iteration must be discarded and re-executed. */ REEXECTION_NEEDED, + /** The execution completed without any error. */ ALL_OK, } } diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/HaltTaskException.java b/core/src/main/java/org/mpi_sws/jmc/runtime/HaltTaskException.java index 26c266f1..15242923 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/HaltTaskException.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/HaltTaskException.java @@ -6,15 +6,17 @@ */ public class HaltTaskException extends RuntimeException { - // The ID of the task that threw the exception. + /** The ID of the task that should be halted. */ private final Long taskId; + /** The reason the task is being halted. */ private final Type type; /** * Constructs a new HaltTaskException object. * * @param taskId the ID of the task that threw the exception + * @param type the reason the task is being halted */ public HaltTaskException(Long taskId, Type type) { super(); @@ -22,18 +24,41 @@ public HaltTaskException(Long taskId, Type type) { this.type = type; } + /** + * Creates a {@link HaltTaskException} for the given task with the given reason. + * + * @param taskId the ID of the task to halt + * @param type the reason the task is being halted + * @return the new exception + */ public static HaltTaskException error(Long taskId, Type type) { return new HaltTaskException(taskId, type); } + /** + * Creates a {@link HaltTaskException} indicating the task is blocked. + * + * @param taskId the ID of the blocked task + * @return the new exception of type {@link Type#BLOCKED} + */ public static HaltTaskException blocked(Long taskId) { return new HaltTaskException(taskId, Type.BLOCKED); } + /** + * Returns whether this exception indicates the task is blocked. + * + * @return {@code true} if the type is {@link Type#BLOCKED} + */ public boolean isBlocked() { return type == Type.BLOCKED; } + /** + * Returns whether this exception indicates a task error. + * + * @return {@code true} if the type is {@link Type#TASK_ERROR} + */ public boolean isTaskError() { return type == Type.TASK_ERROR; } @@ -48,10 +73,12 @@ public Long getTaskId() { } /** - * Exception type when the model checker stops a task. + * The reason the model checker stops a task. */ public enum Type { + /** The task raised an error and must be halted. */ TASK_ERROR, + /** The task is blocked (cannot make progress) and must be halted. */ BLOCKED } } diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntime.java b/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntime.java index 1d40881e..2c23760d 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntime.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntime.java @@ -25,19 +25,39 @@ * *

Calls to the runtime are made by the instrumented byte code. These calls are used to record * events occurring during the execution of tasks or allow for scheduling changes. For example, the - * runtime can be used to record Thread creation and deletion. + * runtime can be used to record thread creation and deletion. * *

The runtime is a static class that stores minimal states and delegates calls to the {@link * Scheduler} which retains all the state. */ public class JmcRuntime { + /** Logger used to trace runtime setup, task switching, and event handling. */ private static final Logger LOGGER = LogManager.getLogger(JmcRuntime.class); + /** + * Owns all per-task state (state machine and pausing futures). + * + *

Created once and reused across iterations; reset by {@link #resetIteration(int)} and {@link + * #tearDown(JmcModelCheckerReport)}. + */ private static final TaskManager taskManager = new TaskManager(); + /** + * The scheduler that owns the scheduler thread and the configured {@link SchedulingStrategy}. + * + *

Instantiated in {@link #setup(JmcRuntimeConfiguration)} or {@link + * #setupReplay(JmcRuntimeConfiguration)} and shut down in {@link + * #tearDown(JmcModelCheckerReport)}. + */ private static Scheduler scheduler; + /** + * The active runtime configuration. + * + *

Set during setup and read by {@link #initIteration(int, JmcModelCheckerReport)} to configure + * the scheduler and the strategy. + */ private static JmcRuntimeConfiguration config; /** @@ -56,6 +76,17 @@ public static void setup(JmcRuntimeConfiguration config) { scheduler.start(); } + /** + * Sets up the runtime to replay a previously recorded schedule. + * + *

The configured strategy must implement {@link ReplayableSchedulingStrategy}; otherwise a + * {@link JmcReplayUnsupported} exception is thrown. The recorded trace is loaded via {@link + * ReplayableSchedulingStrategy#replayRecordedTrace()} before the scheduler is created and + * started. + * + * @param config the configuration (instance of {@link JmcRuntimeConfiguration}) + * @throws JmcCheckerException if the strategy does not support replay + */ public static void setupReplay(JmcRuntimeConfiguration config) throws JmcCheckerException { LOGGER.debug("Setting up for replay!"); JmcRuntime.config = config; @@ -75,7 +106,11 @@ public static void setupReplay(JmcRuntimeConfiguration config) throws JmcChecker } /** - * Tears down the runtime by shutting down the scheduler adn clearing the task manager. + * Tears down the runtime by clearing the task manager and shutting down the scheduler. + * + *

Called once after all iterations are complete. + * + * @param report the report passed to the strategy teardown via the scheduler */ public static void tearDown(JmcModelCheckerReport report) { LOGGER.debug("Tearing down!"); @@ -83,6 +118,15 @@ public static void tearDown(JmcModelCheckerReport report) { scheduler.shutdown(report); } + /** + * Reconfigures log4j to write runtime logs to a per-iteration file. + * + *

The file is named {@code jmc-runtime-.log} under the configured report path. + * Only invoked from {@link #initIteration(int, JmcModelCheckerReport)} when debug logging is + * enabled. + * + * @param iteration the iteration number, used in the log file name + */ private static void updateLoggerFile(int iteration) { String fileName = config.getReportPath() + "/jmc-runtime-" + iteration + ".log"; ConfigurationBuilder builder = @@ -103,11 +147,16 @@ private static void updateLoggerFile(int iteration) { } /** - * Initializes the runtime with the main thread for a given iteration. + * Initializes the runtime for a given iteration and starts the main task. * - *

Initializes the scheduler with the main thread and marks it as ready. + *

When debug logging is enabled, redirects logs to a per-iteration file. Initializes the + * strategy for the iteration, creates the main task (marking it {@link + * TaskManager.TaskState#BLOCKED}), binds the scheduler to the task manager, emits the {@link + * JmcRuntimeEvent.Type#START_EVENT} for the main task, and yields control to the scheduler. From + * the second iteration onward, re-invokes the static initializers of instrumented classes. * * @param iteration the iteration number + * @param report the model checker report, forwarded to the strategy via the scheduler */ public static void initIteration(int iteration, JmcModelCheckerReport report) { if (config.getDebug()) { @@ -137,7 +186,12 @@ public static void initIteration(int iteration, JmcModelCheckerReport report) { } /** - * Resets the runtime for a new iteration. + * Resets the runtime at the end of an iteration. + * + *

Resets the strategy, clears the task manager, and clears the synchronized-method/-block + * lock store so the next iteration starts from a clean state. + * + * @param iteration the iteration number being reset */ public static void resetIteration(int iteration) { scheduler.resetIteration(iteration); @@ -145,13 +199,23 @@ public static void resetIteration(int iteration) { JmcRuntimeUtils.clearSyncLocks(); } + /** + * Records the current schedule via the scheduler. + * + *

Effective only when the configured strategy is replayable; used to persist a buggy + * schedule for later replay. + */ public static void recordTrace() { scheduler.recordTrace(); } /** - * Pauses the current task that invokes this method and yields the control to the scheduler. The + * Pauses the current task that invokes this method and yields control to the scheduler. The * call returns only when the task that invoked this method is resumed. + * + * @param the type of the value delivered when the task is resumed + * @return the value the scheduler attached when resuming the task (used for reactive events such + * as a strategy-provided random value or a symbolic result); may be {@code null} */ public static T yield() { Long currentTask = scheduler.currentTask(); @@ -199,6 +263,17 @@ public static void pause(Long taskId) { } } + /** + * Blocks until the task with the given ID is resumed and returns the delivered value. + * + *

Delegates to {@link TaskManager#wait(Long)}. If re-execution of the iteration is requested, + * a {@link HaltExecutionException#reexecutionNeeded()} is propagated; any other failure is + * rethrown as a {@link HaltExecutionException} error. + * + * @param the type of the value delivered when the task is resumed + * @param taskId the ID of the task to wait on + * @return the value delivered when the task is resumed; may be {@code null} + */ public static T wait(Long taskId) { try { return taskManager.wait(taskId); diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeConfiguration.java b/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeConfiguration.java index 26b92143..4e1dc673 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeConfiguration.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeConfiguration.java @@ -18,45 +18,91 @@ */ public class JmcRuntimeConfiguration { + /** The scheduling strategy that drives the run. */ private SchedulingStrategy strategy; + /** Whether debug logging (including per-iteration log files) is enabled. */ private Boolean debug; + /** Directory where logs and trace artifacts are written. */ private String reportPath; + /** + * Number of times the scheduler thread retries {@code strategy.nextTask()} before giving up when + * no task is runnable yet. + */ private int schedulerTries = 10; + /** Sleep, in nanoseconds, between scheduler retries. */ private long schedulerTrySleepTimeNanos = 100; + /** Private constructor; instances are created through {@link Builder}. */ private JmcRuntimeConfiguration() {} + /** + * Returns the configured scheduling strategy. + * + * @return the scheduling strategy + */ public SchedulingStrategy getStrategy() { return strategy; } + /** + * Returns whether debug logging is enabled. + * + * @return {@code true} if debug logging is enabled + */ public Boolean getDebug() { return debug; } + /** + * Returns the report output directory. + * + * @return the report path + */ public String getReportPath() { return reportPath; } + /** + * Returns the scheduler retry count. + * + * @return the number of scheduler retries + */ public int getSchedulerTries() { return schedulerTries; } + /** + * Returns the sleep between scheduler retries. + * + * @return the scheduler retry sleep time in nanoseconds + */ public long getSchedulerTrySleepTimeNanos() { return schedulerTrySleepTimeNanos; } + /** + * Builder for {@link JmcRuntimeConfiguration}. + * + *

All values are seeded with defaults (a random scheduling strategy, debug off, the default + * report path, 10 scheduler tries, and a 100ns retry sleep) and can be overridden fluently. + */ public static class Builder { + /** The scheduling strategy to build with. */ private SchedulingStrategy strategy; + /** The debug flag to build with. */ private Boolean debug; + /** The report path to build with. */ private String reportPath; + /** The scheduler retry count to build with. */ private int schedulerTries; + /** The scheduler retry sleep (ns) to build with. */ private long schedulerTrySleepTimeNanos; + /** Creates a builder pre-populated with the default configuration values. */ public Builder() { this.strategy = new RandomSchedulingStrategy( @@ -67,31 +113,66 @@ public Builder() { this.schedulerTrySleepTimeNanos = 100; } + /** + * Sets the scheduling strategy. + * + * @param strategy the scheduling strategy + * @return this builder, for chaining + */ public Builder strategy(SchedulingStrategy strategy) { this.strategy = strategy; return this; } + /** + * Sets the debug flag. + * + * @param debug whether debug logging is enabled + * @return this builder, for chaining + */ public Builder debug(Boolean debug) { this.debug = debug; return this; } + /** + * Sets the report output directory. + * + * @param reportPath the report path + * @return this builder, for chaining + */ public Builder reportPath(String reportPath) { this.reportPath = reportPath; return this; } + /** + * Sets the scheduler retry count. + * + * @param schedulerTries the number of scheduler retries + * @return this builder, for chaining + */ public Builder schedulerTries(int schedulerTries) { this.schedulerTries = schedulerTries; return this; } + /** + * Sets the sleep between scheduler retries. + * + * @param schedulerTrySleepTimeNanos the retry sleep time in nanoseconds + * @return this builder, for chaining + */ public Builder schedulerTrySleepTimeNanos(long schedulerTrySleepTimeNanos) { this.schedulerTrySleepTimeNanos = schedulerTrySleepTimeNanos; return this; } + /** + * Builds an immutable {@link JmcRuntimeConfiguration} from the configured values. + * + * @return a new {@link JmcRuntimeConfiguration} instance + */ public JmcRuntimeConfiguration build() { JmcRuntimeConfiguration config = new JmcRuntimeConfiguration(); config.strategy = strategy; diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeEvent.java b/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeEvent.java index 3f0ecd06..35c7cee8 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeEvent.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeEvent.java @@ -6,16 +6,24 @@ import static org.mpi_sws.jmc.api.JmcObject.handleToString; /** - * Represents an event that occurs during the execution of a program. + * Represents an event that occurs during the execution of an instrumented program. + * + *

An event marks an interesting point in a task's execution at which a scheduling decision can + * be made (e.g. thread start/finish, lock acquire/release, field read/write, wait/notify). Events + * are typically reported to the runtime via {@link JmcRuntime#updateEvent(JmcRuntimeEvent)} just + * before a {@link JmcRuntime#yield()} and are forwarded to the scheduling strategy. + * + *

Each event carries a {@link Type}, the ID of the originating task, and an arbitrary map of + * parameters. Instances are usually built with the fluent {@link Builder}. */ public class JmcRuntimeEvent { - // The type of the event + /** The type of the event. */ private Type type; - // The ID of the task that generated the event + /** The ID of the task that generated the event. */ private Long taskId; - // The parameters of the event + /** The additional parameters of the event, keyed by name. */ private Map params; /** @@ -110,17 +118,29 @@ public void setParam(String key, Object value) { } /** - * Returns the value of the parameter with the specified key as an object of the specified - * class. + * Returns the value of the parameter with the specified key, cast to the caller's expected type. * + *

The cast is unchecked; a {@link ClassCastException} may be thrown at the call site if the + * stored value is not of the expected type. + * + * @param the expected type of the parameter value * @param key the key of the parameter - * @return the value of the parameter as an object of the specified class. Can throw an - * exception when casting. + * @return the value of the parameter, or {@code null} if no such parameter exists */ public T getParam(String key) { return (T) params.get(key); } + /** + * Renders the parameter map into a human-readable string for {@link #toString()}. + * + *

The {@code "instance"} parameter is rendered via {@code handleToString} so that + * instrumented object handles print meaningfully; all other values use their own + * {@code toString}. + * + * @param params the parameter map to render (may be {@code null}) + * @return a comma-separated string of the parameter values, or an empty string if {@code null} + */ private String paramToString(Map params) { if (params == null) return ""; StringBuilder sb = new StringBuilder(); @@ -138,6 +158,12 @@ private String paramToString(Map params) { return sb.toString(); } + /** + * Returns a human-readable representation of this event, including its type, task ID, and + * rendered parameters. Used for debug logging of events. + * + * @return a string representation of this event + */ @Override public String toString() { return "RuntimeEvent{" + "type=" + type + ", taskId=" + taskId + ", params=" + paramToString(params) + '}'; @@ -147,12 +173,18 @@ public String toString() { * A builder for constructing a {@link JmcRuntimeEvent} object. */ public static class Builder { + /** The event type to build with. */ private Type type; + /** The originating task ID to build with. */ private Long taskId; + /** The accumulated event parameters; lazily created by {@link #param(String, Object)}. */ private Map params; /** * Sets the type of the event. + * + * @param type the type of the event + * @return this builder, for chaining */ public Builder type(Type type) { this.type = type; @@ -161,6 +193,9 @@ public Builder type(Type type) { /** * Sets the ID of the task that generated the event. + * + * @param taskId the ID of the originating task + * @return this builder, for chaining */ public Builder taskId(Long taskId) { this.taskId = taskId; @@ -168,7 +203,10 @@ public Builder taskId(Long taskId) { } /** - * Sets the parameters of the event. + * Sets the full parameter map of the event, replacing any parameters added so far. + * + * @param params the parameter map + * @return this builder, for chaining */ public Builder params(Map params) { this.params = params; @@ -176,7 +214,11 @@ public Builder params(Map params) { } /** - * Adds a parameter to the event. + * Adds a single parameter to the event, creating the parameter map if necessary. + * + * @param key the parameter key + * @param value the parameter value + * @return this builder, for chaining */ public Builder param(String key, Object value) { if (params == null) { @@ -187,7 +229,9 @@ public Builder param(String key, Object value) { } /** - * Builds the {@link JmcRuntimeEvent} object. + * Builds the {@link JmcRuntimeEvent} from the configured type, task ID, and parameters. + * + * @return a new {@link JmcRuntimeEvent} instance */ public JmcRuntimeEvent build() { return new JmcRuntimeEvent(type, taskId, params); @@ -200,6 +244,7 @@ public JmcRuntimeEvent build() { *

Each event type corresponds to a specific action or occurrence in the program's execution, * such as thread creation, locking, reading, writing, and more. */ + // TODO :: Refactor this enum public enum Type { // Thread creation and termination events START_EVENT, @@ -242,7 +287,6 @@ public enum Type { FUTURE_EXCEPTION_EVENT, FUTURE_SET_EVENT, - // TODO: explain TAKE_WORK_QUEUE, CON_ASSUME_EVENT, SYM_ASSUME_EVENT, diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeUtils.java b/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeUtils.java index 5663c685..a2d1cb8c 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeUtils.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeUtils.java @@ -25,18 +25,37 @@ * and is not intended for direct use within the codebase. */ public class JmcRuntimeUtils { + /** Logger used to trace utility operations (static-init invocation, executor registration). */ private static final Logger LOGGER = LogManager.getLogger(JmcRuntimeUtils.class); + /** + * Store of {@link JmcReentrantLock}s backing instrumented {@code synchronized} methods and + * blocks, keyed by the hash code of the locked instance or class name. + */ private static final JmcSyncLocksStore syncMethodLocksStore = new JmcSyncLocksStore(); // TODO: check if we need to change the type of the list here + /** Instrumented classes with a non-empty static initializer, in registration order. */ private static final List> staticInitializedClassesList = new ArrayList<>(); + /** Names of the registered static-initialized classes, used to deduplicate registrations. */ private static final Set staticInitializedClasses = new HashSet<>(); + /** Private constructor to prevent instantiation of this utility class. */ private JmcRuntimeUtils() { // Private constructor to prevent instantiation } + /** + * Reports a symbolic boolean event and returns the concrete boolean decided by the strategy. + * + *

Emits a {@link JmcRuntimeEvent.Type#SYMBOLIC_EVENT} carrying the given boolean formula and + * yields; the strategy resumes the task with a {@link PrimitiveValue}. Throws a {@link + * RuntimeException} if the result is not a {@link PrimitiveValue}, and a {@link + * ClassCastException} (from {@link PrimitiveValue#asBoolean()}) if it is not a boolean. + * + * @param formula the symbolic boolean formula to evaluate + * @return the boolean value chosen by the strategy for this formula + */ public static boolean SymEvent(JmcBooleanFormula formula) { JmcRuntimeEvent event = new JmcRuntimeEvent.Builder() @@ -428,13 +447,20 @@ public static void clearSyncLocks() { syncMethodLocksStore.clear(); } + /** + * Maps instance/class-name hash codes to the {@link JmcReentrantLock}s that back instrumented + * {@code synchronized} methods and blocks. + */ private static class JmcSyncLocksStore { + /** The hash-code-to-lock map. */ private final Map lockMap; + /** Constructs an empty lock store. */ public JmcSyncLocksStore() { lockMap = new HashMap<>(); } + /** Removes all registered locks. */ public void clear() { lockMap.clear(); } @@ -475,6 +501,15 @@ public void registerLock(int hashcode) { } } + /** + * Registers an instrumented class that has a static initializer. + * + *

Registration is idempotent (deduplicated by class name). Registered classes have their + * synthetic static initializer re-invoked at the start of subsequent iterations by {@link + * #invokeStaticInitializedClasses(int)}. + * + * @param clazz the instrumented class to register + */ public static void registerStaticInitializedClass(Class clazz) { if (!staticInitializedClasses.contains(clazz.getName())) { LOGGER.debug("Static classes registered are : {}", clazz.getName()); @@ -484,6 +519,16 @@ public static void registerStaticInitializedClass(Class clazz) { } } + /** + * Rewrites a compiled-class URL to point at the corresponding instrumented class location. + * + *

Maps {@code build/classes/java/{main,test}/} paths to {@code build/generated/instrumented/}. + * On any failure the original URL is returned. Used only by the (currently disabled) + * class-reloading path. + * + * @param url the original class URL + * @return the rewritten URL, or the original URL if rewriting fails + */ private static URL renameClassURL(URL url) { String urlString = url.toString(); urlString = urlString.replace("build/classes/java/main/", "build/generated/instrumented/"); @@ -523,6 +568,14 @@ private static URL renameClassURL(URL url) { // } // } + /** + * Invokes the synthetic {@code $staticInitExplicit} method on every registered static-initialized + * class. + * + *

Iterates over a snapshot of the registered classes and reflectively calls the generated + * static-init method on each, logging (but not propagating) reflective invocation failures. + * Called by {@link #invokeStaticInitializedClasses(int)}. + */ private static void invokeInstrumentedStaticMethod() { if (staticInitializedClasses.isEmpty()) { LOGGER.debug("No static initialized classes to invoke."); @@ -553,21 +606,42 @@ private static void invokeInstrumentedStaticMethod() { /** - * Invokes static initializer of the instrumented classes. + * Invokes the static initializers of all registered instrumented classes. * - *

The instrumentation introduces a special method `$staticInit` for each class that has a - * non-empty static initializer. Here we invoke that method. + *

The instrumentation introduces a synthetic {@code $staticInitExplicit} method for each class + * that has a non-empty static initializer; this method invokes it on every registered class (via + * {@link #invokeInstrumentedStaticMethod()}) so static state is re-established deterministically + * in later iterations. + * + * @param iteration the current iteration number (the static initializers are re-run from the + * second iteration onward) */ public static void invokeStaticInitializedClasses(int iteration) { // reloadStaticInitializedClasses(); invokeInstrumentedStaticMethod(); } + /** + * Class loader used by the (currently disabled) approach to reload instrumented classes and + * re-trigger their static initializers. Retained for reference; not used by the active code + * path. + */ private static class ReloadingClassLoader extends URLClassLoader { + /** + * Creates a reloading class loader over the given URLs with no parent. + * + * @param urls the URLs to load classes from + */ public ReloadingClassLoader(URL[] urls) { super(urls, null); } + /** + * Loads (reloads) the class with the given name through this loader. + * + * @param className the fully qualified class name to reload + * @throws ClassNotFoundException if the class cannot be found + */ public void reloadClass(String className) throws ClassNotFoundException { // TODO: this is not working. Need to figure out why? // This method is used to reload a class by its name @@ -580,9 +654,6 @@ public void reloadClass(String className) throws ClassNotFoundException { } } - - // Add these methods to JmcRuntimeUtils class: - /** * Creates a start static init event without yielding. * This marks the beginning of static initialization for a class. diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/TaskManager.java b/core/src/main/java/org/mpi_sws/jmc/runtime/TaskManager.java index 76f3849c..7245b0e5 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/TaskManager.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/TaskManager.java @@ -12,41 +12,57 @@ import java.util.concurrent.locks.ReentrantLock; /** - * Encapsulates all the operations related to Task objects used by the runtime Except the - * SchedulerTask The encapsulation ensures no memory leak when creating many tasks. + * Owns all per-task state used by the runtime (except the scheduler thread itself). + * + *

A task is any concurrent computation managed by JMC (a thread, a future, an executor + * task, ...). For each task this class tracks its {@link TaskState} and, while the task is paused, + * the {@link CompletableFuture} it is blocked on. Resuming a task amounts to completing that future, + * optionally with a value. + * + *

Centralizing task ownership here ensures futures are completed and dropped consistently, + * avoiding memory leaks when many tasks are created. Used by {@link JmcRuntime} and by the {@code + * Scheduler} (via the runtime) to pause, resume, block, and terminate tasks. */ public class TaskManager { + /** Logger used to trace task resume failures and the "stop all" path. */ private static final Logger LOGGER = LogManager.getLogger(TaskManager.class); /** - * The state of each task managed by the @RuntimeEnvironment is represented by one of the - * following. + * The lifecycle state of a task managed by the {@link TaskManager}. */ public enum TaskState { + /** The task is currently executing (it has been resumed by the scheduler). */ RUNNING, + /** The task is paused, waiting on its future to be completed. */ BLOCKED, + /** The task has been allocated an ID but has not started running yet. */ CREATED, + /** The task has finished (or been terminated) and will not run again. */ TERMINATED, } /** - * Stores a set of custom IDs used by the Runtime. + * Monotonic counter for the next task ID to assign. Starts at 1 (the main task) and is handed + * out by {@link #nextTaskId()}. Guarded by {@link #idCounterLock}. */ private Long idCounter; + /** Lock guarding {@link #idCounter}. */ private final Object idCounterLock = new Object(); /** - * Stores the state of each task. + * Maps each task ID to its current {@link TaskState}. Guarded by {@link #tasksLock}. */ private final Map taskStates; /** - * Stores the future of blocked tasks. + * Maps each currently-paused task ID to the {@link CompletableFuture} it is blocked on. + * Completing the future resumes the task. Guarded by {@link #tasksLock}. */ private final Map> taskFutures; + /** Lock guarding {@link #taskStates} and {@link #taskFutures}. */ private final Object tasksLock = new Object(); /** @@ -135,11 +151,25 @@ public void resume(Long taskId) throws TaskNotExists { throw new TaskNotExists(taskId); } future.complete(null); - taskFutures.remove(taskId); + //taskFutures.remove(taskId); nstead, we let the future be removed when the waiting thread is + // resumed and reaches the line after future.get() in wait() taskStates.put(taskId, TaskState.RUNNING); } } + /** + * Resumes the task with the specified custom ID, delivering a value to it. + * + *

The task's future is removed and the task is marked {@link TaskState#RUNNING}, then the + * future is completed with {@code value}. The value becomes the return of the task's pending + * {@link #wait(Long)} call (used to deliver reactive/symbolic results). If the stored future + * cannot be cast to the expected type, a {@link TaskNotExists} is thrown. + * + * @param the type of the value delivered to the task + * @param taskId the custom ID of the task + * @param value the value to deliver to the resumed task + * @throws TaskNotExists if the task with the specified custom ID does not exist + */ @SuppressWarnings("unchecked") public void resume(Long taskId, T value) throws TaskNotExists { CompletableFuture future; @@ -149,18 +179,30 @@ public void resume(Long taskId, T value) throws TaskNotExists { // The task is not paused or has been completed. throw new TaskNotExists(taskId); } - taskFutures.remove(taskId); + //taskFutures.remove(taskId); Instead, we let the future be removed when the waiting thread is + // resumed and reaches the line after future.get() in wait() taskStates.put(taskId, TaskState.RUNNING); } try { CompletableFuture castedFuture = (CompletableFuture) future; castedFuture.complete(value); + LOGGER.debug("Task {} is resumed with value {} on future {}", taskId, value, future); } catch (ClassCastException e) { LOGGER.error("Failed to cast future for task: {}", taskId); throw new TaskNotExists(taskId); } } + /** + * Completes the task's future exceptionally with the given exception. + * + *

Used to unblock a paused task by signalling a failure to its pending {@link #wait(Long)} + * call (for example, blocking a task with a {@link HaltTaskException}). Does nothing if the task + * has no pending future. + * + * @param taskId the custom ID of the task + * @param e the exception to complete the task's future with + */ public void error(Long taskId, Exception e) { synchronized (tasksLock) { CompletableFuture future = taskFutures.get(taskId); @@ -168,7 +210,8 @@ public void error(Long taskId, Exception e) { return; } future.completeExceptionally(e); - taskFutures.remove(taskId); + //taskFutures.remove(taskId); nstead, we let the future be removed when the waiting thread is + // resumed and reaches the line after future.get() in wait() } } @@ -186,7 +229,8 @@ public void terminate(Long taskId) { return; } future.complete(null); - taskFutures.remove(taskId); + //taskFutures.remove(taskId); instead, we let the future be removed when the waiting thread is + // resumed and reaches the line after future.get() in wait() } } @@ -278,9 +322,19 @@ public boolean isTaskOfStatus(Long taskId, TaskState state) { } /** - * Wait for the task with the specified custom ID to complete. + * Blocks until the task with the specified custom ID is resumed, returning any delivered value. + * + *

Blocks on the task's future via {@code get()}. Returns {@code null} immediately if the task + * has no pending future. A {@link HaltTaskException} or a re-execution {@link + * HaltExecutionException} wrapped as the future's cause is unwrapped and rethrown; any other + * failure is propagated as {@link ExecutionException}. Invoked by {@link JmcRuntime#wait(Long)}. * + * @param the type of the value delivered when the task is resumed * @param taskId the custom ID of the task + * @return the value delivered when the task is resumed, or {@code null} if there is no pending + * future + * @throws InterruptedException if the waiting thread is interrupted + * @throws ExecutionException if the task's future completed exceptionally */ @SuppressWarnings("unchecked") public T wait(Long taskId) throws InterruptedException, ExecutionException { @@ -289,16 +343,31 @@ public T wait(Long taskId) throws InterruptedException, ExecutionException { future = taskFutures.get(taskId); } if (future == null) { + LOGGER.debug("Task {} has no pending future to wait on", taskId); return null; } try { CompletableFuture castedFuture = (CompletableFuture) future; - return castedFuture.get(); + LOGGER.debug("Task {} is waiting on future {}", taskId, future); + T result = castedFuture.get(); + // A thread will reach this line only if the scheduler has completed it's corresponding future object. + // Thus, it is now safe to remove the future from taskFutures map + synchronized (tasksLock) { + taskFutures.remove(taskId); + } + LOGGER.debug("Task {} is now resumed with value {} from future {}", taskId, result, future); + return result; } catch (Exception e) { + // The future must be removed from the tasksLock even if an exception happens + synchronized (tasksLock) { + taskFutures.remove(taskId); + } Throwable cause = e.getCause(); if (cause instanceof HaltTaskException) { throw (HaltTaskException) cause; } else if (cause instanceof HaltExecutionException && ((HaltExecutionException) cause).isReexecutionNeeded()) { + LOGGER.debug("The future related to task {} has been completed exceptionally" + + " for re-execution purpose", taskId); throw HaltExecutionException.reexecutionNeeded(); } else { throw e; @@ -307,10 +376,13 @@ public T wait(Long taskId) throws InterruptedException, ExecutionException { } /** - * Stop all the tasks in the task pool. + * Stops every task in the pool at once. + * + *

Completes all pending task futures exceptionally with a {@link HaltExecutionException} + * error and then clears both the futures and the state map. This is the bulk counterpart to the + * incremental {@link #doNextStop()} / {@link #stopTask(Long)} teardown. */ public void stopAll() { - System.out.println("******stopAll*****"); synchronized (tasksLock) { for (Map.Entry> entry : taskFutures.entrySet()) { entry.getValue() @@ -322,6 +394,15 @@ public void stopAll() { } } + /** + * Selects the next task to stop while the scheduler is unwinding an execution. + * + *

Returns the highest task ID that is neither {@link TaskState#TERMINATED} nor {@link + * TaskState#CREATED} (i.e. a started task that can still be stopped), or {@code -1} if none + * remain. Used by the scheduler's "stop all" mode to tear tasks down in descending ID order. + * + * @return the ID of the next task to stop, or {@code -1L} if there is none + */ public Long doNextStop() { synchronized (tasksLock) { List taskIds = new ArrayList<>(taskStates.keySet()); @@ -337,6 +418,16 @@ public Long doNextStop() { return -1L; } + /** + * Stops a single paused task by failing its future with a re-execution signal. + * + *

Completes the task's future exceptionally with {@link + * HaltExecutionException#reexecutionNeeded()}, causing its pending {@link #wait(Long)} to + * unwind. Does nothing if the task has no pending future. Invoked by the scheduler's "stop all" + * mode (after {@link #doNextStop()} selects the task). + * + * @param taskId the custom ID of the task to stop + */ public void stopTask(Long taskId) { synchronized (tasksLock) { CompletableFuture future = taskFutures.get(taskId); diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValue.java b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValue.java index 86ee4d9f..e4191d22 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValue.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValue.java @@ -11,22 +11,45 @@ */ public class ObjectValue extends SchedulingChoiceValue { + /** The wrapped object. */ private final Object value; + + /** Shared Gson instance used to serialize the wrapped object. */ private static final Gson gson = new Gson(); + /** + * Constructs a new object value wrapping the given object. + * + * @param value the object to wrap + */ public ObjectValue(Object value) { this.value = value; } + /** + * Returns the wrapped object. + * + * @return the wrapped object + */ public Object asObject() { return value; } + /** + * Serializes the wrapped object to a JSON tree using Gson. + * + * @return the JSON representation of the wrapped object + */ @Override public JsonElement toJson() { return gson.toJsonTree(value); } + /** + * Returns the type tag for object values. + * + * @return the string {@code "object"} + */ @Override public String type() { return "object"; diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValueAdapter.java b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValueAdapter.java index 520bf758..9e6e53a6 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValueAdapter.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValueAdapter.java @@ -3,10 +3,19 @@ import com.google.gson.JsonElement; /** - * Adapter for converting JSON object values into {@link ObjectValue}. + * Adapter that reconstructs an {@link ObjectValue} from its JSON representation. + * + *

Registered with the {@link SchedulingChoiceValueFactory} for the {@code "object"} type tag.

*/ public class ObjectValueAdapter extends SchedulingChoiceValueAdapter { + /** + * Reconstructs an {@link ObjectValue} from a JSON object. + * + * @param json the JSON element to convert + * @return the reconstructed object value, wrapping the JSON object + * @throws IllegalArgumentException if {@code json} is not a JSON object + */ @Override public ObjectValue fromJson(JsonElement json) { if (!json.isJsonObject()) { diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValue.java b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValue.java index f8da86d6..10be263f 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValue.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValue.java @@ -12,12 +12,25 @@ */ public class PrimitiveValue extends SchedulingChoiceValue{ + /** The wrapped primitive value (a {@link Number}, {@link String}, or {@link Boolean}). */ private final Object value; + /** + * Constructs a new primitive value wrapping the given object. + * + * @param value the primitive value (expected to be a {@link Number}, {@link String}, or {@link + * Boolean}) + */ public PrimitiveValue(Object value) { this.value = value; } + /** + * Returns the wrapped value as an {@code int}. + * + * @return the value as an integer + * @throws ClassCastException if the wrapped value is not a {@link Number} + */ public int asInteger() { if (value instanceof Integer) { return (Integer) value; @@ -28,6 +41,12 @@ public int asInteger() { } } + /** + * Returns the wrapped value as a {@link String}. + * + * @return the value as a string + * @throws ClassCastException if the wrapped value is not a {@link String} + */ public String asString() { if (value instanceof String) { return (String) value; @@ -36,6 +55,12 @@ public String asString() { } } + /** + * Returns the wrapped value as a {@code boolean}. + * + * @return the value as a boolean + * @throws ClassCastException if the wrapped value is not a {@link Boolean} + */ public boolean asBoolean() { if (value instanceof Boolean) { return (Boolean) value; @@ -44,6 +69,12 @@ public boolean asBoolean() { } } + /** + * Serializes the wrapped value to a JSON primitive. + * + * @return the JSON representation of the value + * @throws IllegalArgumentException if the wrapped value is not a supported primitive type + */ @Override public JsonElement toJson() { if (value instanceof String) { @@ -57,6 +88,11 @@ public JsonElement toJson() { } } + /** + * Returns the type tag for primitive values. + * + * @return the string {@code "primitive"} + */ @Override public String type() { return "primitive"; diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValueAdapter.java b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValueAdapter.java index 8fb7d2db..a48d0b72 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValueAdapter.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValueAdapter.java @@ -4,13 +4,20 @@ import com.google.gson.JsonPrimitive; /** - * Represents a primitive (Number|String|Boolean) value used in scheduling choices. + * Adapter that reconstructs a {@link PrimitiveValue} from its JSON representation. * - *

This class extends {@link SchedulingChoiceValue} to provide a specific implementation - * for integer, string or boolean values, allowing them to be serialized to JSON and identified by type.

+ *

Handles JSON primitives of string, number, and boolean kind. Registered with the {@link + * SchedulingChoiceValueFactory} for the primitive type tags.

*/ public class PrimitiveValueAdapter extends SchedulingChoiceValueAdapter { + /** + * Reconstructs a {@link PrimitiveValue} from a JSON primitive (string, number, or boolean). + * + * @param json the JSON element to convert + * @return the reconstructed primitive value + * @throws IllegalArgumentException if {@code json} is not a supported JSON primitive + */ @Override public PrimitiveValue fromJson(JsonElement json) { if (json.isJsonPrimitive()) { diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/Scheduler.java b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/Scheduler.java index 1c9d33af..d0ef5d50 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/Scheduler.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/Scheduler.java @@ -23,6 +23,7 @@ */ public class Scheduler { + /** Logger used to trace scheduling decisions and the "stop all" path. */ private static final Logger LOGGER = LogManager.getLogger(Scheduler.class.getName()); /** @@ -40,6 +41,7 @@ public class Scheduler { */ private Long currentTask; + /** Lock guarding {@link #currentTask}. */ private final Object currentTaskLock = new Object(); /** @@ -47,12 +49,16 @@ public class Scheduler { */ private final SchedulerThread schedulerThread; + /** Whether the scheduler is currently unwinding all tasks to end the execution. */ private boolean stopAllMode = false; /** * Constructs a new Scheduler object. * * @param strategy the scheduling strategy + * @param schedulerTries the number of times the scheduler thread retries obtaining a runnable + * task before giving up + * @param schedulerTrySleepTimeNanos the sleep, in nanoseconds, between those retries */ public Scheduler( SchedulingStrategy strategy, int schedulerTries, long schedulerTrySleepTimeNanos) { @@ -84,6 +90,8 @@ public void init(TaskManager taskManager, Long mainTaskId) { * Initializes the strategy for a new iteration. * * @param iteration the number of the iteration + * @param report the model checker report, forwarded to the strategy + * @throws HaltCheckerException if the strategy decides the whole check must stop */ public void initIteration(int iteration, JmcModelCheckerReport report) throws HaltCheckerException { @@ -136,7 +144,7 @@ protected void scheduleTask(SchedulingChoice void scheduleTask(SchedulingChoiceSets {@link #stopAllMode} and immediately stops one task via {@link #doNextStop()}; the + * remaining tasks are stopped incrementally as the scheduler thread runs. + */ private void startStopAllMode() { stopAllMode = true; doNextStop(); } + /** + * Stops the next task while unwinding the execution. + * + *

Selects the next task to stop via {@link TaskManager#doNextStop()}, makes it current, and + * stops it via {@link TaskManager#stopTask(Long)}. When the main task (id {@code 1}) is stopped, + * "stop all" mode is exited. Throws a {@link HaltExecutionException} if no task can be selected. + */ private void doNextStop() { Long taskId = taskManager.doNextStop(); if (taskId == -1L) { LOGGER.error("Task ID is null, cannot stop the task."); throw HaltExecutionException.error("Task ID is null, cannot stop the task."); } + LOGGER.debug("The next task to be stopped: {}", taskId); setCurrentTask(taskId); - taskManager.stopTask(taskId); + // We must reset the stopAllMode flag before trying to stop the main (last remaining active) thread if (taskId == 1L) { // Main task stopped, exit stop all mode stopAllMode = false; LOGGER.debug("Exiting stop all mode."); } + taskManager.stopTask(taskId); } /** - * Updates the event in the scheduling strategy. + * Forwards an event to the scheduling strategy. + * + *

No-op while the scheduler is in "stop all" mode. * - * @param event the event to be updated + * @param event the event to be forwarded + * @throws HaltTaskException if the strategy requires the originating task to be halted */ public void updateEvent(JmcRuntimeEvent event) throws HaltTaskException { if (isInStopAllMode()) { + LOGGER.debug("Event {} received while in stop all mode, ignoring.", event); return; } strategy.updateEvent(event); @@ -208,6 +235,12 @@ public CompletableFuture yield() throws TaskAlreadyPaused { return null; } + /** + * Yields control to the scheduler thread without pausing the current task. + * + *

Clears the current task and enables the scheduler thread, but does not create a pausing + * future for the caller. Used when the caller must not block (e.g. {@code JmcRuntime.join}). + */ public void yieldWithoutPausing() { synchronized (currentTaskLock) { currentTask = null; @@ -241,12 +274,20 @@ public CompletableFuture yield(Long taskId) throws TaskAlreadyPaused { } /** - * Resets the TaskManager and the scheduling strategy for a new iteration. + * Resets the scheduling strategy for a new iteration. + * + * @param iteration the iteration number being reset */ public void resetIteration(int iteration) { strategy.resetIteration(iteration); } + /** + * Records the current schedule if the strategy supports replay. + * + *

If the strategy is a {@link ReplayableSchedulingStrategy}, records its trace; otherwise logs + * a warning. Recording failures are logged and swallowed. + */ public void recordTrace() { if (strategy instanceof ReplayableSchedulingStrategy) { try { @@ -261,12 +302,21 @@ public void recordTrace() { /** * Shuts down the scheduler. + * + *

Stops the scheduler thread and tears down the strategy. + * + * @param report the model checker report, forwarded to the strategy teardown */ public void shutdown(JmcModelCheckerReport report) { schedulerThread.shutdown(); strategy.teardown(report); } + /** + * Returns whether the scheduler is currently unwinding all tasks. + * + * @return {@code true} if in "stop all" mode + */ public boolean isInStopAllMode() { return stopAllMode; } @@ -276,6 +326,7 @@ public boolean isInStopAllMode() { */ private static class SchedulerThread extends Thread { + /** Logger used to trace the scheduler thread's lifecycle and per-step activity. */ private static final Logger LOGGER = LogManager.getLogger(SchedulerThread.class.getName()); /** @@ -294,8 +345,10 @@ private static class SchedulerThread extends Thread { */ private final LinkedBlockingQueue enablingQueue; + /** Number of times {@link SchedulingStrategy#nextTask()} is retried per scheduling step. */ private final int schedulerTries; + /** Sleep, in nanoseconds, between retries of {@link SchedulingStrategy#nextTask()}. */ private final long schedulerTrySleepTimeNanos; /** @@ -303,6 +356,8 @@ private static class SchedulerThread extends Thread { * * @param scheduler the scheduler instance * @param strategy the scheduling strategy + * @param schedulerTries the number of retries to obtain a runnable task per step + * @param schedulerTrySleepTimeNanos the sleep, in nanoseconds, between those retries */ public SchedulerThread( Scheduler scheduler, @@ -341,6 +396,12 @@ public void shutdown() { /** * The main loop of the scheduler thread. + * + *

Blocks on {@link #enablingQueue} until enabled by a yielding task (or signalled to shut + * down). On each step it either advances "stop all" mode, or asks the strategy for the next + * task (retrying up to {@link #schedulerTries} times with a sleep of {@link + * #schedulerTrySleepTimeNanos}) and applies the resulting choice via {@link + * Scheduler#scheduleTask(SchedulingChoice)}. Any exception ends the loop. */ @Override public void run() { diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoice.java b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoice.java index f06ea81a..f3f6f11f 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoice.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoice.java @@ -14,10 +14,22 @@ * @param the type of value associated with the scheduling choice */ public class SchedulingChoice { + /** Logger for this class. */ private static Logger LOGGER = LogManager.getLogger(SchedulingChoice.class); + + /** + * The ID of the task to act on, or {@code null} for an end-of-schedule or block-execution + * choice. + */ private Long taskId; + + /** Whether this choice blocks the task identified by {@link #taskId}. */ private boolean isBlockTask; + + /** Whether this choice stops the entire execution. */ private boolean isBlockExecution; + + /** Optional value delivered to the task when it is resumed (may be {@code null}). */ private T value; /** @@ -169,6 +181,11 @@ public static SchedulingChoice end() { return new SchedulingChoice<>(null, false, false); } + /** + * Returns a human-readable representation of this choice (task ID and the two block flags). + * + * @return a string representation of this scheduling choice + */ @Override public String toString() { return "SchedulingChoice{" diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValue.java b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValue.java index 07b9dcb2..deaff51c 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValue.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValue.java @@ -3,11 +3,15 @@ import com.google.gson.JsonElement; /** - * A value that the strategy uses to communicate with the runtime yields. + * A value that the strategy passes back to the runtime when resuming a task (delivered through the + * yield return value). * - *

The abstraction helps record the values when a buggy trace is found.

+ *

The abstraction also allows such values to be serialized so they can be recorded as part of a + * buggy trace and replayed later.

* - *

For each {@link SchedulingChoiceValue}, there should be a

+ *

For each {@link SchedulingChoiceValue} subclass there should be a corresponding {@link + * SchedulingChoiceValueAdapter} registered with the {@link SchedulingChoiceValueFactory} to + * reconstruct it from JSON.

*/ public abstract class SchedulingChoiceValue { diff --git a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValueFactory.java b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValueFactory.java index 8562aefd..96e7b188 100644 --- a/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValueFactory.java +++ b/core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValueFactory.java @@ -37,6 +37,16 @@ public static void registerAdapter( ADAPTERS.put(type, adapter); } + /** + * Creates a {@link SchedulingChoiceValue} from its type tag and JSON representation. + * + *

Looks up the adapter registered for {@code type} and delegates to its {@code fromJson}. + * + * @param type the type tag (as returned by {@link SchedulingChoiceValue#type()}) + * @param valueObject the JSON representation of the value + * @return the reconstructed scheduling choice value + * @throws IllegalArgumentException if no adapter is registered for the given type + */ public static SchedulingChoiceValue create(String type, JsonElement valueObject) throws IllegalArgumentException{ if (!ADAPTERS.containsKey(type)) { throw new IllegalArgumentException("No adapter registered for type: " + type); @@ -46,6 +56,12 @@ public static SchedulingChoiceValue create(String type, JsonElement valueObject) return adapter.fromJson(valueObject); } + /** + * Returns whether an adapter is registered for the given type tag. + * + * @param type the type tag to check + * @return {@code true} if an adapter is registered for the type + */ public static boolean containsType(String type) { return ADAPTERS.containsKey(type); } diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/JmcInvalidStrategyException.java b/core/src/main/java/org/mpi_sws/jmc/strategies/JmcInvalidStrategyException.java index f39bde6b..7870738d 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/JmcInvalidStrategyException.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/JmcInvalidStrategyException.java @@ -8,6 +8,11 @@ *

This exception indicates that the strategy parameter provided is not valid or recognized. */ public class JmcInvalidStrategyException extends JmcCheckerException { + /** + * Constructs a new exception with the given message. + * + * @param message the detail message describing the invalid strategy + */ public JmcInvalidStrategyException(String message) { super(message); } diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/JmcReplayUnsupported.java b/core/src/main/java/org/mpi_sws/jmc/strategies/JmcReplayUnsupported.java index 6f7433dc..06b1b8ee 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/JmcReplayUnsupported.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/JmcReplayUnsupported.java @@ -9,6 +9,7 @@ * which may be required for certain operations or analyses. */ public class JmcReplayUnsupported extends JmcCheckerException { + /** Constructs a new exception with a fixed "replay not supported" message. */ public JmcReplayUnsupported() { super("Replay is not supported by this strategy."); } diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/RandomSchedulingStrategy.java b/core/src/main/java/org/mpi_sws/jmc/strategies/RandomSchedulingStrategy.java index e3b06668..dce17b9a 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/RandomSchedulingStrategy.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/RandomSchedulingStrategy.java @@ -17,23 +17,42 @@ import java.util.concurrent.atomic.AtomicLong; /** - * A random scheduling strategy that selects the next thread to be scheduled randomly. + * A scheduling strategy that, at each step, picks the next task uniformly at random from the set of + * currently runnable tasks. + * + *

It extends {@link TrackActiveTasksStrategy} to obtain the set of runnable tasks (computed by the + * trackers) and implements {@link ReplayableSchedulingStrategy} so that a run can be reproduced from + * its seed. It also answers reactive random-value events ({@link + * JmcRuntimeEvent.Type#REACTIVE_EVENT_RANDOM_VALUE}) and records every choice into a {@link + * RandomSchedulingTrace} for replay. */ public class RandomSchedulingStrategy extends TrackActiveTasksStrategy implements ReplayableSchedulingStrategy { + /** Logger used to trace seeds, generated random values, and cached choices. */ private static final Logger LOGGER = LogManager.getLogger(RandomSchedulingStrategy.class); + /** Seeded random number generator that also exposes its seed for replay. */ protected final ExtRandom random; + + /** + * Pending reactive random values, keyed by the task that requested them. A value is produced in + * {@link #updateEvent(JmcRuntimeEvent)} and consumed (attached to the choice) in {@link + * #makeSchedulingChoice(Long)}. + */ protected final HashMap randomValueMap; + /** Directory where the replay seed and trace are written by {@link #recordTrace()}. */ private final String reportPath; + + /** The schedule (seed plus ordered choices) recorded for the current iteration. */ protected RandomSchedulingTrace curTrace; /** * Constructs a new RandomSchedulingStrategy object. * * @param seed the seed for the random number generator + * @param reportPath the directory where the replay seed and trace are written */ public RandomSchedulingStrategy(Long seed, String reportPath) { this.random = new ExtRandom(seed); @@ -42,6 +61,17 @@ public RandomSchedulingStrategy(Long seed, String reportPath) { this.curTrace = new RandomSchedulingTrace(seed); } + /** + * Initializes the strategy for a new iteration. + * + *

Delegates to the superclass (resetting tracker-derived state), records the current RNG seed + * into the report for replay, clears the pending reactive random values, and starts a fresh + * trace seeded with the current seed. + * + * @param iteration the number of the iteration + * @param report the model checker report; the replay seed is recorded into it + * @throws HaltExecutionException if initialization fails and the execution must halt + */ @Override public void initIteration(int iteration, JmcModelCheckerReport report) throws HaltExecutionException { @@ -75,6 +105,16 @@ public SchedulingChoice nextTask() { return makeSchedulingChoice(taskToSchedule); } + /** + * Builds the scheduling choice for the chosen task and records it in the current trace. + * + *

If a reactive random value is pending for the task (see {@link + * #updateEvent(JmcRuntimeEvent)}), it is consumed from {@link #randomValueMap} and attached to + * the choice as a {@link PrimitiveValue} so it is delivered to the task on resume. + * + * @param taskToSchedule the ID of the task to schedule + * @return the scheduling choice for the task (with a value attached if one was pending) + */ protected SchedulingChoice makeSchedulingChoice(Long taskToSchedule) { SchedulingChoice choice = SchedulingChoice.task(taskToSchedule); if (randomValueMap.containsKey(taskToSchedule)) { @@ -86,7 +126,18 @@ protected SchedulingChoice makeSchedulingChoice(Long taskToSchedule) { return choice; } - // Keep track of reactive events that need a return value + /** + * Updates the tracker state and answers reactive random-value requests. + * + *

First delegates to the superclass so the trackers update the runnable-task set. Then, for a + * {@link JmcRuntimeEvent.Type#REACTIVE_EVENT_RANDOM_VALUE}, generates a random value of the + * requested bit width and stashes it in {@link #randomValueMap} keyed by the requesting task, to + * be delivered on that task's next scheduling choice. + * + * @param event the event that occurred + * @throws HaltTaskException if the originating task must be halted + * @throws HaltExecutionException if the current execution must be halted + */ @Override public void updateEvent(JmcRuntimeEvent event) throws HaltTaskException, HaltExecutionException { @@ -100,6 +151,14 @@ public void updateEvent(JmcRuntimeEvent event) } } + /** + * Records the current schedule for later replay. + * + *

Writes the seed to {@code replay_seed.txt} and the ordered list of choices to {@code + * replay_trace.json}, both under {@link #reportPath}. + * + * @throws JmcCheckerException if writing the seed or trace files fails + */ @Override public void recordTrace() throws JmcCheckerException { String seedFilePath = Paths.get(this.reportPath, "replay_seed.txt").toString(); @@ -108,40 +167,77 @@ public void recordTrace() throws JmcCheckerException { FileUtil.storeTaskSchedule(traceFilePath, this.curTrace.getChoices()); } + /** + * Replays a previously recorded trace. + * + *

Not yet implemented (the recorded trace is currently not consumed). + * + * @throws JmcCheckerException if replay fails + */ @Override public void replayRecordedTrace() throws JmcCheckerException { // TODO: complete this } - /* - * ExtRandom is a custom random number generator that exposes the seed and mimics the behavior - * of the default Random class. + /** + * ExtRandom mirrors {@link Random} while exposing its internal seed for replay and + * validating that the local Linear Congruential Generator (LCG) step matches {@link Random#next(int)}. */ protected static class ExtRandom extends Random { + /** + * Current LCG state (scrambled seed), kept as an {@link AtomicLong} for atomic updates. + */ private AtomicLong seed; + /** + * LCG multiplier used by {@link Random}. + */ private static final long multiplier = 0x5DEECE66DL; + /** + * LCG addend used by {@link Random}. + */ private static final long addend = 0xBL; + /** + * Bit mask for the 48-bit LCG state used by {@link Random}. + */ private static final long mask = (1L << 48) - 1; + /** + * Creates a new random generator initialized with the provided seed. + * The {@link Random} constructor invokes {@link #setSeed(long)}. + */ public ExtRandom(long seed) { super(seed); } + /** + * Scrambles the external seed to the 48-bit internal LCG state. + */ private static long initialScramble(long seed) { return (seed ^ multiplier) & mask; } + /** + * Resets the generator with a new seed and updates the exposed atomic state. + */ @Override public synchronized void setSeed(long seed) { super.setSeed(seed); this.seed = new AtomicLong(initialScramble(seed)); } + /** + * Returns the current scrambled LCG seed (used for replay reporting and + * reinitializing the current trace's seed) + */ public Long getSeed() { return seed.get(); } + /** + * Advances the LCG state, verifies it matches {@link Random#next(int)}, + * and returns the generated value for the requested bit width. + */ @Override public int next(int bits) { int orig = super.next(bits); @@ -160,23 +256,49 @@ public int next(int bits) { } } + /** + * An immutable-seed record of a single iteration's schedule: the RNG seed plus the ordered list + * of scheduling choices made. Persisted by {@link #recordTrace()} for replay. + */ protected static class RandomSchedulingTrace { + /** The RNG seed for this trace. */ private final long seed; + /** The scheduling choices made during the iteration, in order. */ private final List> choices; + /** + * Constructs a new trace for the given seed with an empty choice list. + * + * @param seed the RNG seed for this trace + */ public RandomSchedulingTrace(long seed) { this.seed = seed; this.choices = new ArrayList<>(); } + /** + * Appends a scheduling choice to this trace. + * + * @param choice the choice to append + */ public void addChoice(SchedulingChoice choice) { choices.add(choice); } + /** + * Returns the RNG seed for this trace. + * + * @return the seed + */ public long getSeed() { return seed; } + /** + * Returns the ordered list of scheduling choices in this trace. + * + * @return the list of choices + */ public List> getChoices() { return choices; } diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/ReplayableSchedulingStrategy.java b/core/src/main/java/org/mpi_sws/jmc/strategies/ReplayableSchedulingStrategy.java index 9991dbf5..29b95a7c 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/ReplayableSchedulingStrategy.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/ReplayableSchedulingStrategy.java @@ -19,9 +19,17 @@ * allow replaying in the subsequent iteration. */ public interface ReplayableSchedulingStrategy extends SchedulingStrategy { - /** Records the current execution trace of the scheduling strategy. */ + /** + * Records the current execution trace of the scheduling strategy. + * + * @throws JmcCheckerException if the trace cannot be recorded + */ void recordTrace() throws JmcCheckerException; - /** Replays the recorded execution trace of the scheduling strategy. */ + /** + * Replays the recorded execution trace of the scheduling strategy. + * + * @throws JmcCheckerException if the recorded trace cannot be loaded or replayed + */ void replayRecordedTrace() throws JmcCheckerException; } diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategy.java b/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategy.java index 59c52f41..7ed0f84c 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategy.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategy.java @@ -15,38 +15,53 @@ *

It is used by the {@link Scheduler} to decide which thread to schedule next. The {@link * Scheduler} is in turn used by the {@link JmcRuntime} to manage the execution of threads. * - *

Implementations of this interface should be thread-safe. Multiple threads can make concurrent - * calls to the {@link SchedulingStrategy#updateEvent} function. + *

Because JMC serializes execution, a strategy is never entered concurrently: {@link + * SchedulingStrategy#updateEvent} runs on the single currently-running task, while {@link + * SchedulingStrategy#nextTask} runs on the scheduler thread while all program tasks are paused. The + * two therefore alternate rather than overlap. */ public interface SchedulingStrategy { /** * Initializes the strategy for a new iteration. * - * @param iteration the number of the iteration. + * @param iteration the number of the iteration + * @param report the model checker report for the run + * @throws HaltCheckerException if the strategy decides the whole check must stop */ void initIteration(int iteration, JmcModelCheckerReport report) throws HaltCheckerException; /** - * Updates the strategy with the event that has occurred. + * Updates the strategy with an event that has occurred. * - *

May be left empty if unused + *

May be left empty if the strategy does not consume events. + * + * @param event the event that occurred + * @throws HaltTaskException if the originating task must be halted + * @throws HaltExecutionException if the current execution must be halted */ void updateEvent(JmcRuntimeEvent event) throws HaltTaskException, HaltExecutionException; /** - * Returns the ID of the next thread to be scheduled. + * Returns the next scheduling choice to apply. + * + *

May return {@code null} if no task is runnable yet; the scheduler thread retries in that + * case. * - * @return the ID of the next thread to be scheduled. + * @return the next {@link SchedulingChoice}, or {@code null} if none is available */ SchedulingChoice nextTask(); /** - * Resets the strategy for the current Iteration. + * Resets the strategy's per-iteration state. + * + * @param iteration the number of the iteration being reset */ void resetIteration(int iteration); /** - * Teardown the strategy. Allows for releasing resources. + * Tears down the strategy, allowing it to release any resources. + * + * @param report the model checker report for the run */ void teardown(JmcModelCheckerReport report); } diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyConfiguration.java b/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyConfiguration.java index 89589221..22c2cd3f 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyConfiguration.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyConfiguration.java @@ -12,48 +12,129 @@ * flexible and readable configuration of scheduling strategies. */ public class SchedulingStrategyConfiguration { + /** Seed for the strategy's random number generator (may be {@code null} for a random seed). */ private Long seed; + /** Scheduling policy used by the {@code trust} strategy family. */ private TrustStrategy.SchedulingPolicy trustSchedulingPolicy; + /** Directory where the strategy writes its reports/artifacts. */ private String reportPath; + /** Whether debug mode is enabled for the strategy. */ private boolean debug; + /** Exploration budget for the estimating strategies (e.g. {@code testor}). */ private int budget; + /** Solver selection for symbolic execution (e.g. {@code "off"}). */ private String solver; + /** Target bug depth {@code d} for the PCT strategies (always ≥ 1). */ + private int bugDepth; + /** + * Fair-suffix bound for the {@code fair-pct} strategy: the number of priority-controlled + * scheduling decisions before switching to a uniform-random ("fair") suffix. A value + * {@code <= 0} selects automatic mode (switch once a run exceeds the learned step bound). + */ + private int pctFairBound; + /** Private constructor; instances are created through {@link Builder}. */ private SchedulingStrategyConfiguration() { } + /** + * Returns the configured RNG seed. + * + * @return the seed, or {@code null} if unset + */ public Long getSeed() { return seed; } + /** + * Returns the configured solver selection. + * + * @return the solver selection + */ public String getSolver() { return solver; } + /** + * Returns the report output directory. + * + * @return the report path + */ public String getReportPath() { return reportPath; } + /** + * Returns whether debug mode is enabled. + * + * @return {@code true} if debug mode is enabled + */ public boolean getDebug() { return debug; } + /** + * Returns the exploration budget. + * + * @return the budget + */ public int getBudget() { return budget; } + /** + * Returns the trust scheduling policy. + * + * @return the trust scheduling policy + */ public TrustStrategy.SchedulingPolicy getTrustSchedulingPolicy() { return trustSchedulingPolicy; } + /** + * Returns the target bug depth {@code d} used by the PCT strategies. + * + * @return the bug depth (always ≥ 1) + */ + public int getBugDepth() { + return bugDepth; + } + + /** + * Returns the fair-suffix bound used by the {@code fair-pct} strategy. + * + * @return the fair bound; a value {@code <= 0} means automatic mode + */ + public int getPctFairBound() { + return pctFairBound; + } + + /** + * Builder for {@link SchedulingStrategyConfiguration}. + * + *

All values start with defaults (no seed, {@code RANDOM} trust policy, the default report + * path, debug off, budget 2, solver {@code "off"}, bug depth 3, fair bound 0 = auto) and can be + * overridden fluently. + */ public static class Builder { + /** The RNG seed to build with. */ private Long seed; + /** The trust scheduling policy to build with. */ private TrustStrategy.SchedulingPolicy trustSchedulingPolicy; + /** The report path to build with. */ private String reportPath; + /** The debug flag to build with. */ private boolean debug; + /** The exploration budget to build with. */ private int budget; + /** The solver selection to build with. */ private String solver; + /** The PCT bug depth to build with. */ + private int bugDepth; + /** The fair-pct fair-suffix bound to build with ({@code <= 0} = auto). */ + private int pctFairBound; + /** Creates a builder pre-populated with the default configuration values. */ public Builder() { this.seed = null; this.trustSchedulingPolicy = TrustStrategy.SchedulingPolicy.RANDOM; @@ -61,33 +142,71 @@ public Builder() { this.debug = false; this.budget = 2; this.solver = "off"; + this.bugDepth = 3; + this.pctFairBound = 0; } + /** + * Sets the trust scheduling policy. + * + * @param trustSchedulingPolicy the trust scheduling policy + * @return this builder, for chaining + */ public Builder trustSchedulingPolicy(TrustStrategy.SchedulingPolicy trustSchedulingPolicy) { this.trustSchedulingPolicy = trustSchedulingPolicy; return this; } + /** + * Sets the report output directory. + * + * @param reportPath the report path + * @return this builder, for chaining + */ public Builder reportPath(String reportPath) { this.reportPath = reportPath; return this; } + /** + * Sets the solver selection. + * + * @param solver the solver selection + * @return this builder, for chaining + */ public Builder solver(String solver) { this.solver = solver; return this; } + /** + * Enables debug mode. + * + * @return this builder, for chaining + */ public Builder debug() { this.debug = true; return this; } + /** + * Sets the RNG seed. + * + * @param seed the seed + * @return this builder, for chaining + */ public Builder seed(Long seed) { this.seed = seed; return this; } + /** + * Sets the exploration budget. + * + * @param budget the budget (must be at least 1) + * @return this builder, for chaining + * @throws IllegalArgumentException if {@code budget} is less than 1 + */ public Builder budget(int budget) { if (budget < 1) { throw new IllegalArgumentException("Budget must be at least 1"); @@ -96,6 +215,38 @@ public Builder budget(int budget) { return this; } + /** + * Sets the target bug depth {@code d} for the PCT strategies. + * + * @param bugDepth the bug depth (must be at least 1) + * @return this builder, for chaining + * @throws IllegalArgumentException if {@code bugDepth} is less than 1 + */ + public Builder bugDepth(int bugDepth) { + if (bugDepth < 1) { + throw new IllegalArgumentException("bugDepth must be at least 1"); + } + this.bugDepth = bugDepth; + return this; + } + + /** + * Sets the fair-suffix bound for the {@code fair-pct} strategy. + * + * @param pctFairBound the number of priority-controlled decisions before switching to the + * fair random suffix; a value {@code <= 0} selects automatic mode + * @return this builder, for chaining + */ + public Builder pctFairBound(int pctFairBound) { + this.pctFairBound = pctFairBound; + return this; + } + + /** + * Builds an immutable {@link SchedulingStrategyConfiguration} from the configured values. + * + * @return a new {@link SchedulingStrategyConfiguration} instance + */ public SchedulingStrategyConfiguration build() { SchedulingStrategyConfiguration config = new SchedulingStrategyConfiguration(); config.seed = this.seed; @@ -104,12 +255,23 @@ public SchedulingStrategyConfiguration build() { config.debug = this.debug; config.budget = this.budget; config.solver = this.solver; + config.bugDepth = this.bugDepth; + config.pctFairBound = this.pctFairBound; return config; } } + /** + * Functional interface for constructing a {@link SchedulingStrategy} from a configuration. + */ @FunctionalInterface public interface SchedulingStrategyConstructor { + /** + * Creates a scheduling strategy from the given configuration. + * + * @param config the configuration + * @return the constructed scheduling strategy + */ SchedulingStrategy create(SchedulingStrategyConfiguration config); } } diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyFactory.java b/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyFactory.java index cfcafdfb..5f4fa525 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyFactory.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyFactory.java @@ -6,6 +6,8 @@ import org.mpi_sws.jmc.strategies.estimation.trust.TrustEstimationStrategy; import org.mpi_sws.jmc.strategies.estimation.trust.testor.TestorStrategy; import org.mpi_sws.jmc.strategies.estimation.trust.wgTrust.WgTrustEstimationStrategy; +import org.mpi_sws.jmc.strategies.pct.FairPCTSchedulingStrategy; +import org.mpi_sws.jmc.strategies.pct.PCTSchedulingStrategy; import org.mpi_sws.jmc.strategies.trust.TrustStrategy; import java.util.HashSet; @@ -16,11 +18,13 @@ */ public class SchedulingStrategyFactory { - // Set of valid strategies + /** Set of recognized strategy names accepted by {@link #createSchedulingStrategy}. */ private static final Set validStrategies = new HashSet<>(); static { validStrategies.add("random"); + validStrategies.add("pct"); + validStrategies.add("fair-pct"); validStrategies.add("trust"); validStrategies.add("pestor"); validStrategies.add("abs-dag-estimation"); @@ -36,6 +40,7 @@ public class SchedulingStrategyFactory { * @param name the name of the strategy * @param config the configuration for the strategy * @return the scheduling strategy + * @throws JmcInvalidStrategyException if {@code name} is not a recognized strategy */ public static SchedulingStrategy createSchedulingStrategy( String name, SchedulingStrategyConfiguration config) @@ -45,6 +50,15 @@ public static SchedulingStrategy createSchedulingStrategy( } if (name.equals("random")) { return new RandomSchedulingStrategy(config.getSeed(), config.getReportPath()); + } else if (name.equals("pct")) { + return new PCTSchedulingStrategy( + config.getSeed(), config.getReportPath(), config.getBugDepth()); + } else if (name.equals("fair-pct")) { + return new FairPCTSchedulingStrategy( + config.getSeed(), + config.getReportPath(), + config.getBugDepth(), + config.getPctFairBound()); } else if (name.equals("trust")) { return new TrustStrategy( config.getSeed(), diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/ValueTracker.java b/core/src/main/java/org/mpi_sws/jmc/strategies/ValueTracker.java index 2fe7a7af..94998555 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/ValueTracker.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/ValueTracker.java @@ -16,48 +16,95 @@ */ public class ValueTracker { + /** Pending values keyed by task ID, to be delivered to each task when it is resumed. */ private final Map values; + /** Constructs an empty value tracker. */ public ValueTracker() { values = new HashMap(); } + /** + * Constructs a value tracker backed by the given map. + * + * @param values the map to use as backing storage + */ public ValueTracker(Map values) { this.values = values; } + /** + * Returns the backing map of all tracked values. + * + * @return the map of task ID to value + */ public Map getValues() { return values; } + /** + * Returns the value tracked for the given task ID. + * + * @param id the task ID + * @return the tracked value, or {@code null} if none + */ public Object getValue(long id) { return values.get(id); } + /** + * Sets the value to deliver to the given task. + * + * @param id the task ID + * @param value the value to track for that task + */ public void setValue(long id, Object value) { values.put(id, value); } + /** Clears all tracked values. */ public void reset() { values.clear(); } + /** + * Adds all entries from the given map to the tracked values. + * + * @param newValues the values to merge in + */ public void updateValues(Map newValues) { values.putAll(newValues); } + /** + * Removes the value tracked for the given task ID. + * + * @param id the task ID whose value to remove + */ public void removeValue(long id) { values.remove(id); } + /** Clears all tracked values. */ public void removeAll() { values.clear(); } + /** + * Returns whether a value is tracked for the given task ID. + * + * @param id the task ID + * @return {@code true} if a value is tracked for that task + */ public boolean containsValue(long id) { return values.containsKey(id); } + /** + * Returns the number of tracked values. + * + * @return the number of tracked values + */ public int size() { return values.size(); } diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/pct/FairPCTSchedulingStrategy.java b/core/src/main/java/org/mpi_sws/jmc/strategies/pct/FairPCTSchedulingStrategy.java new file mode 100644 index 00000000..9bcd3bfd --- /dev/null +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/pct/FairPCTSchedulingStrategy.java @@ -0,0 +1,161 @@ +package org.mpi_sws.jmc.strategies.pct; + +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import org.mpi_sws.jmc.checker.JmcModelCheckerReport; +import org.mpi_sws.jmc.runtime.HaltExecutionException; +import org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice; +import org.mpi_sws.jmc.strategies.RandomSchedulingStrategy; + +import java.util.Set; + +/** + * A fair variant of {@link PCTSchedulingStrategy}: it schedules with PCT priorities for a + * bounded prefix and then falls back to uniform-random scheduling for the remainder of the + * iteration (a "fair execution suffix"). + * + *

Why a fair suffix is needed. Pure PCT is a strict priority scheduler, so a high-priority + * task that busy-waits on a value produced by a lower-priority task can starve it and the run never + * terminates. In JMC this is a real possibility: a task spinning on a plain field keeps emitting + * {@code READ_EVENT}s and therefore stays in the active set (only lock/join/wait-notify/static-init + * blocking removes a task). After a bounded number of priority-controlled decisions this strategy + * switches to uniform-random selection, which is probabilistically fair and guarantees progress. + * This mirrors Coyote's {@code FairPrioritization} and Lockstep's {@code FairPCT}. (It is a + * tool-inspired liveness extension, not part of the original PCT paper, whose own remedy is to lower + * the priority of non-progressing threads with small probability.) + * + *

The fair bound. The switch point is configured by {@code fairBound}: + * + *

    + *
  • {@code fairBound > 0} — an explicit bound: switch to the fair suffix once {@code + * fairBound} priority-controlled decisions have been made (Coyote/Lockstep style). + *
  • {@code fairBound <= 0} — automatic: the bound for each iteration is a snapshot of the + * learned step bound {@code k} ({@link #getMaxStep()}) taken at the start of that iteration, + * i.e. the largest number of decisions seen in any previous run. So normal-length + * runs stay entirely under PCT, and only an abnormally long run — the signature of a + * spin-loop livelock — crosses the bound and switches to the fair suffix. The first iteration + * has no learned bound yet ({@code k == 0}), so it runs as pure PCT (which is also how {@code + * k} is discovered). + *
+ * + *

The decision is driven by {@link #getCurrentStep()} (the number of genuine scheduling + * decisions made so far this iteration, counted by the PCT superclass). The effective bound + * for the current iteration is computed once in {@link #initIteration(int, JmcModelCheckerReport)} + * and stored in {@link #effectiveBound}. Because the fair suffix does not advance the decision + * counter, the strategy stays in the suffix for the rest of the iteration once it switches. + * + *

Faithfulness. The pure PCT per-run probabilistic guarantee applies to the + * priority-controlled prefix; randomizing the suffix only helps liveness and never prevents a + * prefix-reachable bug from being found. Pure PCT (without a suffix) remains available as {@link + * PCTSchedulingStrategy}. All randomness comes from the inherited seeded generator, so runs remain + * reproducible from their seed. + */ +public class FairPCTSchedulingStrategy extends PCTSchedulingStrategy { + + /** Logger used to trace the switch from the PCT prefix to the fair random suffix. */ + private static final Logger LOGGER = LogManager.getLogger(FairPCTSchedulingStrategy.class); + + /** + * The configured fair bound. A value {@code > 0} is an explicit number of priority-controlled + * decisions before switching to the fair suffix; a value {@code <= 0} selects automatic mode + * (the bound is derived from the learned step bound each iteration — see {@link #effectiveBound}). + */ + private final int fairBound; + + /** + * The fair bound actually used for the current iteration, recomputed in {@link + * #initIteration(int, JmcModelCheckerReport)}. Equals {@link #fairBound} in explicit mode, or a + * snapshot of {@link #getMaxStep()} (the learned bound from previous iterations) in automatic + * mode. A value {@code <= 0} disables the switch for this iteration (pure PCT), which is what + * happens on the first iteration in automatic mode before {@code k} is known. + */ + private int effectiveBound; + + /** + * Constructs a new fair PCT scheduling strategy. + * + * @param seed the seed for the random number generator + * @param reportPath the directory where the replay seed and trace are written + * @param bugDepth the target bug depth {@code d} (must be ≥ 1); forwarded to {@link + * PCTSchedulingStrategy} + * @param fairBound the fair-suffix bound: {@code > 0} for an explicit number of + * priority-controlled decisions before switching to the fair random suffix, or {@code <= 0} + * for automatic mode (derived from the learned step bound) + * @throws IllegalArgumentException if {@code bugDepth < 1} (from the superclass) + */ + public FairPCTSchedulingStrategy(Long seed, String reportPath, int bugDepth, int fairBound) { + super(seed, reportPath, bugDepth); + this.fairBound = fairBound; + this.effectiveBound = 0; + } + + /** + * Initializes the strategy for a new iteration and computes this iteration's effective fair + * bound. + * + *

Delegates to {@link PCTSchedulingStrategy#initIteration(int, JmcModelCheckerReport)}, then + * sets {@link #effectiveBound}: the configured {@link #fairBound} when it is positive (explicit + * mode), otherwise a snapshot of {@link #getMaxStep()} (automatic mode). Since the superclass + * does not change the learned bound during initialization, this snapshot reflects the largest + * number of decisions observed in previous iterations. + * + * @param iteration the number of the iteration + * @param report the model checker report; the replay seed is recorded into it + * @throws HaltExecutionException if initialization fails and the execution must halt + */ + @Override + public void initIteration(int iteration, JmcModelCheckerReport report) + throws HaltExecutionException { + super.initIteration(iteration, report); + effectiveBound = fairBound > 0 ? fairBound : getMaxStep(); + LOGGER.debug("Fair PCT iteration {}: effectiveBound={}", iteration, effectiveBound); + } + + /** + * Returns the next task to schedule. + * + *

While this iteration's decision count ({@link #getCurrentStep()}) is below the + * {@link #effectiveBound} (or the bound is non-positive, i.e. disabled for this iteration), it + * delegates to {@link PCTSchedulingStrategy#nextTask()} (PCT priority scheduling). Once the bound + * is reached it selects uniformly at random among the active tasks (the fair suffix) and — because + * the suffix does not advance the decision counter — remains in the suffix for the rest of the + * iteration. + * + * @return the scheduling choice for the next task, or {@code null} if no task is active + */ + @Override + public SchedulingChoice nextTask() { + if (effectiveBound > 0 && getCurrentStep() >= effectiveBound) { + return fairRandomChoice(); + } + return super.nextTask(); + } + + /** + * Selects the next task uniformly at random among the active tasks, mirroring {@link + * RandomSchedulingStrategy#nextTask()}. + * + *

Uses the inherited seeded random generator so the suffix remains reproducible from the seed. + * A single active task is scheduled directly; otherwise one is chosen uniformly at random. The + * choice is built via {@link #makeSchedulingChoice(Long)} so trace recording and reactive-value + * delivery behave exactly as for the random strategy. + * + * @return the scheduling choice for the randomly selected task, or {@code null} if none is active + */ + private SchedulingChoice fairRandomChoice() { + Set active = getActiveTasks(); + if (active.isEmpty()) { + return null; + } + Long chosen; + if (active.size() == 1) { + chosen = active.iterator().next(); + } else { + int index = random.nextInt(active.size()); + chosen = (Long) active.toArray()[index]; + } + LOGGER.debug("Fair suffix (step {} >= bound {}): randomly scheduling task {}", + getCurrentStep(), effectiveBound, chosen); + return makeSchedulingChoice(chosen); + } +} diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/pct/PCTSchedulingStrategy.java b/core/src/main/java/org/mpi_sws/jmc/strategies/pct/PCTSchedulingStrategy.java new file mode 100644 index 00000000..77441ccd --- /dev/null +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/pct/PCTSchedulingStrategy.java @@ -0,0 +1,351 @@ +package org.mpi_sws.jmc.strategies.pct; + +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import org.mpi_sws.jmc.checker.JmcModelCheckerReport; +import org.mpi_sws.jmc.runtime.HaltExecutionException; +import org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice; +import org.mpi_sws.jmc.strategies.RandomSchedulingStrategy; +import org.mpi_sws.jmc.strategies.ReplayableSchedulingStrategy; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +/** + * A priority-based randomized scheduling strategy implementing PCT (Probabilistic Concurrency + * Testing). + * + *

PCT comes from "A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs" + * (Burckhardt, Kothari, Musuvathi, Nagarakatte, ASPLOS 2010). For a program with at most {@code n} + * tasks and {@code k} scheduling steps it finds a bug of depth {@code d} with probability + * at least {@code 1 / (n * k^(d-1))} per iteration. The strategy realizes the algorithm with three + * ingredients: + * + *

    + *
  1. Random initial priorities. Every task receives a random priority the first time it + * becomes runnable; at each step the runnable task of maximal priority runs. + *
  2. {@code d - 1} priority change points. Before each iteration, {@code d - 1} step + * indices are drawn uniformly from {@code [1, k]}. When the step counter reaches a change + * point, the task that would run is demoted below all others, inducing a preemption + * at that step. + *
  3. Schedule the maximal-priority runnable task at every step. + *
+ * + *

Integration with JMC

+ * + *

This class extends {@link RandomSchedulingStrategy} (and therefore {@link + * org.mpi_sws.jmc.strategies.tracker.TrackActiveTasksStrategy}) so that the set of runnable + * ("active") tasks is computed by the trackers exactly as for the random strategy. PCT only changes + * the selection made in {@link #nextTask()}: instead of picking a uniformly random active + * task it picks the active task of maximal priority. Everything else — the seeded {@code ExtRandom}, + * reactive-random-value handling in {@code updateEvent}, trace recording via {@link + * #makeSchedulingChoice(Long)}, and seed-based replay ({@link ReplayableSchedulingStrategy}) — is + * inherited unchanged. No change to {@code JmcRuntime}, the {@code Scheduler}, {@code TaskManager}, + * or any tracker is required. + * + *

Optimizations adopted from other PCT tools

+ * + *
    + *
  • Learned {@code k}. The step bound {@code k} ({@link #maxStep}) is not supplied by the + * user; it is learned as the largest number of scheduling decisions observed across + * iterations. Because JMC reuses the same strategy instance across iterations, this is simply + * a field that survives {@link #initIteration(int, JmcModelCheckerReport)}. + *
  • Decision-point counting (sequential-execution optimization). Steps where only one + * task is runnable are not counted, so change points fall only on genuine scheduling + * decisions. + *
  • Lazy priority assignment. Priorities are assigned on demand when a task first appears + * in the active set, so dynamically created tasks are handled and {@code n} need not be known + * in advance. + *
  • O(1) demotion. A demotion assigns an ever-decreasing priority value, guaranteeing the + * demoted task sits below all currently-known tasks without reordering a list. + *
+ * + *

The first iteration runs with {@link #maxStep} {@code == 0}, so no change points are installed: + * it is depth-1 PCT (random priorities only) and simultaneously the run during which {@code k} is + * discovered. + * + *

Determinism / replay. All PCT randomness (initial priorities and change-point indices) + * is drawn from the inherited seeded {@code ExtRandom}, so a run is fully reproducible from its seed + * — the same property the random strategy relies on. + * + *

Liveness. This is pure PCT and is therefore intentionally unfair: a + * high-priority task spinning on a value produced by a low-priority task can livelock. Use {@code + * FairPCTSchedulingStrategy} when a fair execution suffix is needed. + */ +public class PCTSchedulingStrategy extends RandomSchedulingStrategy { + + /** Logger used to trace priority assignments, change points, and demotions. */ + private static final Logger LOGGER = LogManager.getLogger(PCTSchedulingStrategy.class); + + /** + * Number of priority change points per iteration, equal to {@code d - 1} for a target bug depth + * {@code d}. Zero means no change points (pure depth-1 PCT). + */ + private final int numSwitchPoints; + + /** + * Priority assigned to each task seen so far this iteration (higher value = higher priority). + * Initial priorities are random values in {@code [0, 1)}; demotions are negative values handed + * out by {@link #nextDemotedPriority}, so a demoted task always ranks below every task with an + * initial priority. Tasks are added lazily by {@link #assignPriorities(Set)}. + */ + private final Map priorities; + + /** + * The set of decision-step indices (in {@code [1, maxStep]}) at which a demotion occurs. Sampled + * once per iteration by {@link #prepareChangePoints()}. + */ + private final Set changePoints; + + /** Number of scheduling decisions made in the current iteration (steps with > 1 active task). */ + private int currentStep; + + /** + * The largest {@link #currentStep} observed across all iterations so far — the learned step + * bound {@code k}. Persists across {@link #initIteration(int, JmcModelCheckerReport)} so that + * change points can be sampled from a realistic range. + */ + private int maxStep; + + /** + * Strictly decreasing counter that supplies the next demotion priority. Starts at {@code 0.0}; + * each demotion pre-decrements it (so values are {@code -1.0, -2.0, ...}), guaranteeing every + * demoted task ranks below all tasks holding an initial priority in {@code [0, 1)}. + */ + private double nextDemotedPriority; + + /** + * Constructs a new PCT scheduling strategy. + * + * @param seed the seed for the random number generator + * @param reportPath the directory where the replay seed and trace are written + * @param bugDepth the target bug depth {@code d} (must be ≥ 1); the number of priority change + * points is {@code d - 1} + */ + public PCTSchedulingStrategy(Long seed, String reportPath, int bugDepth) { + super(seed, reportPath); + if (bugDepth < 1) { + throw new IllegalArgumentException("bugDepth must be >= 1, but was " + bugDepth); + } + this.numSwitchPoints = bugDepth - 1; + this.priorities = new HashMap<>(); + this.changePoints = new HashSet<>(); + this.currentStep = 0; + this.maxStep = 0; + this.nextDemotedPriority = 0.0; + } + + /** + * Initializes the strategy for a new iteration. + * + *

Delegates to {@link RandomSchedulingStrategy#initIteration(int, JmcModelCheckerReport)} + * (which records the seed and resets the random-value map and trace), then resets the + * per-iteration PCT state and samples this iteration's change points from the learned step bound + * {@link #maxStep}. {@link #maxStep} itself is preserved across iterations. + * + * @param iteration the number of the iteration + * @param report the model checker report; the replay seed is recorded into it + * @throws HaltExecutionException if initialization fails and the execution must halt + */ + @Override + public void initIteration(int iteration, JmcModelCheckerReport report) + throws HaltExecutionException { + super.initIteration(iteration, report); + priorities.clear(); + changePoints.clear(); + currentStep = 0; + nextDemotedPriority = 0.0; + prepareChangePoints(); + LOGGER.debug( + "PCT iteration {}: maxStep={}, changePoints={}", iteration, maxStep, changePoints); + } + + /** + * Returns the next task to schedule: the active task of maximal priority. + * + *

The procedure is: + * + *

    + *
  1. If no task is active, return {@code null} (the scheduler will retry or detect a + * deadlock). + *
  2. If exactly one task is active, schedule it without counting a step (sequential-execution + * optimization). + *
  3. Assign random initial priorities to any newly-seen active tasks, then count this + * decision and update the learned bound {@link #maxStep}. + *
  4. If the current step is a change point, demote the maximal-priority active task and + * re-select, inducing a preemption at this step. + *
  5. Return the maximal-priority active task via {@link #makeSchedulingChoice(Long)} (which + * records the choice and attaches any pending reactive value). + *
+ * + * @return the scheduling choice for the maximal-priority active task, or {@code null} if none is + * active + */ + @Override + public SchedulingChoice nextTask() { + Set active = getActiveTasks(); + if (active.isEmpty()) { + return null; + } + if (active.size() == 1) { + return makeSchedulingChoice(active.iterator().next()); + } + + assignPriorities(active); + + // Count this scheduling decision and learn the step bound k (see recordDecision). + recordDecision(); + + Long next = highestPriority(active); + if (changePoints.contains(currentStep)) { + LOGGER.debug("Change point at step {}: demoting task {}", currentStep, next); + demote(next); + next = highestPriority(active); + } + return makeSchedulingChoice(next); + } + + /** + * Assigns a random initial priority in {@code [0, 1)} to every active task not yet seen this + * iteration. + * + *

New tasks are processed in ascending id order so the sequence of random draws is + * deterministic for a given seed regardless of the (unordered) iteration order of the active + * set, preserving reproducibility. + * + * @param active the current set of active (runnable) tasks + */ + private void assignPriorities(Set active) { + List newTasks = new ArrayList<>(); + for (Long task : active) { + if (!priorities.containsKey(task)) { + newTasks.add(task); + } + } + if (newTasks.isEmpty()) { + return; + } + Collections.sort(newTasks); + for (Long task : newTasks) { + double priority = random.nextDouble(); + priorities.put(task, priority); + LOGGER.debug("Assigned initial priority {} to task {}", priority, task); + } + } + + /** + * Returns the active task with the maximal priority. + * + *

Every active task is guaranteed to have a priority (assigned by {@link + * #assignPriorities(Set)} before this is called). Ties — which are effectively impossible with + * random {@code double} priorities — are broken deterministically in favor of the smaller task + * id so selection is reproducible. + * + * @param active the current set of active (runnable) tasks + * @return the active task of maximal priority + */ + private Long highestPriority(Set active) { + Long best = null; + double bestPriority = 0.0; + for (Long task : active) { + double priority = priorities.get(task); + if (best == null + || priority > bestPriority + || (priority == bestPriority && task < best)) { + best = task; + bestPriority = priority; + } + } + return best; + } + + /** + * Demotes the given task below all tasks holding an initial priority by assigning it the next + * (strictly decreasing) demotion priority. + * + * @param task the task to demote + */ + private void demote(Long task) { + nextDemotedPriority -= 1.0; + priorities.put(task, nextDemotedPriority); + } + + /** + * Records that a genuine scheduling decision (more than one runnable task) was made and learns + * the step bound {@code k}. + * + *

Increments the current-iteration decision counter and raises {@link #maxStep} if this + * iteration has now produced more decisions than any previous one. Because {@link #maxStep} is + * preserved across {@link #initIteration(int, JmcModelCheckerReport)}, this is how the bound + * {@code k} used to sample change points is learned over iterations (no user-supplied + * {@code k} is required). Steps with a single runnable task never reach this method, so {@code k} + * counts only real decision points (the sequential-execution optimization). + */ + private void recordDecision() { + currentStep += 1; + if (currentStep > maxStep) { + maxStep = currentStep; + } + } + + /** + * Samples this iteration's priority change points. + * + *

Draws {@code min(numSwitchPoints, maxStep)} distinct step indices uniformly from {@code [1, + * maxStep]} using the inherited seeded random generator. Does nothing when there are no change + * points to place (depth-1 PCT) or when {@code maxStep} is not yet known (the first iteration), + * leaving {@link #changePoints} empty. + */ + private void prepareChangePoints() { + if (numSwitchPoints <= 0 || maxStep <= 0) { + return; + } + int count = Math.min(numSwitchPoints, maxStep); + List candidates = new ArrayList<>(maxStep); + for (int step = 1; step <= maxStep; step++) { + candidates.add(step); + } + for (int i = 0; i < count; i++) { + int index = random.nextInt(candidates.size()); + changePoints.add(candidates.remove(index)); + } + } + + /** + * Returns the learned step bound {@code k}. + * + *

Package-private; exposed for unit testing. + * + * @return the largest number of scheduling decisions observed across iterations + */ + int getMaxStep() { + return maxStep; + } + + /** + * Returns the number of scheduling decisions made in the current iteration. + * + *

Package-private; exposed for unit testing. + * + * @return the current decision-step count + */ + int getCurrentStep() { + return currentStep; + } + + /** + * Returns a copy of the change points sampled for the current iteration. + * + *

Package-private; exposed for unit testing. + * + * @return the set of change-point step indices + */ + Set getChangePoints() { + return new HashSet<>(changePoints); + } +} diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackActiveTasksStrategy.java b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackActiveTasksStrategy.java index dd50a6de..3e2934c0 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackActiveTasksStrategy.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackActiveTasksStrategy.java @@ -11,20 +11,33 @@ import java.util.Set; /** - * A strategy that tracks the active tasks. + * Abstract scheduling strategy that maintains the set of currently runnable ("active") tasks. + * + *

It delegates to a list of {@link Tracker}s, each watching a category of events (task lifecycle, + * locks, wait/notify, static init, executors). On every event the runnable set is recomputed as the + * intersection of all trackers' runnable sets, so any tracker can independently block a + * task. Concrete strategies (e.g. {@link + * org.mpi_sws.jmc.strategies.RandomSchedulingStrategy}) extend this class and only decide which of + * the active tasks to schedule. */ public abstract class TrackActiveTasksStrategy implements SchedulingStrategy { + /** Logger used to trace the computed active-task set. */ private static final Logger LOGGER = LogManager.getLogger(TrackActiveTasksStrategy.class); + /** Every task ID seen so far this iteration. */ private final Set allTasks; + /** The currently runnable subset of {@link #allTasks}. Guarded by {@link #tasksLock}. */ private final Set activeTasks; + /** Lock guarding {@link #allTasks} and {@link #activeTasks}. */ private final Object tasksLock = new Object(); + /** The trackers consulted on every event; the active set is their intersection. */ private final List trackers; /** - * Constructs a new TrackActiveTasksStrategy object. + * Constructs a new strategy with the default trackers: {@link TrackTasks}, {@link + * TrackWaitNotify}, {@link TrackStaticInit}, and {@link TrackExecutors}. */ public TrackActiveTasksStrategy() { this.allTasks = new HashSet<>(); @@ -36,7 +49,9 @@ public TrackActiveTasksStrategy() { } /** - * Constructs a new TrackActiveTasksStrategy object with the given trackers. + * Constructs a new strategy with a custom list of trackers. + * + * @param trackers the trackers whose runnable sets are intersected to form the active set */ public TrackActiveTasksStrategy(List trackers) { this.allTasks = new HashSet<>(); @@ -44,10 +59,24 @@ public TrackActiveTasksStrategy(List trackers) { this.trackers = trackers; } + /** + * {@inheritDoc} + * + *

No-op at this level; subclasses may override to seed per-iteration state. + */ @Override public void initIteration(int iteration, JmcModelCheckerReport report) { } + /** + * Recomputes the active-task set from the given event. + * + *

Adds the event's task to {@link #allTasks}, then intersects that set with the runnable set + * returned by each {@link Tracker} for this event. The resulting intersection becomes the new + * {@link #activeTasks}. + * + * @param event the event to process + */ @Override public void updateEvent(JmcRuntimeEvent event) { Set localActiveTasks; @@ -66,6 +95,7 @@ public void updateEvent(JmcRuntimeEvent event) { } } + /** Clears the task sets and resets every tracker. */ private void clear() { synchronized (tasksLock) { activeTasks.clear(); @@ -76,11 +106,21 @@ private void clear() { } } + /** + * {@inheritDoc} + * + *

Clears all task and tracker state for the next iteration. + */ @Override public void resetIteration(int iteration) { clear(); } + /** + * {@inheritDoc} + * + *

Clears all task and tracker state on shutdown. + */ @Override public void teardown(JmcModelCheckerReport report) { clear(); diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackExecutors.java b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackExecutors.java index 64043b08..5fb65d7c 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackExecutors.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackExecutors.java @@ -1,5 +1,3 @@ -// Create new file: jmc/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackExecutors.java - package org.mpi_sws.jmc.strategies.tracker; import org.apache.logging.log4j.LogManager; @@ -12,14 +10,20 @@ import java.util.Set; import java.util.concurrent.ConcurrentHashMap; import java.util.concurrent.ExecutorService; -import java.util.concurrent.atomic.AtomicLong; /** - * Tracks ExecutorService instances to ensure proper shutdown and prevent memory leaks. - * Prioritizes tasks related to executor shutdown when executors are not properly closed. + * Tracks {@link ExecutorService} instances so they can be shut down between iterations, preventing + * leaked threads. + * + *

As a {@link Tracker} it does not restrict the runnable set during normal operation; its + * {@link #updateEvent(JmcRuntimeEvent)} simply records executors reported via {@code + * EXECUTOR_SHUTDOWN_EVENT} (action {@code "register"}) and otherwise returns all active tasks. Its + * real work happens in {@link #reset()}, which force-shuts-down any registered executor that was not + * already closed. */ public class TrackExecutors implements Tracker { + /** Logger used to trace executor registration and forced shutdown. */ private static final Logger LOGGER = LogManager.getLogger(TrackExecutors.class); /** @@ -34,11 +38,22 @@ public class TrackExecutors implements Tracker { */ private final Set activeTasks; + /** Constructs a new executor tracker with empty state. */ public TrackExecutors() { this.registeredExecutors = ConcurrentHashMap.newKeySet(); this.activeTasks = ConcurrentHashMap.newKeySet(); } + /** + * Records executor registrations and returns all active tasks. + * + *

This tracker does not block any task during normal operation; it only watches {@code + * EXECUTOR_SHUTDOWN_EVENT}s to register executors (its real work, force-shutting-down leaked + * executors, happens in {@link #reset()}). + * + * @param event the event to process + * @return the set of active tasks + */ @Override public Set updateEvent(JmcRuntimeEvent event) { Long taskId = event.getTaskId(); @@ -58,6 +73,12 @@ public Set updateEvent(JmcRuntimeEvent event) { return getActiveTasks(); } + /** + * Handles an executor shutdown event, registering the executor when the action is {@code + * "register"}. + * + * @param event the executor shutdown event (params {@code action} and {@code executor}) + */ private void handleExecutorEvent(JmcRuntimeEvent event) { String action = event.getParam("action"); ExecutorService executor = event.getParam("executor"); @@ -90,10 +111,19 @@ public void shutdownExecutors() { } } + /** + * Returns a snapshot copy of all active tasks. + * + * @return a copy of the active task set + */ private Set getActiveTasks() { return new HashSet<>(activeTasks); } + /** + * Resets the tracker, first forcing shutdown of any registered executors that were not properly + * shut down (to avoid leaking threads across iterations), then clearing all state. + */ @Override public void reset() { // Shutdown any executors that weren't properly shutdown diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackLocks.java b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackLocks.java index c7b09777..02872a46 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackLocks.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackLocks.java @@ -18,8 +18,13 @@ public class TrackLocks implements Tracker { */ private final Map> waitingTasks; + /** + * For each lock, the set of tasks that have requested it while it was free but have not yet been + * confirmed as the owner (via a {@code LOCK_ACQUIRED_EVENT}). + */ private final Map> wantingTasks; + /** Maps each known task to the lock it currently holds, if any. */ private final Map> activeTasks; /** Constructs a new TrackLocks object. */ @@ -70,6 +75,15 @@ public Set updateEvent(JmcRuntimeEvent event) { return getActiveTasks(); } + /** + * Handles a lock-acquire request for a task. Three cases: the task already holds the lock + * (reentrant, allowed); the lock is held by another task (the task is blocked and removed from + * active); or the lock is free (the task is recorded as wanting it and stays active). + * + * @param taskId the requesting task + * @param lock the lock instance being requested + * @return {@code true} if the task may proceed (reentrant case), {@code false} otherwise + */ protected boolean tryLock(Long taskId, Object lock) { // Want the lock. Three cases. // 1. Current task already has the lock. Ignore. @@ -98,6 +112,13 @@ protected boolean tryLock(Long taskId, Object lock) { return false; } + /** + * Records that a task has acquired a lock. The task becomes the owner; every other task that was + * wanting the same lock is moved to the waiting set (blocked) and removed from active. + * + * @param taskId the task that acquired the lock + * @param lock the lock instance that was acquired + */ protected void lockAcquired(Long taskId, Object lock) { // The lock is acquired by the current task. Remove it from the wanting list and add // the rest to waiting @@ -120,6 +141,13 @@ protected void lockAcquired(Long taskId, Object lock) { } } + /** + * Records that a task has released a lock. The owner is cleared and every task waiting on the + * lock is made active again (re-contending as wanting). + * + * @param taskId the task releasing the lock + * @param lock the lock instance being released + */ protected void unlock(Long taskId, Object lock) { // The lock is released. The waiting tasks are marked as active. LOGGER.debug("Task {} released lock {}", taskId, lock.hashCode()); @@ -135,10 +163,16 @@ protected void unlock(Long taskId, Object lock) { } } + /** + * Returns the set of tasks not currently blocked on a lock (the keys of {@link #activeTasks}). + * + * @return the set of active (non-lock-blocked) tasks + */ protected Set getActiveTasks() { return activeTasks.keySet(); } + /** Clears all tracked lock state. */ @Override public void reset() { activeTasks.clear(); diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackStaticInit.java b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackStaticInit.java index 2a799d65..14e4c825 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackStaticInit.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackStaticInit.java @@ -18,6 +18,7 @@ */ public class TrackStaticInit implements Tracker { + /** Logger for this tracker. */ private static final Logger LOGGER = LogManager.getLogger(TrackStaticInit.class); /** @@ -35,10 +36,22 @@ public class TrackStaticInit implements Tracker { */ private final Set activeTasks; + /** Constructs a new static-init tracker with empty state. */ public TrackStaticInit() { this.activeTasks = ConcurrentHashMap.newKeySet(); } + /** + * Tracks static-initialization events to enforce JVM-like single-threaded {@code }. + * + *

{@code START_STATIC_INIT_EVENT} marks the task as performing static init (with a + * re-entrancy count); {@code END_STATIC_INIT_EVENT} decrements/clears it. While any task is + * performing static init, only that task is reported as runnable; otherwise all active tasks are + * returned. + * + * @param event the event to process + * @return the runnable task set (the single initializing task, or all active tasks) + */ @Override public Set updateEvent(JmcRuntimeEvent event) { Long taskId = event.getTaskId(); @@ -83,10 +96,16 @@ public Set updateEvent(JmcRuntimeEvent event) { } + /** + * Returns a snapshot copy of all active tasks. + * + * @return a copy of the active task set + */ private Set getActiveTasks() { return new HashSet<>(activeTasks); } + /** Clears all tracked static-initialization state. */ @Override public void reset() { activeTasks.clear(); diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackTasks.java b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackTasks.java index c24e7c1b..38fcd7c5 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackTasks.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackTasks.java @@ -11,9 +11,13 @@ * Tracks the tasks start finish and join request events. */ public class TrackTasks implements Tracker { + /** Tasks that have started and not yet finished or blocked on a join. */ private final Set activeTasks; + /** For each target task, the set of tasks blocked joining on it. */ private final Map> waitingTasks; + /** Tasks that have finished. */ private final Set completedTasks; + /** Lock guarding {@link #activeTasks}, {@link #waitingTasks}, and {@link #completedTasks}. */ private final Object tasksLock = new Object(); /** @@ -25,6 +29,18 @@ public TrackTasks() { this.waitingTasks = new ConcurrentHashMap<>(); } + /** + * Tracks task start, finish, and join events. + * + *

On {@link JmcRuntimeEvent.Type#START_EVENT} the task becomes active. On {@link + * JmcRuntimeEvent.Type#FINISH_EVENT} the task is moved to completed and any tasks joining on it + * are released back to active. On {@link JmcRuntimeEvent.Type#JOIN_REQUEST_EVENT}, if the target + * task (param {@code waitingTask}) has not yet completed, the requesting task is blocked until it + * does. + * + * @param event the event to process + * @return the set of currently active tasks + */ @Override public Set updateEvent(JmcRuntimeEvent event) { if (event.getType() == JmcRuntimeEvent.Type.START_EVENT) { @@ -63,12 +79,18 @@ public Set updateEvent(JmcRuntimeEvent event) { return getActiveTasks(); } + /** + * Returns a snapshot copy of the currently active tasks. + * + * @return a copy of the active task set + */ private Set getActiveTasks() { synchronized (tasksLock) { return new HashSet<>(activeTasks); } } + /** Clears all tracked task state. */ @Override public void reset() { synchronized (tasksLock) { diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackWaitNotify.java b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackWaitNotify.java index 468adaf8..22074a71 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackWaitNotify.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackWaitNotify.java @@ -11,15 +11,29 @@ import static org.mpi_sws.jmc.api.JmcObject.handleHashCode; +/** + * Tracks Java monitor {@code wait}/{@code notify} semantics on top of {@link TrackLocks}. + * + *

Maintains, per monitor object, a set of tasks parked in {@code wait()} and a set of tasks that + * have been notified and are eligible to re-acquire the monitor. A waiting task is blocked (and its + * lock released); {@code notify}/{@code notifyAll} move waiters back toward active. The runnable set + * it reports is intersected with the lock tracker's runnable set. + */ public class TrackWaitNotify extends TrackLocks { + /** Logger used to trace the runnable set after wait/notify processing. */ private static final Logger LOGGER = LogManager.getLogger(TrackWaitNotify.class); + /** Tasks considered runnable by this tracker (not parked in a wait set). */ private final Set activeTasks; + /** All tasks this tracker has observed at least one event from. */ private final Set trackedTasks; + /** For each monitor object (by hash code), the tasks currently parked in {@code wait()}. */ private final HashMap> waitingTasks; + /** For each monitor object (by hash code), the notified tasks eligible to re-acquire it. */ private final HashMap> availableTasks; + /** Constructs a new wait/notify tracker with empty state. */ public TrackWaitNotify() { this.activeTasks = new HashSet<>(); this.trackedTasks = new HashSet<>(); @@ -27,6 +41,19 @@ public TrackWaitNotify() { this.availableTasks = new HashMap<>(); } + /** + * Tracks wait/notify events on top of lock tracking. + * + *

After delegating to {@link TrackLocks#updateEvent(JmcRuntimeEvent)}: {@code WAIT_EVENT} + * parks the task on the object's wait set and releases its lock; {@code NOTIFY_EVENT} moves the + * object's waiters to the available set and back to active; {@code NOTIFY_ALL_EVENT} moves all + * waiters (and previously available tasks) to active; {@code WAKEUP_EVENT} consumes an available + * notification (and errors if none is available). The result is intersected with the lock + * tracker's active set. + * + * @param event the event to process + * @return the set of tasks runnable according to both this tracker and the lock tracker + */ @Override public Set updateEvent(JmcRuntimeEvent event) { super.updateEvent(event); @@ -95,6 +122,7 @@ public Set updateEvent(JmcRuntimeEvent event) { return result; } + /** Clears all wait/notify state and the underlying lock state. */ @Override public void reset() { super.reset(); diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/Tracker.java b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/Tracker.java index 39b67de2..e048943d 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/Tracker.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/tracker/Tracker.java @@ -9,10 +9,14 @@ /** Tracks the active tasks based on events. */ public interface Tracker { /** - * Updates the event. + * Processes an event and returns the tasks this tracker currently considers runnable. * - * @param event the event to update - * @return the set of active tasks + *

The owning {@link TrackActiveTasksStrategy} intersects the returned set with those of the + * other trackers, so a tracker effectively blocks any task it omits. + * + * @param event the event to process + * @return the set of tasks this tracker considers runnable + * @throws HaltCheckerException if the tracker detects a condition that must stop the whole check */ Set updateEvent(JmcRuntimeEvent event) throws HaltCheckerException; diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/trust/Algo.java b/core/src/main/java/org/mpi_sws/jmc/strategies/trust/Algo.java index 0b7f0643..4824f528 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/trust/Algo.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/trust/Algo.java @@ -164,6 +164,7 @@ public void updateExternalValue(SchedulingChoice task) { long id = task.getTaskId() - 1; if (externalValueTracker.containsValue(id)) { Object value = externalValueTracker.getValue(id); + LOGGER.debug("Updating external value {} for task: {}", value, id); externalValueTracker.removeValue(id); PrimitiveValue val = new PrimitiveValue(value); @@ -217,9 +218,11 @@ private void handleGuidedEvent(Event event) { private void storeExternalValue(long id, Object value) { if (externalValueTracker.containsValue(id)) { + LOGGER.error("Value for id {} already exists in external tracker. This should not happen.", id); throw new RuntimeException("Value for id " + id + " already exists"); } + LOGGER.debug("Storing value {} for id {}", value, id); externalValueTracker.setValue(id, value); } @@ -371,6 +374,7 @@ public void handleNoop(Event event) { } public void handleSymbolic(Event event) { + LOGGER.debug("Handling symbolic event: {}", event); boolean result = processNewSymEvent(event); storeExternalValue(event.getKey().getTaskId(), result); } @@ -384,6 +388,7 @@ private boolean processNewSymEvent(Event event) { ExecutionGraphNode symb = this.executionGraph.addEvent(event); if (solverResult.isNegatable()) { + LOGGER.debug("Pushing the fWR item to explore the other outcome of symbolic event {}", event.key()); explorationStack.push( ExplorationStack.Item.symbolicForwardRevisit( symb, diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/trust/TrustStrategy.java b/core/src/main/java/org/mpi_sws/jmc/strategies/trust/TrustStrategy.java index da767843..7c75ca41 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/trust/TrustStrategy.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/trust/TrustStrategy.java @@ -123,7 +123,8 @@ public SchedulingChoice nextTask() { SchedulingChoice nextTask = algoInstance.nextTask(); if (nextTask != null) { if (!activeTasks.contains(nextTask.getTaskId())) { - LOGGER.debug("Guiding trace led us to a task that is not active: {}", nextTask); + LOGGER.debug("Guiding trace led us to a task={} that is not" + + " in active={}", nextTask, activeTasks); } // Update it's value based on value tracker in the algo algoInstance.updateExternalValue(nextTask); diff --git a/core/src/test/java/org/mpi_sws/jmc/strategies/pct/FairPCTSchedulingStrategyTest.java b/core/src/test/java/org/mpi_sws/jmc/strategies/pct/FairPCTSchedulingStrategyTest.java new file mode 100644 index 00000000..bbd5bced --- /dev/null +++ b/core/src/test/java/org/mpi_sws/jmc/strategies/pct/FairPCTSchedulingStrategyTest.java @@ -0,0 +1,156 @@ +package org.mpi_sws.jmc.strategies.pct; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertThrows; + +import org.junit.jupiter.api.Test; +import org.mpi_sws.jmc.checker.JmcModelCheckerReport; +import org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +/** + * Unit tests for {@link FairPCTSchedulingStrategy}. + * + *

The tests use {@code bugDepth == 1}, so the PCT prefix installs no change points and therefore + * selects a constant winner (strict priority), while the fair suffix selects uniformly at + * random. The boundary between a constant prefix and a varying suffix is what makes the + * prefix/suffix switch observable. As in {@link PCTSchedulingStrategyTest}, a {@link + * TestableFairPCT} subclass injects a controlled active set. + */ +public class FairPCTSchedulingStrategyTest { + + private static final String REPORT_PATH = "build/test-results/jmc-report-test"; + + /** A test seam over {@link FairPCTSchedulingStrategy} with an injectable active set. */ + private static final class TestableFairPCT extends FairPCTSchedulingStrategy { + private Set active = new HashSet<>(); + + TestableFairPCT(long seed, int bugDepth, int fairBound) { + super(seed, REPORT_PATH, bugDepth, fairBound); + } + + @Override + protected Set getActiveTasks() { + return new HashSet<>(active); + } + + void setActive(Long... ids) { + this.active = new HashSet<>(Arrays.asList(ids)); + } + + Long pick() { + SchedulingChoice choice = nextTask(); + return choice == null ? null : choice.getTaskId(); + } + } + + private static JmcModelCheckerReport report() { + return new JmcModelCheckerReport(REPORT_PATH); + } + + private static List runIteration( + TestableFairPCT strategy, int iteration, int numPicks, Long... activeIds) { + strategy.setActive(activeIds); + strategy.initIteration(iteration, report()); + List winners = new ArrayList<>(); + for (int i = 0; i < numPicks; i++) { + winners.add(strategy.pick()); + } + return winners; + } + + /** Asserts every element in {@code [from, to)} equals the element at {@code from}. */ + private static void assertConstant(List winners, int from, int to) { + Long ref = winners.get(from); + for (int i = from; i < to; i++) { + assertEquals(ref, winners.get(i), "expected constant winner at index " + i); + } + } + + /** Asserts some element in {@code [from, to)} differs from {@code value}. */ + private static void assertHasVariation(List winners, int from, int to, Long value) { + for (int i = from; i < to; i++) { + if (!winners.get(i).equals(value)) { + return; + } + } + throw new AssertionError("expected the suffix to vary from " + value + " but it never did"); + } + + @Test + public void constructorAllowsNonPositiveFairBoundButValidatesBugDepth() { + // fairBound <= 0 is the (valid) automatic mode. + new FairPCTSchedulingStrategy(0L, REPORT_PATH, 1, 0); + new FairPCTSchedulingStrategy(0L, REPORT_PATH, 1, -5); + // bugDepth < 1 is rejected by the superclass. + assertThrows( + IllegalArgumentException.class, + () -> new FairPCTSchedulingStrategy(0L, REPORT_PATH, 0, 5)); + } + + @Test + public void autoModeFirstIterationIsPurePct() { + // Auto mode (fairBound = 0): on the first iteration maxStep is 0, so effectiveBound is 0 and + // the fair switch is disabled — the whole iteration is pure PCT (a constant winner). + TestableFairPCT strategy = new TestableFairPCT(123L, 1, 0); + List winners = runIteration(strategy, 0, 30, 1L, 2L, 3L); + assertConstant(winners, 0, winners.size()); + assertEquals(30, strategy.getMaxStep()); + } + + @Test + public void explicitBoundSwitchesToFairSuffix() { + // Explicit fairBound = 3 applies from the first iteration: picks 1..3 are PCT (constant), + // picks 4+ are the fair (random) suffix. + int fairBound = 3; + TestableFairPCT strategy = new TestableFairPCT(123L, 1, fairBound); + List winners = runIteration(strategy, 0, 40, 1L, 2L, 3L); + + assertConstant(winners, 0, fairBound); + assertHasVariation(winners, fairBound, winners.size(), winners.get(0)); + } + + @Test + public void autoModeSwitchesAfterLearnedBound() { + // Auto mode: iteration 0 learns maxStep; iteration 1's effectiveBound is that snapshot, so + // the first maxStep decisions are PCT and the rest are the fair suffix. + TestableFairPCT strategy = new TestableFairPCT(2024L, 1, 0); + + runIteration(strategy, 0, 5, 1L, 2L, 3L); + int learned = strategy.getMaxStep(); + assertEquals(5, learned); + + List winners = runIteration(strategy, 1, 40, 1L, 2L, 3L); + assertConstant(winners, 0, learned); + assertHasVariation(winners, learned, winners.size(), winners.get(0)); + } + + @Test + public void sameSeedProducesIdenticalSchedules() { + // Determinism / replay-by-seed, including the random fair suffix. + TestableFairPCT a = new TestableFairPCT(777L, 1, 3); + TestableFairPCT b = new TestableFairPCT(777L, 1, 3); + + assertEquals( + runIteration(a, 0, 30, 1L, 2L, 3L), runIteration(b, 0, 30, 1L, 2L, 3L)); + assertEquals( + runIteration(a, 1, 30, 1L, 2L, 3L), runIteration(b, 1, 30, 1L, 2L, 3L)); + } + + @Test + public void autoModeRunNoLongerThanLearnedBoundStaysPurePct() { + // In auto mode, a later run that is no longer than the learned bound never reaches the fair + // suffix, so it remains a constant PCT winner. + TestableFairPCT strategy = new TestableFairPCT(55L, 1, 0); + runIteration(strategy, 0, 8, 1L, 2L, 3L); // learns maxStep = 8 + assertEquals(8, strategy.getMaxStep()); + + List winners = runIteration(strategy, 1, 8, 1L, 2L, 3L); // exactly the learned bound + assertConstant(winners, 0, winners.size()); + } +} diff --git a/core/src/test/java/org/mpi_sws/jmc/strategies/pct/PCTSchedulingStrategyTest.java b/core/src/test/java/org/mpi_sws/jmc/strategies/pct/PCTSchedulingStrategyTest.java new file mode 100644 index 00000000..10d1cef4 --- /dev/null +++ b/core/src/test/java/org/mpi_sws/jmc/strategies/pct/PCTSchedulingStrategyTest.java @@ -0,0 +1,245 @@ +package org.mpi_sws.jmc.strategies.pct; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import org.junit.jupiter.api.Test; +import org.mpi_sws.jmc.checker.JmcModelCheckerReport; +import org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +/** + * Unit tests for {@link PCTSchedulingStrategy} that exercise the PCT logic in isolation. + * + *

The tests drive the strategy directly: a {@link TestablePCT} subclass overrides {@link + * PCTSchedulingStrategy#getActiveTasks()} to inject a controlled active set, so {@link + * PCTSchedulingStrategy#nextTask()} can be invoked without the runtime/tracker machinery. The + * package-private accessors {@code getMaxStep()}, {@code getCurrentStep()} and {@code + * getChangePoints()} (visible because this test lives in the same package) are used for white-box + * assertions. + */ +public class PCTSchedulingStrategyTest { + + private static final String REPORT_PATH = "build/test-results/jmc-report-test"; + + /** A test seam over {@link PCTSchedulingStrategy} with an injectable active set. */ + private static final class TestablePCT extends PCTSchedulingStrategy { + private Set active = new HashSet<>(); + + TestablePCT(long seed, int bugDepth) { + super(seed, REPORT_PATH, bugDepth); + } + + @Override + protected Set getActiveTasks() { + return new HashSet<>(active); + } + + void setActive(Long... ids) { + this.active = new HashSet<>(Arrays.asList(ids)); + } + + /** Invokes {@link #nextTask()} and returns the chosen task id (or {@code null}). */ + Long pick() { + SchedulingChoice choice = nextTask(); + return choice == null ? null : choice.getTaskId(); + } + } + + private static JmcModelCheckerReport report() { + return new JmcModelCheckerReport(REPORT_PATH); + } + + /** Runs {@code numPicks} decisions over the given (constant) active set and returns the winners. */ + private static List runIteration( + TestablePCT strategy, int iteration, int numPicks, Long... activeIds) { + strategy.setActive(activeIds); + strategy.initIteration(iteration, report()); + List winners = new ArrayList<>(); + for (int i = 0; i < numPicks; i++) { + winners.add(strategy.pick()); + } + return winners; + } + + @Test + public void constructorRejectsBugDepthBelowOne() { + assertThrows( + IllegalArgumentException.class, + () -> new PCTSchedulingStrategy(0L, REPORT_PATH, 0)); + assertThrows( + IllegalArgumentException.class, + () -> new PCTSchedulingStrategy(0L, REPORT_PATH, -3)); + } + + @Test + public void emptyActiveSetReturnsNull() { + TestablePCT strategy = new TestablePCT(1L, 1); + strategy.setActive(); + strategy.initIteration(0, report()); + assertEquals(null, strategy.pick()); + } + + @Test + public void singleActiveTaskIsReturnedWithoutCountingAStep() { + TestablePCT strategy = new TestablePCT(1L, 2); + strategy.setActive(7L); + strategy.initIteration(0, report()); + + assertEquals(7L, strategy.pick()); + // A single-enabled step is the sequential-execution optimization: no decision is counted. + assertEquals(0, strategy.getCurrentStep()); + + // Once two tasks are enabled, the next call counts a decision. + strategy.setActive(7L, 8L); + strategy.pick(); + assertEquals(1, strategy.getCurrentStep()); + } + + @Test + public void selectionIsStableWithoutChangePoints() { + // bugDepth = 1 => no change points ever => strict priority => the same task always wins. + TestablePCT strategy = new TestablePCT(42L, 1); + List winners = runIteration(strategy, 0, 8, 1L, 2L, 3L); + Long first = winners.get(0); + for (Long w : winners) { + assertEquals(first, w); + } + // depth-1 PCT installs no change points regardless of the learned bound. + assertTrue(strategy.getChangePoints().isEmpty()); + } + + @Test + public void initialPrioritiesAreRandomizedAcrossSeeds() { + // With random initial priorities, the winner among {1,2} should vary across seeds. + Set winners = new HashSet<>(); + for (long seed = 0; seed < 100; seed++) { + TestablePCT strategy = new TestablePCT(seed, 1); + strategy.setActive(1L, 2L); + strategy.initIteration(0, report()); + winners.add(strategy.pick()); + } + assertTrue(winners.contains(1L), "task 1 never won across 100 seeds"); + assertTrue(winners.contains(2L), "task 2 never won across 100 seeds"); + } + + @Test + public void sameSeedProducesIdenticalSchedules() { + // Determinism / replay-by-seed: identical seed + identical active sets => identical winners. + TestablePCT a = new TestablePCT(12345L, 2); + TestablePCT b = new TestablePCT(12345L, 2); + + List winnersA0 = runIteration(a, 0, 6, 1L, 2L, 3L); + List winnersB0 = runIteration(b, 0, 6, 1L, 2L, 3L); + assertEquals(winnersA0, winnersB0); + + List winnersA1 = runIteration(a, 1, 6, 1L, 2L, 3L); + List winnersB1 = runIteration(b, 1, 6, 1L, 2L, 3L); + assertEquals(winnersA1, winnersB1); + } + + @Test + public void learnsStepBoundAcrossIterationsAndNeverDecreases() { + TestablePCT strategy = new TestablePCT(7L, 1); + + // First iteration: nothing learned yet, no change points. + strategy.setActive(1L, 2L); + strategy.initIteration(0, report()); + assertEquals(0, strategy.getMaxStep()); + for (int i = 0; i < 3; i++) { + strategy.pick(); + } + assertEquals(3, strategy.getCurrentStep()); + assertEquals(3, strategy.getMaxStep()); + + // Second iteration: currentStep resets, maxStep is preserved, then grows with a longer run. + strategy.initIteration(1, report()); + assertEquals(0, strategy.getCurrentStep()); + assertEquals(3, strategy.getMaxStep()); + for (int i = 0; i < 5; i++) { + strategy.pick(); + } + assertEquals(5, strategy.getMaxStep()); + + // Third iteration: a shorter run must not lower the learned bound. + strategy.initIteration(2, report()); + for (int i = 0; i < 2; i++) { + strategy.pick(); + } + assertEquals(5, strategy.getMaxStep()); + } + + @Test + public void changePointsAreSampledWithinTheLearnedBound() { + // bugDepth = 2 => numSwitchPoints = 1. + TestablePCT strategy = new TestablePCT(99L, 2); + + // Iteration 0 learns maxStep; no change points yet. + runIteration(strategy, 0, 6, 1L, 2L); + assertTrue(strategy.getChangePoints().isEmpty()); + assertEquals(6, strategy.getMaxStep()); + + // Iteration 1: exactly one change point, drawn from [1, maxStep]. + strategy.setActive(1L, 2L); + strategy.initIteration(1, report()); + Set points = strategy.getChangePoints(); + assertEquals(1, points.size()); + int point = points.iterator().next(); + assertTrue(point >= 1 && point <= 6, "change point " + point + " out of [1,6]"); + } + + @Test + public void demotionHappensExactlyAtTheChangePoint() { + // bugDepth = 2 => one change point. The winner must flip exactly at that step (or, if the + // change point is step 1, there is no earlier winner to flip from). + TestablePCT strategy = new TestablePCT(2024L, 2); + + // Learn maxStep = 6 with a change-point-free first iteration (constant winner). + List firstWinners = runIteration(strategy, 0, 6, 1L, 2L); + Long w0 = firstWinners.get(0); + for (Long w : firstWinners) { + assertEquals(w0, w, "iteration 0 must have a constant winner (no change points)"); + } + + // Second iteration with a single change point. + List winners = runIteration(strategy, 1, 6, 1L, 2L); + Set points = strategy.getChangePoints(); + assertEquals(1, points.size()); + int changePoint = points.iterator().next(); + + // Collect the 1-based steps at which the winner changed from the previous step. + List flips = new ArrayList<>(); + for (int i = 1; i < winners.size(); i++) { + if (!winners.get(i).equals(winners.get(i - 1))) { + flips.add(i + 1); // step index is 1-based + } + } + + assertTrue(flips.size() <= 1, "a single change point can cause at most one winner flip"); + if (flips.size() == 1) { + assertEquals(changePoint, flips.get(0).intValue(), + "the winner flip must occur exactly at the change point"); + } else { + // No observable flip => the change point demoted the leader on the very first step. + assertEquals(1, changePoint, "no flip observed, so the change point must be step 1"); + } + } + + @Test + public void depthOneNeverInstallsChangePoints() { + TestablePCT strategy = new TestablePCT(5L, 1); + // Learn a non-zero bound, then confirm subsequent iterations still have no change points. + runIteration(strategy, 0, 5, 1L, 2L); + assertFalse(strategy.getMaxStep() == 0); + strategy.setActive(1L, 2L); + strategy.initIteration(1, report()); + assertTrue(strategy.getChangePoints().isEmpty()); + } +} diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyAllTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyAllTest.java index e5aa2b9b..682ffc33 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyAllTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyAllTest.java @@ -28,4 +28,11 @@ private void testProgramWaitNotifyAll() { public void testChannel() { testProgramWaitNotifyAll(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + // TODO :: Check this test + public void testChannelPct() { + testProgramWaitNotifyAll(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyTest.java index cdb0a5ed..a3680bde 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyTest.java @@ -24,11 +24,19 @@ private void testProgram() { } } - // TODO : Fix the following test + // TODO :: Fix the following test @JmcCheck @JmcCheckConfiguration(numIterations = 10) @Disabled public void testChannel() { testProgram(); } + + // TODO :: Fix the following test + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + @Disabled + public void testChannelPct() { + testProgram(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ExpectFailureTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ExpectFailureTest.java index 1f015b08..87555061 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ExpectFailureTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ExpectFailureTest.java @@ -14,4 +14,12 @@ public void testExpectFailure() { // This test is expected to fail due to an assertion failure. fail("This assertion is expected to fail."); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 1, strategy = "pct") + @JmcExpectAssertionFailure + public void testExpectFailurePct() { + // This test is expected to fail due to an assertion failure. + fail("This assertion is expected to fail."); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ObjectWaitNotifyTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ObjectWaitNotifyTest.java index 8fe6aef4..05028fc5 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ObjectWaitNotifyTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ObjectWaitNotifyTest.java @@ -39,4 +39,37 @@ public void testBasicWaitNotify() throws InterruptedException { assertTrue(flag[0]); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void testBasicWaitNotifyPct() throws InterruptedException { + final Object obj = new Object(); + final boolean[] flag = {false}; + + Thread waiter = new Thread(() -> { + synchronized (obj) { + while (!flag[0]) { + try { + obj.wait(); + } catch (InterruptedException e) {} + } + } + }); + + Thread notifier = new Thread(() -> { + synchronized (obj) { + flag[0] = true; + obj.notify(); + } + }); + + waiter.start(); + Thread.sleep(50); // Ensure waiter calls wait() + notifier.start(); + + waiter.join(); + notifier.join(); + + assertTrue(flag[0]); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/StaticFinalFieldTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/StaticFinalFieldTest.java index a338e6a2..16fd51db 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/StaticFinalFieldTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/StaticFinalFieldTest.java @@ -13,4 +13,11 @@ public void testStaticFinalInterfaceField() { ConcreteFields f = new ConcreteFields(); assertEquals(3, f.getInitCounter()); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void testStaticFinalInterfaceFieldPct() { + ConcreteFields f = new ConcreteFields(); + assertEquals(3, f.getInitCounter()); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/SynchronisedAnnotationTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/SynchronisedAnnotationTest.java index c6f164c8..ba84ef55 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/SynchronisedAnnotationTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/SynchronisedAnnotationTest.java @@ -15,4 +15,11 @@ public void testSynchronisedAnnotation() { SynchronisedExtension e = new SynchronisedExtension(); assertEquals(1, e.doSomething()); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void testSynchronisedAnnotationPct() { + SynchronisedExtension e = new SynchronisedExtension(); + assertEquals(1, e.doSomething()); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ThreadFeaturesTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ThreadFeaturesTest.java index fe0f21d0..2fd2d96d 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ThreadFeaturesTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/features/ThreadFeaturesTest.java @@ -32,4 +32,15 @@ public void testGetCurrentThread() { // But for jdk classes like Thread, it causes issues. getCurrentThread(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void testGetCurrentThreadPct() { + // Static method invocations on extended class are fine. + // So the following is okay. + callTestClass(); + + // But for jdk classes like Thread, it causes issues. + getCurrentThread(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/ArrayTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/ArrayTest.java index 04a284a1..1e5a2ccd 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/ArrayTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/ArrayTest.java @@ -53,4 +53,10 @@ private void detArray(int SIZE) { public void runDetArrayTest() { detArray(3); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runDetArrayTestPct() { + detArray(3); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/AtomicCounterTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/AtomicCounterTest.java index 6aed72a4..51d55a1d 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/AtomicCounterTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/AtomicCounterTest.java @@ -39,4 +39,10 @@ private void atomicCounterTest(int length) { public void runAtomicCounterTest() { atomicCounterTest(3); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runAtomicCounterTestPct() { + atomicCounterTest(3); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/BigShotTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/BigShotTest.java index f8d89b5d..f8d10633 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/BigShotTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/BigShotTest.java @@ -92,4 +92,23 @@ public void runBigShotSTest() { public void runBigShotS2Test() { bigShotS2(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runBigShotPTestPct() { + bigShotP(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runBigShotSTestPct() { + bigShotS(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + @JmcExpectAssertionFailure + public void runBigShotS2TestPct() { + bigShotS2(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/CounterTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/CounterTest.java index 59531158..60bf28ba 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/CounterTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/CounterTest.java @@ -117,6 +117,13 @@ public void runFineCounterTest() { FineCounter(new String[]{"0", "1", "2", "3", "4", "5", "6", "7"}); } + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runFineCounterTestPct() { + // TODO : Make the test parametric + FineCounter(new String[]{"0", "1", "2", "3", "4", "5", "6", "7"}); + } + @JmcCheck @JmcCheckConfiguration(numIterations = 10) public void testRandomCounter() { @@ -125,6 +132,14 @@ public void testRandomCounter() { assertEquals(2, counter.getCounterValue()); } + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void testRandomCounterPct() { + ParametricCounter counter = new ParametricCounter(3); + counter.run(); + assertEquals(3, counter.getCounterValue()); + } + @JmcCheck @JmcCheckConfiguration(strategy = "trust", numIterations = 1000) public void testTrustCounter() { diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/OrderedListTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/OrderedListTest.java index 3a2c77f8..d8de0d50 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/OrderedListTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/OrderedListTest.java @@ -144,4 +144,28 @@ public void runRandom_50_50_FineListTest() { public void runTrust_50_50_FineListTest() { test_50_50_workload(3, new FineList()); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runPct_100_0_CoarseListTest() { + test_100_0_workload(3, new CoarseList()); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runPct_50_50_CoarseListTest() { + test_50_50_workload(3, new CoarseList()); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runPct_100_0_FineListTest() { + test_100_0_workload(3, new FineList()); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runPct_50_50_FineListTest() { + test_50_50_workload(3, new FineList()); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SendRecvTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SendRecvTest.java index 1e8fcd7c..942e270f 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SendRecvTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SendRecvTest.java @@ -34,4 +34,10 @@ private void sendRecvTest() { public void runSendRecvTest() { sendRecvTest(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void runSendRecvTestPct() { + sendRecvTest(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SynchronizedCounterTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SynchronizedCounterTest.java index 2bcc6ca3..74c1f77f 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SynchronizedCounterTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SynchronizedCounterTest.java @@ -79,4 +79,16 @@ public void testRandomSynchronizedBlockCounter() { public void testTrustSynchronizedBlockCounter() { testCounterSyncBlockProgram(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void testPctSynchronizedCounter() { + twoCounterProgram(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct") + public void testPctSynchronizedBlockCounter() { + testCounterSyncBlockProgram(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/BusyWaitFutureTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/BusyWaitFutureTest.java index 0f786249..5f7e08e9 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/BusyWaitFutureTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/BusyWaitFutureTest.java @@ -1,5 +1,6 @@ package org.mpi_sws.jmc.test.stress; +import org.junit.jupiter.api.Disabled; import org.mpi_sws.jmc.annotations.JmcCheck; import org.mpi_sws.jmc.annotations.JmcCheckConfiguration; @@ -147,9 +148,22 @@ public void testBusyWaitScenario() throws Exception { testBusyWait(); } + @JmcCheck + @JmcCheckConfiguration(numIterations = 3, strategy = "fair-pct", pctFairBound = 10, timeout = 10000L) + @Disabled + public void testBusyWaitScenarioPct() throws Exception { + testBusyWait(); + } + @JmcCheck @JmcCheckConfiguration(numIterations = 3) public void testBlockingWaitScenario() throws Exception { testBlockingWait(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 3, strategy = "pct", timeout = 10000L) + public void testBlockingWaitScenarioPct() throws Exception { + testBlockingWait(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ConcurrentStaticInitRaceTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ConcurrentStaticInitRaceTest.java index b9545824..bcaba550 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ConcurrentStaticInitRaceTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ConcurrentStaticInitRaceTest.java @@ -255,6 +255,197 @@ public void testMultipleThreadsNestedStaticInit() throws Exception { } + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testTwoThreadsAccessStaticFieldPct() throws Exception { + + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Thread 1: Access the static field + futures.add(executor.submit(() -> { + String value = StaticPatterns.ClassWithStaticInit.VALUE; + return value; + })); + + // Thread 2: Access the same static field + futures.add(executor.submit(() -> { + String value = StaticPatterns.ClassWithStaticInit.VALUE; + return value; + })); + + // Wait for both threads + String result1 = futures.get(0).get(); + + String result2 = futures.get(1).get(); + + executor.shutdown(); + + // Both should get the same value + assertEquals("initialized", result1); + assertEquals("initialized", result2); + + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMultipleThreadsComplexStaticInitPct() throws Exception { + + ExecutorService executor = Executors.newFixedThreadPool(3); + List> futures = new ArrayList<>(); + + // Three threads all accessing the same class + for (int i = 1; i <= 3; i++) { + final int threadNum = i; + futures.add(executor.submit(() -> { + int value = StaticPatterns.ComplexStaticInit.COMPUTED_VALUE; + return value; + })); + } + + // Wait for all threads + List results = new ArrayList<>(); + for (int i = 0; i < futures.size(); i++) { + Integer result = futures.get(i).get(); + results.add(result); + } + + executor.shutdown(); + + // All threads should get the same value + assertEquals(42 , results.get(0)); + assertEquals(42 , results.get(1)); + assertEquals(42 , results.get(2)); + + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMultipleStaticFieldsPct() throws Exception { + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Thread 1: Access field1 + futures.add(executor.submit(() -> { + String value = StaticPatterns.MultipleStaticFields.FIELD1; + return value; + })); + + // Thread 2: Access field2 (triggers same static init) + futures.add(executor.submit(() -> { + String value = StaticPatterns.MultipleStaticFields.FIELD2; + return value; + })); + + // Wait for both threads + String result1 = futures.get(0).get(); + String result2 = futures.get(1).get(); + + executor.shutdown(); + + assertEquals("field1", result1); + assertEquals("field2", result2); + + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + @JmcExpectAssertionFailure + public void testStaticInitSideEffectsPct() throws Exception { + // Reset the counter before test + StaticPatterns.StaticInitCounter.resetGlobalCounter(); + + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Thread 1: Access the class + futures.add(executor.submit(() -> { + int value = StaticPatterns.StaticInitCounter.VALUE; + return value; + })); + + // Thread 2: Access the class + futures.add(executor.submit(() -> { + int value = StaticPatterns.StaticInitCounter.VALUE; + return value; + })); + + // Wait for both threads + int result1 = futures.get(0).get(); + int result2 = futures.get(1).get(); + + executor.shutdown(); + + // Check how many times static init ran + int globalCount = StaticPatterns.StaticInitCounter.getGlobalCounter(); + + // In correct implementation, static init should run exactly once + // If there's a race, it might run multiple times + assertEquals(1 , globalCount); + + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMethodChainingStaticInitPct() throws Exception { + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Thread 1: Access the chained result + futures.add(executor.submit(() -> { + String value = StaticPatterns.IcebergLikeClass.JOINER; + return value; + })); + + // Thread 2: Access the chained result + futures.add(executor.submit(() -> { + String value = StaticPatterns.IcebergLikeClass.JOINER; + return value; + })); + + // Wait for both threads + String result1 = futures.get(0).get(); + String result2 = futures.get(1).get(); + + executor.shutdown(); + + assertEquals("joiner-configured", result1); + assertEquals("joiner-configured", result2); + + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMultipleThreadsNestedStaticInitPct() throws Exception { + ExecutorService executor = Executors.newFixedThreadPool(3); + List> futures = new ArrayList<>(); + + // Three threads all accessing the same class + for (int i = 1; i <= 3; i++) { + final int threadNum = i; + futures.add(executor.submit(() -> { + int value = StaticPatterns.ComplexStaticInit.COMPUTED_VALUE; + int value2 = StaticPatterns.B.y; + return value; + })); + } + + // Wait for all threads + List results = new ArrayList<>(); + for (int i = 0; i < futures.size(); i++) { + Integer result = futures.get(i).get(); + results.add(result); + } + + executor.shutdown(); + + // All threads should get the same value + assertEquals(42 , results.get(0)); + assertEquals(42 , results.get(1)); + assertEquals(42 , results.get(2)); + + } + } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ExecutorWithoutFutureTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ExecutorWithoutFutureTest.java index 1ae00c8a..a674a6e3 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ExecutorWithoutFutureTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ExecutorWithoutFutureTest.java @@ -13,8 +13,9 @@ * Stress test to reproduce the race condition in JmcExecutorWorker * where multiple tasks completing simultaneously cause incorrect * join() vs terminate() decisions due to racy queue.isEmpty() check. - * TODO : These tests do not explicitly call future, JMC cannot support them currently, we need to extend JMC to support them. */ +// TODO :: These tests do not explicitly call future, JMC cannot +// support them currently, we need to extend JMC to support them. public class ExecutorWithoutFutureTest { @Disabled @@ -97,4 +98,92 @@ public void testRaceConditionWithDebug() throws InterruptedException { throw new RuntimeException("Expected 5 tasks to complete, but got " + counter.get()); } } + + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + @Disabled + public void testMultipleTasksCompletingSimultaneouslyPct() throws InterruptedException { + ExecutorService executor = Executors.newFixedThreadPool(7); + AtomicInteger counter = new AtomicInteger(0); + + // Submit 7 tasks that do minimal work + // This maximizes the chance they'll all complete around the same time + // and all see queue.isEmpty() == true + for (int i = 0; i < 7; i++) { + executor.submit(() -> { + counter.incrementAndGet(); + return null; + }); + } + + + + executor.shutdown(); + //boolean terminated = executor.awaitTermination(1, TimeUnit.MINUTES); + +// if (!terminated) { +// throw new RuntimeException("Executor did not terminate in time"); +// } + + if (counter.get() != 7) { + throw new RuntimeException("Expected 7 tasks to complete, but got " + counter.get()); + } + } + + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + @Disabled + public void testManyTasksWithShutdownPct() throws InterruptedException { + // Even more tasks to increase race condition probability + ExecutorService executor = Executors.newFixedThreadPool(10); + AtomicInteger counter = new AtomicInteger(0); + + for (int i = 0; i < 10; i++) { + executor.submit(() -> { + counter.incrementAndGet(); + return null; + }); + } + + executor.shutdown(); + boolean terminated = executor.awaitTermination(1, TimeUnit.MINUTES); + + if (!terminated) { + throw new RuntimeException("Executor did not terminate in time"); + } + + if (counter.get() != 10) { + throw new RuntimeException("Expected 10 tasks to complete, but got " + counter.get()); + } + } + + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + @Disabled + public void testRaceConditionWithDebugPct() throws InterruptedException { + // Smaller test with debug enabled to see the exact error sequence + ExecutorService executor = Executors.newFixedThreadPool(5); + AtomicInteger counter = new AtomicInteger(0); + + for (int i = 0; i < 5; i++) { + executor.submit(() -> { + counter.incrementAndGet(); + return null; + }); + } + + executor.shutdown(); + boolean terminated = executor.awaitTermination(1, TimeUnit.MINUTES); + + if (!terminated) { + throw new RuntimeException("Executor did not terminate in time"); + } + + if (counter.get() != 5) { + throw new RuntimeException("Expected 5 tasks to complete, but got " + counter.get()); + } + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FieldAccessStarvationTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FieldAccessStarvationTest.java index 4500872e..66fb9845 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FieldAccessStarvationTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FieldAccessStarvationTest.java @@ -179,4 +179,137 @@ public void testTwoTasksFewerFieldAccesses() throws Exception { assertNotEquals(0, result2); executor.shutdown(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testTwoTasksManyFieldAccessesPct() throws Exception { + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Task 1: Access fields from object1 many times + DataObject object1 = new DataObject(); + futures.add(executor.submit(() -> { + int sum = 0; + // Access each field 10 times = 100 field reads total + for (int i = 0; i < 10; i++) { + sum += object1.field1; + sum += object1.field2; + sum += object1.field3; + sum += object1.field4; + sum += object1.field5; + sum += object1.field6; + sum += object1.field7; + sum += object1.field8; + sum += object1.field9; + sum += object1.field10; + } + return sum; + })); + + // Task 2: Access fields from object2 many times + DataObject object2 = new DataObject(); + futures.add(executor.submit(() -> { + int sum = 0; + // Access each field 10 times = 100 field reads total + for (int i = 0; i < 10; i++) { + sum += object2.field1; + sum += object2.field2; + sum += object2.field3; + sum += object2.field4; + sum += object2.field5; + sum += object2.field6; + sum += object2.field7; + sum += object2.field8; + sum += object2.field9; + sum += object2.field10; + } + return sum; + })); + + // Main thread waits for both tasks + int result1 = futures.get(0).get(); + + int result2 = futures.get(1).get(); + assertNotEquals(0, result1); + assertNotEquals(0, result2); + executor.shutdown(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testSingleTaskManyFieldAccessesPct() throws Exception { + ExecutorService executor = Executors.newFixedThreadPool(1); + + DataObject object = new DataObject(); + Future future = executor.submit(() -> { + int sum = 0; + for (int i = 0; i < 10; i++) { + sum += object.field1; + sum += object.field2; + sum += object.field3; + sum += object.field4; + sum += object.field5; + sum += object.field6; + sum += object.field7; + sum += object.field8; + sum += object.field9; + sum += object.field10; + } + return sum; + }); + + int result = future.get(); + assertNotEquals(0, result); + executor.shutdown(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testTwoTasksFewerFieldAccessesPct() throws Exception { + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + DataObject object1 = new DataObject(); + futures.add(executor.submit(() -> { + int sum = 0; + // Only 2 iterations = 20 field reads + for (int i = 0; i < 2; i++) { + sum += object1.field1; + sum += object1.field2; + sum += object1.field3; + sum += object1.field4; + sum += object1.field5; + sum += object1.field6; + sum += object1.field7; + sum += object1.field8; + sum += object1.field9; + sum += object1.field10; + } + return sum; + })); + + DataObject object2 = new DataObject(); + futures.add(executor.submit(() -> { + int sum = 0; + for (int i = 0; i < 2; i++) { + sum += object2.field1; + sum += object2.field2; + sum += object2.field3; + sum += object2.field4; + sum += object2.field5; + sum += object2.field6; + sum += object2.field7; + sum += object2.field8; + sum += object2.field9; + sum += object2.field10; + } + return sum; + })); + + int result1 = futures.get(0).get(); + int result2 = futures.get(1).get(); + assertNotEquals(0, result1); + assertNotEquals(0, result2); + executor.shutdown(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FinalizerThreadTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FinalizerThreadTest.java index daf55664..1861fdda 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FinalizerThreadTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FinalizerThreadTest.java @@ -46,6 +46,38 @@ public void testFinalizerConflictWithConcurrentTasks() throws Exception { executor.shutdown(); } + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testFinalizerConflictWithConcurrentTasksPct() throws Exception { + ExecutorService executor = Executors.newFixedThreadPool(2); + + // Create objects with finalizers + for (int i = 0; i < 5; i++) { + StreamLikeObject obj = new StreamLikeObject(); + obj.closed = false; + // Don't close it - let finalizer handle it + } + + // Submit concurrent tasks while finalizers might run + Future f1 = executor.submit(() -> { + // Trigger GC while task is running + System.gc(); + Thread.sleep(50); + return 1; + }); + + Future f2 = executor.submit(() -> { + Thread.sleep(50); + return 2; + }); + + // Wait for tasks + f1.get(); + f2.get(); + + executor.shutdown(); + } + /** * Mimics HadoopSeekableInputStream/HadoopPositionOutputStream * with a finalizer that checks a 'closed' field. diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergTasksRunParallelTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergTasksRunParallelTest.java index 7db6880d..24183edf 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergTasksRunParallelTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergTasksRunParallelTest.java @@ -616,4 +616,351 @@ public void testComplexScenarioAllFeatures() { executor.shutdown(); } } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testBasicParallelExecutionPct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + AtomicInteger counter = new AtomicInteger(0); + List items = List.of(1, 2, 3, 4, 5); + + try { + boolean result = new TasksBuilder<>(items) + .executeWith(executor) + .throwFailureWhenFinished(false) + .run(item -> { + counter.incrementAndGet(); + }); + + assertTrue(result); + assertEquals(5, counter.get()); + } finally { + executor.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testParallelExecutionWithFailuresPct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentLinkedQueue executed = new ConcurrentLinkedQueue<>(); + ConcurrentLinkedQueue failed = new ConcurrentLinkedQueue<>(); + List items = List.of(1, 2, 3, 4, 5); + + try { + boolean result = new TasksBuilder<>(items) + .executeWith(executor) + .stopOnFailure() + .throwFailureWhenFinished(false) + .onFailure((item, exception) -> { + failed.add(item); + }) + .run(item -> { + executed.add(item); + if (item == 2) { + throw new RuntimeException("Task 2 fails"); + } + }); + + assertFalse(result); + assertTrue(failed.contains(2)); + assertTrue(executed.contains(1) || executed.contains(2)); + } finally { + executor.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testAbortMechanismRacePct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentLinkedQueue executed = new ConcurrentLinkedQueue<>(); + ConcurrentLinkedQueue aborted = new ConcurrentLinkedQueue<>(); + List items = List.of(1, 2, 3, 4, 5); + + try { + new TasksBuilder<>(items) + .executeWith(executor) + .stopOnFailure() + .throwFailureWhenFinished(false) + .abortWith(item -> { + aborted.add(item); + }) + .run(item -> { + executed.add(item); + if (item == 1) { + throw new RuntimeException("Task 1 fails"); + } + }); + + // Verify no task is both executed and aborted + for (Integer item : executed) { + assertFalse(aborted.contains(item), + "Item " + item + " was both executed and aborted"); + } + } finally { + executor.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testRevertMechanismRacePct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentLinkedQueue executed = new ConcurrentLinkedQueue<>(); + ConcurrentLinkedQueue reverted = new ConcurrentLinkedQueue<>(); + List items = List.of(1, 2, 3, 4, 5); + + try { + new TasksBuilder<>(items) + .executeWith(executor) + .stopOnFailure() + .throwFailureWhenFinished(false) + .revertWith(item -> { + reverted.add(item); + }) + .run(item -> { + executed.add(item); + if (item >= 4) { + throw new RuntimeException("Task " + item + " fails"); + } + }); + + // Only successful tasks should be reverted + for (Integer item : reverted) { + assertTrue(executed.contains(item), + "Reverted item " + item + " was never executed"); + } + } finally { + executor.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMultipleConcurrentFailuresPct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentLinkedQueue failedItems = new ConcurrentLinkedQueue<>(); + List items = List.of(1, 2, 3, 4, 5); + + try { + new TasksBuilder<>(items) + .executeWith(executor) + .throwFailureWhenFinished(false) + .onFailure((item, exception) -> { + failedItems.add(item); + }) + .run(item -> { + if (item % 2 == 0) { + throw new RuntimeException("Even item fails"); + } + }); + + // All even items should have failed + assertTrue(failedItems.contains(2)); + assertTrue(failedItems.contains(4)); + assertFalse(failedItems.contains(1)); + assertFalse(failedItems.contains(3)); + assertFalse(failedItems.contains(5)); + } finally { + executor.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testRetryMechanismWithParallelExecutionPct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentHashMap attemptCounts = new ConcurrentHashMap<>(); + List items = List.of(1, 2, 3); + + for (int i : items) { + attemptCounts.put(i, new AtomicInteger(0)); + } + + try { + boolean result = new TasksBuilder<>(items) + .executeWith(executor) + .retry(2) + .throwFailureWhenFinished(false) + .run(item -> { + int attempt = attemptCounts.get(item).incrementAndGet(); + if (item == 2 && attempt < 2) { + throw new RuntimeException("Task 2 fails on attempt " + attempt); + } + }); + + assertTrue(result); + assertEquals(1, attemptCounts.get(1).get()); + assertEquals(2, attemptCounts.get(2).get()); + assertEquals(1, attemptCounts.get(3).get()); + } finally { + executor.shutdown(); + } + } + + /** + * PCT variant of {@link #testStopAbortsOnFailureFlag()}. + * TODO This needs JmcAtomicBoolean.getAndSet(boolean), currently throws NoSuchMEthodException + */ + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + @Disabled + public void testStopAbortsOnFailureFlagPct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentLinkedQueue aborted = new ConcurrentLinkedQueue<>(); + AtomicBoolean firstAbortFailed = new AtomicBoolean(false); + List items = List.of(1, 2, 3, 4, 5); + + try { + new TasksBuilder<>(items) + .executeWith(executor) + .stopOnFailure() + .stopAbortsOnFailure() + .throwFailureWhenFinished(false) + .abortWith(item -> { + aborted.add(item); + if (item == 3 && !firstAbortFailed.getAndSet(true)) { + throw new RuntimeException("Abort fails for item 3"); + } + }) + .run(item -> { + if (item == 1) { + throw new RuntimeException("Task 1 fails"); + } + }); + + // With stopAbortsOnFailure, aborts should stop after first failure + assertTrue(aborted.size() <= items.size()); + } finally { + executor.shutdown(); + } + } + + /** + * PCT variant of {@link #testStopRevertsOnFailureFlag()}. + * TODO This needs JmcAtomicBoolean.getAndSet(boolean), currently throws NoSuchMEthodException + */ + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + @Disabled + public void testStopRevertsOnFailureFlagPct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentLinkedQueue reverted = new ConcurrentLinkedQueue<>(); + AtomicBoolean firstRevertFailed = new AtomicBoolean(false); + List items = List.of(1, 2, 3, 4, 5); + + try { + new TasksBuilder<>(items) + .executeWith(executor) + .stopOnFailure() + .stopRevertsOnFailure() + .throwFailureWhenFinished(false) + .revertWith(item -> { + reverted.add(item); + if (item == 2 && !firstRevertFailed.getAndSet(true)) { + throw new RuntimeException("Revert fails for item 2"); + } + }) + .run(item -> { + if (item >= 4) { + throw new RuntimeException("Task " + item + " fails"); + } + }); + + // With stopRevertsOnFailure, reverts should stop after first failure + assertTrue(reverted.size() <= 3); + } finally { + executor.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testFutureGetVisibilityPct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentLinkedQueue completed = new ConcurrentLinkedQueue<>(); + List items = List.of(1, 2, 3, 4, 5); + + try { + boolean result = new TasksBuilder<>(items) + .executeWith(executor) + .throwFailureWhenFinished(false) + .run(item -> { + completed.add(item); + }); + + assertTrue(result); + // All items should be visible after Future.get() returns + assertEquals(5, completed.size()); + for (int i = 1; i <= 5; i++) { + assertTrue(completed.contains(i), "Item " + i + " not found in completed queue"); + } + } finally { + executor.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testComplexScenarioAllFeaturesPct() { + ExecutorService executor = Executors.newFixedThreadPool(3); + ConcurrentLinkedQueue executed = new ConcurrentLinkedQueue<>(); + ConcurrentLinkedQueue failed = new ConcurrentLinkedQueue<>(); + ConcurrentLinkedQueue aborted = new ConcurrentLinkedQueue<>(); + ConcurrentLinkedQueue reverted = new ConcurrentLinkedQueue<>(); + ConcurrentHashMap attempts = new ConcurrentHashMap<>(); + List items = List.of(1, 2, 3, 4, 5); + + for (int i : items) { + attempts.put(i, new AtomicInteger(0)); + } + + try { + new TasksBuilder<>(items) + .executeWith(executor) + .stopOnFailure() + .retry(1) + .throwFailureWhenFinished(false) + .onFailure((item, exception) -> { + failed.add(item); + }) + .abortWith(item -> { + aborted.add(item); + }) + .revertWith(item -> { + reverted.add(item); + }) + .run(item -> { + int attempt = attempts.get(item).incrementAndGet(); + executed.add(item); + + // Item 3 fails even after retry + if (item == 3) { + throw new RuntimeException("Task 3 always fails"); + } + }); + + // Verify invariants + assertTrue(failed.contains(3), "Task 3 should have failed"); + + // No item should be both executed successfully and aborted + for (Integer item : executed) { + if (!failed.contains(item)) { + assertFalse(aborted.contains(item), + "Item " + item + " was both successful and aborted"); + } + } + + // Only successful tasks should be reverted + for (Integer item : reverted) { + assertTrue(executed.contains(item), + "Reverted item " + item + " was never executed"); + assertFalse(failed.contains(item), + "Reverted item " + item + " was marked as failed"); + } + } finally { + executor.shutdown(); + } + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergThreadPoolsTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergThreadPoolsTest.java index d78e8d5c..47943b29 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergThreadPoolsTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergThreadPoolsTest.java @@ -419,4 +419,348 @@ public void testNewExitingWorkerPool() { pool.shutdown(); } } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testConcurrentWorkerPoolAccessPct() { + ExecutorService executor = Executors.newFixedThreadPool(10); + ExecutorService pool = ThreadPools.getWorkerPool(); + AtomicInteger counter = new AtomicInteger(0); + List> futures = new ArrayList<>(); + + // Submit tasks from multiple threads concurrently + for (int i = 0; i < 10; i++) { + futures.add(pool.submit(() -> { + //System.out.println("Thread: " + Thread.currentThread().getName() + " - inside submit"); + return counter.incrementAndGet(); + })); + } + + // Wait for all tasks + int sum = 0; + for (Future future : futures) { + try { + sum += future.get(); + } catch (Exception e) { + fail("Task execution failed: " + e.getMessage()); + } + } + //ThreadPools.shutdownAll(); + + //assert(sum > 0); + assertEquals(10, counter.get()); + assertTrue(sum > 0); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testConcurrentDeleteWorkerPoolAccessPct() { + ExecutorService pool = ThreadPools.getDeleteWorkerPool(); + ConcurrentLinkedQueue results = new ConcurrentLinkedQueue<>(); + List> futures = new ArrayList<>(); + + for (int i = 0; i < 8; i++) { + final int value = i; + futures.add(pool.submit(() -> { + results.add(value); + })); + } + + for (Future future : futures) { + try { + future.get(); + } catch (Exception e) { + fail("Task execution failed: " + e.getMessage()); + } + } + + assertEquals(8, results.size()); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testScheduledPoolConcurrentSchedulingPct() { + ScheduledExecutorService pool = ThreadPools.authRefreshPool(); + AtomicInteger counter = new AtomicInteger(0); + List> futures = new ArrayList<>(); + + // Schedule multiple tasks with minimal delay + for (int i = 0; i < 5; i++) { + futures.add(pool.schedule(() -> { + counter.incrementAndGet(); + }, 1, TimeUnit.MILLISECONDS)); + } + + // Wait for all scheduled tasks + for (ScheduledFuture future : futures) { + try { + future.get(100, TimeUnit.MILLISECONDS); + } catch (Exception e) { + fail("Scheduled task failed: " + e.getMessage()); + } + } + pool.shutdown(); + + assertEquals(5, counter.get()); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testConcurrentPoolCreationPct() throws Exception { + ConcurrentLinkedQueue pools = new ConcurrentLinkedQueue<>(); + List> futures = new ArrayList<>(); + ExecutorService coordinator = Executors.newFixedThreadPool(3); + + try { + for (int i = 0; i < 3; i++) { + futures.add(coordinator.submit(() -> { + ExecutorService pool = ThreadPools.newFixedThreadPool("test-pool", 2); + pools.add(pool); + })); + } + + for (Future future : futures) { + future.get(); + } + + assertEquals(3, pools.size()); + + // Cleanup + for (ExecutorService pool : pools) { + pool.shutdown(); + } + } finally { + coordinator.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testFutureGetVisibilityPct() { + ExecutorService pool = ThreadPools.getWorkerPool(); + ConcurrentHashMap results = new ConcurrentHashMap<>(); + List> futures = new ArrayList<>(); + + for (int i = 0; i < 10; i++) { + final int key = i; + futures.add(pool.submit(() -> { + results.put(key, key * 2); + })); + } + + // Wait for all tasks + for (Future future : futures) { + try { + future.get(); + } catch (Exception e) { + fail("Task failed: " + e.getMessage()); + } + } + + // Verify all results are visible + assertEquals(10, results.size()); + for (int i = 0; i < 10; i++) { + assertTrue(results.containsKey(i), "Missing key: " + i); + assertEquals(i * 2, results.get(i)); + } + } + + /** + * PCT variant of {@link #testScheduledFixedDelay()}. + */ + // TODO :: Fix this test + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + @JmcExpectAssertionFailure + @Disabled + public void testScheduledFixedDelayPct() { + ScheduledExecutorService pool = ThreadPools.newScheduledPool("test-scheduled", 2); + AtomicInteger counter = new AtomicInteger(0); + AtomicBoolean running = new AtomicBoolean(true); + + try { + ScheduledFuture future = pool.scheduleWithFixedDelay(() -> { + if (running.get()) { + counter.incrementAndGet(); + } + }, 0, 1, TimeUnit.MILLISECONDS); + + // Let it run briefly + Thread.sleep(5); + running.set(false); + future.cancel(false); + + assertTrue(counter.get() > 0, "Scheduled task should have run at least once"); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + fail("Test interrupted"); + } finally { + pool.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMultiplePoolsConcurrentAccessPct() { + ExecutorService workerPool = ThreadPools.getWorkerPool(); + ExecutorService deletePool = ThreadPools.getDeleteWorkerPool(); + + AtomicInteger workerCounter = new AtomicInteger(0); + AtomicInteger deleteCounter = new AtomicInteger(0); + + List> futures = new ArrayList<>(); + + // Submit to worker pool + for (int i = 0; i < 5; i++) { + futures.add(workerPool.submit(() -> { + workerCounter.incrementAndGet(); + })); + } + + // Submit to delete pool + for (int i = 0; i < 5; i++) { + futures.add(deletePool.submit(() -> { + deleteCounter.incrementAndGet(); + })); + } + + // Wait for all + for (Future future : futures) { + try { + future.get(); + } catch (Exception e) { + fail("Task failed: " + e.getMessage()); + } + } + + assertEquals(5, workerCounter.get()); + assertEquals(5, deleteCounter.get()); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testConcurrentExceptionHandlingPct() { + ExecutorService pool = ThreadPools.getWorkerPool(); + AtomicInteger successCount = new AtomicInteger(0); + List> futures = new ArrayList<>(); + + for (int i = 0; i < 10; i++) { + final int value = i; + futures.add(pool.submit(() -> { + if (value == 5) { + throw new RuntimeException("Task 5 fails"); + } + successCount.incrementAndGet(); + })); + } + + int exceptions = 0; + for (Future future : futures) { + try { + future.get(); + } catch (ExecutionException e) { + exceptions++; + } catch (Exception e) { + fail("Unexpected exception: " + e.getMessage()); + } + } + + assertEquals(1, exceptions); + assertEquals(9, successCount.get()); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testCallableTasksWithResultsPct() { + ExecutorService pool = ThreadPools.getWorkerPool(); + List> futures = new ArrayList<>(); + + for (int i = 0; i < 10; i++) { + final int value = i; + futures.add(pool.submit(() -> value * value)); + } + + List results = new ArrayList<>(); + for (Future future : futures) { + try { + results.add(future.get()); + } catch (Exception e) { + fail("Task failed: " + e.getMessage()); + } + } + + assertEquals(10, results.size()); + assertTrue(results.contains(0)); // 0*0 + assertTrue(results.contains(1)); // 1*1 + assertTrue(results.contains(81)); // 9*9 + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + @Disabled + // TODO :: Investigate this test + public void testScheduledTaskCancellationPct() { + ScheduledExecutorService pool = ThreadPools.newScheduledPool("test-cancel", 2); + AtomicInteger counter = new AtomicInteger(0); + + try { + List> futures = new ArrayList<>(); + + // Schedule multiple tasks + for (int i = 0; i < 5; i++) { + futures.add(pool.schedule(() -> { + counter.incrementAndGet(); + }, 10, TimeUnit.MILLISECONDS)); + } + + // Cancel some tasks immediately + futures.get(0).cancel(false); + futures.get(2).cancel(false); + + // Wait for non-cancelled tasks + try { + futures.get(1).get(); + futures.get(3).get(); + futures.get(4).get(); + } catch (CancellationException e) { + // Expected for cancelled tasks + } + + // Counter should be less than 5 due to cancellations + assertTrue(counter.get() <= 5); + assertTrue(counter.get() >= 3); + } catch (Exception e) { + fail("Test failed: " + e.getMessage()); + } finally { + pool.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testNewExitingWorkerPoolPct() { + ExecutorService pool = ThreadPools.newExitingWorkerPool("test-exiting", 3); + AtomicInteger counter = new AtomicInteger(0); + List> futures = new ArrayList<>(); + + try { + for (int i = 0; i < 10; i++) { + futures.add(pool.submit(() -> { + counter.incrementAndGet(); + })); + } + + for (Future future : futures) { + try { + future.get(); + } catch (Exception e) { + fail("Task failed: " + e.getMessage()); + } + } + + assertEquals(10, counter.get()); + } finally { + pool.shutdown(); + } + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynFutureExecutorTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynFutureExecutorTest.java index fefc1c6d..72c93335 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynFutureExecutorTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynFutureExecutorTest.java @@ -137,6 +137,7 @@ public void testFuture_seq() throws Exception { @JmcCheck @JmcCheckConfiguration(numIterations = 10) + // TODO :: There is an unknown exception in the agent public void testExecutor_seq() throws Exception { executor_seq(); } @@ -153,6 +154,31 @@ public void testFuture_par() throws Exception { future_par(); } + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testFuture_seqPct() throws Exception { + future_seq(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + // TODO :: There is an unknown exception in the agent + public void testExecutor_seqPct() throws Exception { + executor_seq(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testFutureNested_seqPct() throws Exception { + futureNested_seq(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testFuture_parPct() throws Exception { + future_par(); + } + /* @JmcCheck @JmcCheckConfiguration(numIterations = 10) public void testExecutor_par() throws Exception { diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynamicTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynamicTest.java index b37ba7a2..132eda0b 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynamicTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynamicTest.java @@ -179,4 +179,34 @@ public void testReentrantLock_par() { public void testSynchronizedBlock_seq() { synchronizedBlock_seq(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testAtomicInteger_seqPct() { + atomicInteger_seq(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testReentrantLock_seqPct() { + reentrantLock_seq(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testLockAtomic_seqPct() { + lockAtomic_seq(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testReentrantLock_parPct() { + reentrantLock_par(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testSynchronizedBlock_seqPct() { + synchronizedBlock_seq(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/NestedExecutorJoinTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/NestedExecutorJoinTest.java index cbf37ca2..4415cb53 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/NestedExecutorJoinTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/NestedExecutorJoinTest.java @@ -61,4 +61,44 @@ public void testNestedExecutorPattern() throws Exception { mainExecutor.shutdown(); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testNestedExecutorPatternPct() throws Exception { + final ExecutorService WORKER_POOL = Executors.newFixedThreadPool(2); + + // Main executor (like the one created in the test) + ExecutorService mainExecutor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Submit 3 tasks that each use the worker pool internally + for (int i = 0; i < 3; i++) { + final int taskId = i; + futures.add(mainExecutor.submit(() -> { + + // Each task submits work to the shared worker pool + List> workerFutures = new ArrayList<>(); + for (int j = 0; j < 2; j++) { + final int workerId = j; + workerFutures.add(WORKER_POOL.submit(() -> { + return "result-" + taskId + "-" + workerId; + })); + } + + // Wait for worker tasks + for (Future wf : workerFutures) { + wf.get(); + } + + return taskId; + })); + } + + // Main thread waits for all tasks + for (int i = 0; i < futures.size(); i++) { + Integer result = futures.get(i).get(); + } + + mainExecutor.shutdown(); + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedTest.java index dcd1d07b..af173969 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedTest.java @@ -37,6 +37,48 @@ public void testNestedYieldInHashCode() throws InterruptedException { }); + Thread t2 = new Thread(() -> { + int hash = container.computeHash(); + + if (hash < 0) { + System.out.println("Unexpected"); + } + }); + + t1.start(); + t2.start(); + t1.join(); + t2.join(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testNestedYieldInHashCodePct() throws InterruptedException { + Container container = new Container(); + + + Item i = new Item(1); + container.addItem(i); + Item i2 = new Item(2); + container.addItem(i2); + i = new Item(3); + container.addItem(i); + + if (!i.equals(i2)) { + System.out.println("Unexpected equality"); + System.out.println(i.hashCode()); + } + + + Thread t1 = new Thread(() -> { + int hash = container.computeHash(); + + if (hash < 0) { + System.out.println("Unexpected"); + } + }); + + Thread t2 = new Thread(() -> { int hash = container.computeHash(); diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedYieldTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedYieldTest.java index e3124e30..2f4dde2d 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedYieldTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedYieldTest.java @@ -65,6 +65,41 @@ public void testNestedYieldInHashCode() throws InterruptedException { container.addItem(new Item(3)); + Thread t1 = new Thread(() -> { + int hash = container.computeHash(); + + if (hash < 0) { + //System.out.println("Unexpected"); + } + }); + + Thread t2 = new Thread (() -> { + int hash = container.computeHash(); + + if (hash < 0) { + //System.out.println("Unexpected"); + } + }); + t1.start(); + t2.start(); + t1.join(); + t2.join(); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testNestedYieldInHashCodePct() throws InterruptedException { + + + Container container = new Container(); + + container.addItem(new Item(1)); + + container.addItem(new Item(2)); + + container.addItem(new Item(3)); + + Thread t1 = new Thread(() -> { int hash = container.computeHash(); diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/SimpleScheduledExecutorTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/SimpleScheduledExecutorTest.java index 3906e90d..46497396 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/SimpleScheduledExecutorTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/SimpleScheduledExecutorTest.java @@ -81,4 +81,71 @@ public void testMultipleScheduledTasks() throws Exception { pool.shutdown(); } } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testSimpleSchedulePct() throws Exception { + ScheduledExecutorService pool = Executors.newScheduledThreadPool(1); + AtomicInteger counter = new AtomicInteger(0); + + try { + ScheduledFuture future = pool.schedule(() -> { + counter.incrementAndGet(); + }, 0, TimeUnit.MILLISECONDS); + + // Wait for task to complete + future.get(); + + assertEquals(1, counter.get(), "Task should have run exactly once"); + } finally { + pool.shutdown(); + } + } + + // TODO: Fix the following test + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + @JmcExpectAssertionFailure + @Disabled + public void testScheduleWithFixedDelayRunsOncePct() throws Exception { + ScheduledExecutorService pool = Executors.newScheduledThreadPool(1); + AtomicInteger counter = new AtomicInteger(0); + + try { + ScheduledFuture future = pool.scheduleWithFixedDelay(() -> { + counter.incrementAndGet(); + }, 0, 1, TimeUnit.MILLISECONDS); + + // In JMC, periodic tasks run once, so we can wait for completion + // But periodic tasks don't complete, so we need to cancel and check + Thread.yield(); // Give the task a chance to run + Thread.yield(); + Thread.yield(); + + future.cancel(false); + + assertTrue(counter.get() >= 1, "Task should have run at least once, got: " + counter.get()); + } finally { + pool.shutdown(); + } + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMultipleScheduledTasksPct() throws Exception { + ScheduledExecutorService pool = Executors.newScheduledThreadPool(2); + AtomicInteger counter = new AtomicInteger(0); + + try { + ScheduledFuture future1 = pool.schedule(() -> counter.incrementAndGet(), 0, TimeUnit.MILLISECONDS); + ScheduledFuture future2 = pool.schedule(() -> counter.incrementAndGet(), 0, TimeUnit.MILLISECONDS); + + future1.get(); + future2.get(); + + assertEquals(2, counter.get(), "Both tasks should have run"); + } finally { + pool.shutdown(); + } + } } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticSynchronizedMethodTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticSynchronizedMethodTest.java index 66d9350d..c0326afb 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticSynchronizedMethodTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticSynchronizedMethodTest.java @@ -16,6 +16,13 @@ public void testStaticSynchronizedMethod() { String result = TestClass.getOrCreateValue(); } + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, strategy = "pct", timeout = 10000L) + public void testStaticSynchronizedMethodPct() { + // Call a static synchronized method + String result = TestClass.getOrCreateValue(); + } + /** * Test class with a static synchronized method, similar to HadoopTables. * No explicit static initializer block. diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticThreadPoolLeakTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticThreadPoolLeakTest.java index ef86fd40..45224f72 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticThreadPoolLeakTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticThreadPoolLeakTest.java @@ -146,5 +146,77 @@ public void testMultipleEagerPoolsLeak() throws Exception { ThreadMXBean threadBean = ManagementFactory.getThreadMXBean(); } + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testEagerInitializationLeakPct() throws Exception { + // Get the thread pool (will be a DIFFERENT instance each iteration) + ExecutorService pool = EagerThreadPool.getPool(); + + // Submit a simple task + Future future = pool.submit(() -> { + return 42; + }); + + // Wait for result + assertEquals(42, future.get()); + + // Print thread count to see it growing + ThreadMXBean threadBean = ManagementFactory.getThreadMXBean(); + int threadCount = threadBean.getThreadCount(); + + // With eager initialization, thread count keeps growing! + // Iteration 1: ~10 threads + // Iteration 10: ~30 threads + // Iteration 1000: OutOfMemoryError! + } + + /** + * PCT variant of {@link #testLazyInitializationNoLeak()}. + */ + // TODO :: Investigate and fix the hang + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + @Disabled + public void testLazyInitializationNoLeakPct() throws Exception { + // Get the thread pool (will be the SAME instance each iteration) + ExecutorService pool = LazyThreadPool.getPool(); + + // Submit a simple task + Future future = pool.submit(() -> { + return 42; + }); + + // Wait for result + assertEquals(42, future.get()); + + // With lazy initialization, thread count stays stable! + // All iterations: ~10-15 threads (stable) + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMultipleEagerPoolsLeakPct() throws Exception { + // Each of these creates a NEW pool on every iteration + ExecutorService pool1 = Executors.newFixedThreadPool(2); + ExecutorService pool2 = Executors.newFixedThreadPool(2); + ExecutorService pool3 = Executors.newFixedThreadPool(2); + + // Submit tasks + Future f1 = pool1.submit(() -> 1); + Future f2 = pool2.submit(() -> 2); + Future f3 = pool3.submit(() -> 3); + + assertEquals(1, f1.get()); + assertEquals(2, f2.get()); + assertEquals(3, f3.get()); + + // This creates 6 threads per iteration + // After 10 iterations: 60 threads + // After 100 iterations: 600 threads + // After 1000 iterations: OutOfMemoryError! + + ThreadMXBean threadBean = ManagementFactory.getThreadMXBean(); + } + } diff --git a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ThreadPoolReadWriteInteractionTest.java b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ThreadPoolReadWriteInteractionTest.java index c8f0d756..2473ae8c 100644 --- a/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ThreadPoolReadWriteInteractionTest.java +++ b/integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ThreadPoolReadWriteInteractionTest.java @@ -310,4 +310,152 @@ public void testStressThreadPoolWithManyOperations() throws Exception { int finalCounter = store.getCounter(); assertEquals(10, finalCounter); } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testMinimalThreadPoolWithFieldAccessPct() throws Exception { + SharedDataStore store = new SharedDataStore(); + + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Submit 2 tasks that access shared fields + for (int i = 0; i < 2; i++) { + final int taskId = i; + Future future = executor.submit(() -> { + store.performOperation("task-" + taskId); + return taskId; + }); + futures.add(future); + } + + // Wait for completion + for (Future f : futures) { + f.get(); + } + + executor.shutdown(); + + // Verify results + int finalCounter = store.getCounter(); + assertEquals(2, finalCounter); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testThreadPoolWithMultipleFieldAccessesPct() throws Exception { + SharedDataStore store = new SharedDataStore(); + + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Each task performs multiple operations + for (int i = 0; i < 2; i++) { + final int taskId = i; + Future future = executor.submit(() -> { + for (int j = 0; j < 3; j++) { + store.performOperation("task-" + taskId + "-op-" + j); + // Read operations to trigger more yields + int counter = store.getCounter(); + String lastOp = store.getLastOperation(); + } + return null; + }); + futures.add(future); + } + + // Wait for completion + for (Future f : futures) { + f.get(); + } + + executor.shutdown(); + + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testThreadPoolWithNestedFieldAccessesPct() throws Exception { + NestedDataStructure data = new NestedDataStructure(); + + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + for (int i = 0; i < 2; i++) { + final int taskId = i; + Future future = executor.submit(() -> { + data.performNestedOperation(taskId); + return null; + }); + futures.add(future); + } + + for (Future f : futures) { + f.get(); + } + + executor.shutdown(); + + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testIcebergLikeCommitPatternPct() throws Exception { + CatalogSimulator catalog = new CatalogSimulator(); + + ExecutorService executor = Executors.newFixedThreadPool(2); + List> futures = new ArrayList<>(); + + // Simulate concurrent commits + for (int i = 0; i < 3; i++) { + final int fileId = i; + Future future = executor.submit(() -> { + boolean success = catalog.commit(fileId); + return success; + }); + futures.add(future); + } + + // Wait for all commits + int successCount = 0; + for (Future f : futures) { + if (f.get()) { + successCount++; + } + } + + executor.shutdown(); + + assertEquals(3, successCount); + } + + @JmcCheck + @JmcCheckConfiguration(numIterations = 10, debug = false, strategy = "pct", timeout = 10000L) + public void testStressThreadPoolWithManyOperationsPct() throws Exception { + SharedDataStore store = new SharedDataStore(); + + ExecutorService executor = Executors.newFixedThreadPool(3); + List> futures = new ArrayList<>(); + + // Submit many tasks + for (int i = 0; i < 5; i++) { + final int taskId = i; + Future future = executor.submit(() -> { + for (int j = 0; j < 2; j++) { + store.performOperation("task-" + taskId + "-" + j); + } + return null; + }); + futures.add(future); + } + + for (Future f : futures) { + f.get(); + } + + executor.shutdown(); + + int finalCounter = store.getCounter(); + assertEquals(10, finalCounter); + } }