Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
17 changes: 17 additions & 0 deletions core/src/main/java/org/mpi_sws/jmc/runtime/JmcRuntime.java
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,23 @@ public static void pause(Long taskId) {
}
}

/**
* Cooperatively waits until the task with the given ID is terminated.
*
* <p>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> T wait(Long taskId) {
try {
return taskManager.wait(taskId);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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() {
Expand All @@ -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;
}

/**
Expand Down Expand Up @@ -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.
*/
Expand Down Expand Up @@ -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;
}
}
Expand Down
3 changes: 3 additions & 0 deletions core/src/main/java/org/mpi_sws/jmc/strategies/trust/Algo.java
Original file line number Diff line number Diff line change
Expand Up @@ -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)) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -426,6 +426,11 @@ public void trackThreadCreates(ExecutionGraphNode node) {

// Tracking thread starts in the coherency order with a special static location object.
List<ExecutionGraphNode> 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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand All @@ -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;
}

Expand Down