diff --git a/core/src/main/java/org/mpi_sws/jmc/api/util/concurrent/JmcThread.java b/core/src/main/java/org/mpi_sws/jmc/api/util/concurrent/JmcThread.java index 0d806813..2e427efe 100644 --- a/core/src/main/java/org/mpi_sws/jmc/api/util/concurrent/JmcThread.java +++ b/core/src/main/java/org/mpi_sws/jmc/api/util/concurrent/JmcThread.java @@ -232,7 +232,7 @@ public void join1(Long millis) throws InterruptedException { } catch (HaltTaskException e) { LOGGER.error("Failed to join task : {}", e.getMessage()); } - super.join(millis); + JmcRuntime.waitForTaskTermination(jmcThreadId); JmcRuntimeEvent completedEvent = new JmcRuntimeEvent.Builder() .type(JmcRuntimeEvent.Type.JOIN_COMPLETE_EVENT) 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..6157026c 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 @@ -199,6 +199,23 @@ public static void pause(Long taskId) { } } + /** + * Cooperatively waits until the task with the given ID is terminated. + * + *

Unlike {@link Thread#join()}, this keeps the waiting task in the scheduler's task pool so + * {@link TaskManager#stopTask(Long)} can interrupt it during stop-all (e.g. trust-estimation + * re-execution). A native join would block the OS thread outside JMC's pause/resume machinery. + */ + public static void waitForTaskTermination(Long taskId) { + while (true) { + TaskManager.TaskState status = taskManager.getStatus(taskId); + if (status == null || status == TaskManager.TaskState.TERMINATED) { + return; + } + JmcRuntime.yield(); + } + } + public static T wait(Long taskId) { try { return taskManager.wait(taskId); 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..9dd180c2 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 @@ -161,8 +161,9 @@ private void startStopAllMode() { 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("No pausable tasks remain in stop-all mode; exiting."); + stopAllMode = false; + return; } setCurrentTask(taskId); taskManager.stopTask(taskId); @@ -194,18 +195,15 @@ public void updateEvent(JmcRuntimeEvent event) throws HaltTaskException { * @throws TaskAlreadyPaused if the current task is already paused */ public CompletableFuture yield() throws TaskAlreadyPaused { - if (!isInStopAllMode()) { - CompletableFuture future; - synchronized (currentTaskLock) { - future = taskManager.pause(currentTask); - currentTask = null; - } - // Release the scheduler thread - LOGGER.debug("Enabling scheduler thread."); - schedulerThread.enable(); - return future; + CompletableFuture future; + synchronized (currentTaskLock) { + future = taskManager.pause(currentTask); + currentTask = null; } - return null; + // Release the scheduler thread + LOGGER.debug("Enabling scheduler thread."); + schedulerThread.enable(); + return future; } public void yieldWithoutPausing() { @@ -227,17 +225,14 @@ public void yieldWithoutPausing() { * @throws TaskAlreadyPaused if the task is already paused */ public CompletableFuture yield(Long taskId) throws TaskAlreadyPaused { - if (!isInStopAllMode()) { - CompletableFuture future = taskManager.pause(taskId); - synchronized (currentTaskLock) { - currentTask = null; - } - // Release the scheduler thread - LOGGER.debug("Enabling scheduler thread."); - schedulerThread.enable(); - return future; + CompletableFuture future = taskManager.pause(taskId); + synchronized (currentTaskLock) { + currentTask = null; } - return null; + // Release the scheduler thread + LOGGER.debug("Enabling scheduler thread."); + schedulerThread.enable(); + return future; } /** @@ -271,6 +266,20 @@ public boolean isInStopAllMode() { return stopAllMode; } + /** + * When the strategy returns no choice but tasks are paused on the scheduler, resume one so + * exploration can continue. This avoids a global stall when every live task is blocked in + * {@link TaskManager#pause(Long)} waiting for a scheduling decision. + */ + Long resumeBlockedTaskIfNeeded() { + for (Long taskId : taskManager.findTasksWithStatus(TaskManager.TaskState.BLOCKED)) { + LOGGER.debug("Resuming blocked task {} because the strategy returned no choice.", taskId); + scheduleTask(SchedulingChoice.task(taskId)); + return taskId; + } + return null; + } + /** * The SchedulerThread class is responsible for scheduling the tasks. */ @@ -377,10 +386,15 @@ public void run() { if (nextTask != null) { scheduler.scheduleTask(nextTask); } else { - LOGGER.error("No task to schedule."); + Long blockedTask = scheduler.resumeBlockedTaskIfNeeded(); + if (blockedTask == null) { + LOGGER.error("No task to schedule."); + } } + } catch (HaltExecutionException e) { + LOGGER.debug("Scheduler thread halt: {}", e.getMessage()); } catch (Exception e) { - LOGGER.error("Scheduler thread threw an exception: {}", e.getMessage()); + LOGGER.error("Scheduler thread threw an exception: {}", e.getMessage(), e); break; } } 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..22e12afb 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 @@ -160,6 +160,9 @@ private SolverResult extractSolverResult(SchedulingChoice choice) { * @param task scheduling choice to update its value */ public void updateExternalValue(SchedulingChoice task) { + if (task.getTaskId() == null) { + return; + } // Since the task we receive is from runtime, the task id must be treated adjusted in algo long id = task.getTaskId() - 1; if (externalValueTracker.containsValue(id)) { diff --git a/core/src/main/java/org/mpi_sws/jmc/strategies/trust/ExecutionGraph.java b/core/src/main/java/org/mpi_sws/jmc/strategies/trust/ExecutionGraph.java index bb28808d..18bdcf63 100644 --- a/core/src/main/java/org/mpi_sws/jmc/strategies/trust/ExecutionGraph.java +++ b/core/src/main/java/org/mpi_sws/jmc/strategies/trust/ExecutionGraph.java @@ -426,6 +426,11 @@ public void trackThreadCreates(ExecutionGraphNode node) { // Tracking thread starts in the coherency order with a special static location object. List threadStarts = coherencyOrder.get(LocationStore.ThreadLocation); + if (threadStarts == null || threadStarts.isEmpty()) { + threadStarts = new ArrayList<>(); + threadStarts.add(allEvents.get(0)); + coherencyOrder.put(LocationStore.ThreadLocation, threadStarts); + } ExecutionGraphNode lastThreadStart = threadStarts.get(threadStarts.size() - 1); lastThreadStart.addEdge(node, Relation.ThreadCreation); coherencyOrder.get(LocationStore.ThreadLocation).add(node); 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..f24a30c3 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 @@ -122,6 +122,13 @@ public SchedulingChoice nextTask() { // If the algorithm has a task to execute, return it SchedulingChoice nextTask = algoInstance.nextTask(); if (nextTask != null) { + if (nextTask.isBlockExecution() || nextTask.isBlockTask()) { + return nextTask; + } + if (nextTask.getTaskId() == null) { + LOGGER.debug("Guiding trace returned a scheduling choice without a task id: {}", nextTask); + return null; + } if (!activeTasks.contains(nextTask.getTaskId())) { LOGGER.debug("Guiding trace led us to a task that is not active: {}", nextTask); } @@ -137,25 +144,20 @@ public SchedulingChoice nextTask() { .filter(activeTasks::contains) .toList(); + if (activeScheduleAbleTasks.isEmpty()) { + return null; + } + // If the policy is FIFO, return the first active, schedule-able task - SchedulingChoice next = SchedulingChoice.task( + Long chosenTask = switch (policy) { - case FIFO -> activeScheduleAbleTasks.isEmpty() - ? null - : activeScheduleAbleTasks.get(0); - case LIFO -> activeScheduleAbleTasks.isEmpty() - ? null - : activeScheduleAbleTasks.get(activeScheduleAbleTasks.size() - 1); - case RANDOM -> { - int size = activeScheduleAbleTasks.size(); - yield size == 0 ? null : activeScheduleAbleTasks.get(random.nextInt(size)); - } - }); - - // Update it's value based on value tracker in the algo - if (next != null) { - algoInstance.updateExternalValue(next); - } + case FIFO -> activeScheduleAbleTasks.get(0); + case LIFO -> activeScheduleAbleTasks.get(activeScheduleAbleTasks.size() - 1); + case RANDOM -> activeScheduleAbleTasks.get(random.nextInt(activeScheduleAbleTasks.size())); + }; + + SchedulingChoice next = SchedulingChoice.task(chosenTask); + algoInstance.updateExternalValue(next); return next; }