Implementation of the probabilistic concurrent testing (pct) + Fixing data races + Editing documentation

[joulook]

No description provided.

[Copilot]

Pull request overview

This PR adds Probabilistic Concurrency Testing (PCT) scheduling to JMC (including a fair-suffix variant), updates configuration/plumbing to expose the new strategies, expands integration coverage with PCT-enabled variants of existing tests, and ports CI timeout/budget controls across GitLab and GitHub Actions.

Changes:

• Implement pct and fair-pct scheduling strategies (plus unit tests) and wire them into strategy/configuration factories and annotations.
• Extend integration tests to run many existing scenarios under PCT/fair-PCT, and document the new strategies in the README.
• Harden CI with per-test timeouts + total budget enforcement, and align GitHub Actions workflow behavior with GitLab CI.

Reviewed changes

Copilot reviewed 72 out of 72 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
README.md	Documents pct / fair-pct strategies and adds citation.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ThreadPoolReadWriteInteractionTest.java	Adds PCT variants of thread-pool stress tests.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticThreadPoolLeakTest.java	Adds PCT variants around thread-pool leak scenarios (some disabled).
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/StaticSynchronizedMethodTest.java	Adds a PCT variant for static synchronized method scenario.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/SimpleScheduledExecutorTest.java	Adds PCT variants for scheduled executor scenarios (one disabled).
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedYieldTest.java	Adds a PCT variant for nested yield/hash computation scenario.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ReadWriteNestedTest.java	Adds a PCT variant for nested read/write hash scenario.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/NestedExecutorJoinTest.java	Adds a PCT variant for nested executor/future pattern.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynFutureExecutorTest.java	Adds multiple PCT variants for invoke-dynamic future/executor tests.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/InvokeDynamicTest.java	Adds PCT variants for several invoke-dynamic scenarios.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergThreadPoolsTest.java	Adds many PCT variants targeting Iceberg thread pool patterns (some disabled).
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/IcebergTasksRunParallelTest.java	Adds many PCT variants for TasksBuilder parallel execution scenarios (some disabled).
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FinalizerThreadTest.java	Adds a PCT variant for finalizer/concurrent tasks scenario.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/FieldAccessStarvationTest.java	Adds PCT variants exploring heavy field-access patterns.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ExecutorWithoutFutureTest.java	Adjusts comment formatting and adds disabled PCT variants.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/ConcurrentStaticInitRaceTest.java	Adds several PCT variants for static-init concurrency patterns.
integration-test/src/test/java/org/mpi_sws/jmc/test/stress/BusyWaitFutureTest.java	Adds fair-PCT/PCT variants (one disabled) and import updates.
integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SynchronizedCounterTest.java	Adds PCT variants for synchronized counter programs.
integration-test/src/test/java/org/mpi_sws/jmc/test/programs/SendRecvTest.java	Adds a PCT variant for send/recv program.
integration-test/src/test/java/org/mpi_sws/jmc/test/programs/OrderedListTest.java	Adds multiple PCT variants for ordered list workloads.
integration-test/src/test/java/org/mpi_sws/jmc/test/programs/CounterTest.java	Adds PCT variants for counter programs (includes a TODO).
integration-test/src/test/java/org/mpi_sws/jmc/test/programs/BigShotTest.java	Adds PCT variants for BigShot programs (one expects failure).
integration-test/src/test/java/org/mpi_sws/jmc/test/programs/AtomicCounterTest.java	Adds a PCT variant for atomic counter.
integration-test/src/test/java/org/mpi_sws/jmc/test/programs/ArrayTest.java	Adds a PCT variant for deterministic array test.
integration-test/src/test/java/org/mpi_sws/jmc/test/features/ThreadFeaturesTest.java	Adds a PCT variant for thread feature test.
integration-test/src/test/java/org/mpi_sws/jmc/test/features/SynchronisedAnnotationTest.java	Adds a PCT variant for synchronized annotation feature.
integration-test/src/test/java/org/mpi_sws/jmc/test/features/StaticFinalFieldTest.java	Adds a PCT variant for static final field feature test.
integration-test/src/test/java/org/mpi_sws/jmc/test/features/ObjectWaitNotifyTest.java	Adds a PCT variant for wait/notify feature test.
integration-test/src/test/java/org/mpi_sws/jmc/test/features/ExpectFailureTest.java	Adds a PCT variant that expects assertion failure.
integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyTest.java	Adds a disabled PCT variant and comment formatting update.
integration-test/src/test/java/org/mpi_sws/jmc/test/features/ChannelWaitNotifyAllTest.java	Adds a PCT variant with a TODO note.
core/src/test/java/org/mpi_sws/jmc/strategies/pct/PCTSchedulingStrategyTest.java	New unit tests for PCT scheduling behavior.
core/src/test/java/org/mpi_sws/jmc/strategies/pct/FairPCTSchedulingStrategyTest.java	New unit tests for fair-PCT prefix/suffix behavior.
core/src/main/java/org/mpi_sws/jmc/strategies/ValueTracker.java	Adds clarifying docs to value tracking utility.
core/src/main/java/org/mpi_sws/jmc/strategies/trust/TrustStrategy.java	Improves debug logging message content.
core/src/main/java/org/mpi_sws/jmc/strategies/trust/Algo.java	Adds debug/error logging around external value tracking and symbolic events.
core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackWaitNotify.java	Adds documentation for wait/notify tracking.
core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackTasks.java	Adds documentation and clarifies internal locking.
core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackStaticInit.java	Adds documentation for static-init tracking.
core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackLocks.java	Adds documentation for lock tracking operations.
core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackExecutors.java	Documents and implements executor registration + forced shutdown on reset.
core/src/main/java/org/mpi_sws/jmc/strategies/tracker/Tracker.java	Clarifies tracker contract in Javadoc.
core/src/main/java/org/mpi_sws/jmc/strategies/tracker/TrackActiveTasksStrategy.java	Documents tracker intersection model and default tracker set.
core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyFactory.java	Adds pct / fair-pct strategy creation and validation.
core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategyConfiguration.java	Adds config fields + builder methods for PCT bug depth and fair bound.
core/src/main/java/org/mpi_sws/jmc/strategies/SchedulingStrategy.java	Updates interface Javadoc to match runtime threading model.
core/src/main/java/org/mpi_sws/jmc/strategies/ReplayableSchedulingStrategy.java	Expands replay interface documentation.
core/src/main/java/org/mpi_sws/jmc/strategies/RandomSchedulingStrategy.java	Adds extensive documentation and clarifies replay/trace behavior.
core/src/main/java/org/mpi_sws/jmc/strategies/pct/PCTSchedulingStrategy.java	New PCT strategy implementation (priority scheduler + change points).
core/src/main/java/org/mpi_sws/jmc/strategies/pct/FairPCTSchedulingStrategy.java	New fair-PCT wrapper (PCT prefix + random suffix).
core/src/main/java/org/mpi_sws/jmc/strategies/JmcReplayUnsupported.java	Adds constructor documentation.
core/src/main/java/org/mpi_sws/jmc/strategies/JmcInvalidStrategyException.java	Adds constructor documentation.
core/src/main/java/org/mpi_sws/jmc/runtime/TaskManager.java	Changes future lifecycle handling and adds logging/docs.
core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValueFactory.java	Documents adapter lookup and errors.
core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoiceValue.java	Clarifies purpose and adapter requirement in Javadoc.
core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/SchedulingChoice.java	Adds field-level docs and improves toString docs.
core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/Scheduler.java	Adds docs/logging for scheduling and stop-all behavior.
core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValueAdapter.java	Clarifies adapter behavior in docs.
core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/PrimitiveValue.java	Adds docs for accessors and serialization/type tagging.
core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValueAdapter.java	Clarifies adapter behavior in docs.
core/src/main/java/org/mpi_sws/jmc/runtime/scheduling/ObjectValue.java	Adds docs for wrapped object and serialization/type tagging.
core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeUtils.java	Adds documentation for runtime utilities and static-init invocation.
core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeEvent.java	Expands event documentation and builder docs.
core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntimeConfiguration.java	Documents runtime configuration fields and builder.
core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntime.java	Adds documentation for setup/replay/iteration lifecycle and yielding.
core/src/main/java/org/mpi_sws/jmc/runtime/HaltTaskException.java	Adds documentation for halt reasons and helpers.
core/src/main/java/org/mpi_sws/jmc/runtime/HaltExecutionException.java	Adds documentation and clarifies halt reasons.
core/src/main/java/org/mpi_sws/jmc/runtime/HaltCheckerException.java	Adds documentation for flags/constructors.
core/src/main/java/org/mpi_sws/jmc/checker/JmcCheckerConfiguration.java	Wires PCT params into runtime configuration and annotation parsing.
core/src/main/java/org/mpi_sws/jmc/annotations/JmcCheckConfiguration.java	Adds bugDepth and pctFairBound annotation parameters and docs.
.gitlab-ci.yml	Adds test-stage hard timeout and per-test/total-budget guards; expands publish rules.
.github/workflows/gradle.yml	Reworks workflow to mirror GitLab stages, adds budgets/timeouts, and adds publish job.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[joulook]

I've added a commit to address these issues.