Index

A B C D E F G H I J K L M N O P R S T U V W Y
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

A

acquireLock(Integer, Long) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

addAdditionalEvent(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

addAlias(Integer, Integer) - Method in class org.mpi_sws.jmc.strategies.trust.LocationStore

Adds an alias between the two location codes.

addAndGet(int) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger

Atomically adds the given delta to the current value and returns the updated value.

addAttribute(String, Object) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Adds an attribute to this node.

addBlockingLabel(Long) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Adds a blocking label to the execution graph.

addCo(Event) - Method in class org.mpi_sws.jmc.strategies.trust.CoverageGraph

addEdge(ExecutionGraphNode, Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Adds an edge to this node.

addEvent(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Adds an event to the execution graph.

additionalEvent() - Method in class org.mpi_sws.jmc.strategies.trust.BackwardRevisitView

addLocation(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.LocationStore

Add a location to the store.

addNewTask() - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Adds a new task to the runtime and creates a future for that task.

addNextTask() - Method in class org.mpi_sws.jmc.runtime.TaskManager

Adds a new task to the TaskManager object.

addPo(Event) - Method in class org.mpi_sws.jmc.strategies.trust.CoverageGraph

addRf(Event) - Method in class org.mpi_sws.jmc.strategies.trust.CoverageGraph

Algo - Class in org.mpi_sws.jmc.strategies.trust

Contains the core Trust algorithm implementation.

Algo() - Constructor for class org.mpi_sws.jmc.strategies.trust.Algo

Creates a new instance of the Trust algorithm.

ALL_OK - Enum constant in enum class org.mpi_sws.jmc.runtime.HaltExecutionException.Type

asBoolean() - Method in class org.mpi_sws.jmc.runtime.scheduling.PrimitiveValue

asInteger() - Method in class org.mpi_sws.jmc.runtime.scheduling.PrimitiveValue

ASSERT_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

asString() - Method in class org.mpi_sws.jmc.runtime.scheduling.PrimitiveValue

assume(boolean) - Static method in class org.mpi_sws.jmc.api.util.statements.JmcAssume

Assumes that the given condition is true.

ASSUME - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

ASSUME_BLOCKED_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

ASSUME_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

awaitTermination(long, TimeUnit) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

Waits for the executor service to terminate.

B

backEdges - Variable in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

backwardRevisit(ExecutionGraphNode, ExecutionGraph) - Static method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Creates a backward revisit item for a write revisiting a read.

BackwardRevisitView - Class in org.mpi_sws.jmc.strategies.trust

Represents a restricted view of the execution graph.

BackwardRevisitView(ExecutionGraph, ExecutionGraphNode, ExecutionGraphNode) - Constructor for class org.mpi_sws.jmc.strategies.trust.BackwardRevisitView

Creates a new backward revisit view.

BLOCK - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

BLOCKED - Enum constant in enum class org.mpi_sws.jmc.runtime.TaskManager.TaskState

blockExecution() - Static method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Creates a scheduling choice that blocks execution.

blockTask(Long) - Static method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Creates a scheduling choice that blocks a specific task.

blockTaskForLock(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

BRR - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.ExplorationStack.ItemType

build() - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

build() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration.Builder

build() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Builder

Builds the JmcRuntimeEvent object.

build() - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration.Builder

build() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder

builder() - Static method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig

Builder() - Constructor for class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

Builder() - Constructor for class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration.Builder

Builder() - Constructor for class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Builder

Builder() - Constructor for class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration.Builder

BWR - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.ExplorationStack.ItemType

C

cancel(boolean) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

Cancel the future.

CAS_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

changeReadsFrom(ExecutionGraphNode, ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Updates the reads from relation between the given read and write events.

check(JmcTestTarget) - Method in class org.mpi_sws.jmc.checker.JmcModelChecker

Checks the given test target.

checkCoherencyEdges() - Method in class org.mpi_sws.jmc.strategies.trust.Algo

checkCoherencyEdges() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

checkConsistency() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

checkConsistencyAndTopologicallySort() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

checkDanglingEdges() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

checkExtensiveConsistency() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

checkReadsFromEdges() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

checkStrategyConfig(JmcCheckerConfiguration.Builder, Class<?>, Method) - Static method in class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcDescriptorUtil

Checks the provided class and method for JMC trust strategy annotations and updates the JMC checker configuration builder accordingly.

choice() - Method in record class org.mpi_sws.jmc.strategies.trust.SchedulingChoiceWrapper

Returns the value of the choice record component.

clear() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Clears the execution graph.

clear() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Clears the stack.

clear() - Method in class org.mpi_sws.jmc.strategies.trust.LocationStore

Remove all locations from the store.

clearAliases() - Method in class org.mpi_sws.jmc.strategies.trust.LocationStore

Remove all aliases from the store.

clearSyncLocks() - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Clears all synchronization locks.

clone() - Method in class org.mpi_sws.jmc.strategies.trust.Event

Creates a clone of the event.

clone() - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

clone() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Creates a clone of the execution graph.

clone() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Constructs a new ExecutionGraphNode copying the given node.

Coherency - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Relation

compare(LamportVectorClock) - Method in class org.mpi_sws.jmc.util.LamportVectorClock

compare(LamportVectorClock.Component) - Method in class org.mpi_sws.jmc.util.LamportVectorClock.Component

compare(T) - Method in interface org.mpi_sws.jmc.util.PartialOrder

Compares two objects of type T - the current instance and the other object.

compare(T) - Method in interface org.mpi_sws.jmc.util.TotalOrder

Compares two objects of type T - the current and the other passed as argument.

compareAndSet(boolean, boolean) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicBoolean

Atomically sets the value to the given updated value if the current value is equal to the expected value.

compareAndSet(int, int) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger

Atomically sets the value to the given updated value if the current value is equal to the expected value.

compareAndSet(V, V) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReference

Constructs a new JmcAtomicReference with a null initial value.

compareAndSet(V, V, int, int) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicStampedReference

compareTo(Event.Key) - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

Component(int, LamportVectorClock) - Constructor for class org.mpi_sws.jmc.util.LamportVectorClock.Component

Constructs a new LamportVectorClock.Component with the given index and vector clock.

CON_ASSUME_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

CONSISTENCY_VIOLATION - Enum constant in enum class org.mpi_sws.jmc.runtime.HaltExecutionException.Type

contains(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.LocationStore

Returns if a location is contained in the store.

contains(Event.Key) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns true if the execution graph contains the event with the given key.

containsAlias(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.LocationStore

Returns if an alias is contained in the store.

containsType(String) - Static method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoiceValueFactory

CoverageGraph - Class in org.mpi_sws.jmc.strategies.trust

CoverageGraph() - Constructor for class org.mpi_sws.jmc.strategies.trust.CoverageGraph

create(String, JsonElement) - Static method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoiceValueFactory

create(SchedulingStrategyConfiguration) - Method in interface org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration.SchedulingStrategyConstructor

CREATED - Enum constant in enum class org.mpi_sws.jmc.runtime.TaskManager.TaskState

createSchedulingStrategy(String, SchedulingStrategyConfiguration) - Static method in class org.mpi_sws.jmc.strategies.SchedulingStrategyFactory

Creates a new scheduling strategy.

currentTask() - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Returns the current task id.

currentTask() - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Returns the ID of the current task.

D

DEADLOCK - Enum constant in enum class org.mpi_sws.jmc.runtime.HaltExecutionException.Type

debug() - Element in annotation interface org.mpi_sws.jmc.annotations.JmcCheckConfiguration

Enables debug logs and additional information based on the strategy used.

debug() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcMeasureGraphCoverage

Enable debug mode for the graph coverage measurement.

debug() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcTrustStrategy

Debug flag to enable graph logging.

debug() - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration.Builder

debug(boolean) - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

debug(boolean) - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder

debug(Boolean) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration.Builder

defaultExecutor() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture

discover(EngineDiscoveryRequest, UniqueId) - Method in class org.mpi_sws.jmc.integrations.junit5.engine.JmcTestEngine

Discovers tests based on the provided discovery request and unique ID.

E

edges - Variable in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

end() - Static method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Creates a scheduling choice that indicates the end of the task schedule.

end() - Static method in class org.mpi_sws.jmc.strategies.trust.Event

Creates the bottom event to indicate end of the execution.

END - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

ENGINE_DISPLAY_NAME - Static variable in class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcEngineDescriptor

ENTER_MONITOR_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

EQ - Enum constant in enum class org.mpi_sws.jmc.util.PartialOrder.Relation

EQ - Enum constant in enum class org.mpi_sws.jmc.util.TotalOrder.Relation

equals(Object) - Method in class org.mpi_sws.jmc.strategies.trust.Event

equals(Object) - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

equals(Object) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

equals(Object) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

equals(Object) - Method in record class org.mpi_sws.jmc.strategies.trust.SchedulingChoiceWrapper

Indicates whether some other object is "equal to" this one.

equals(LamportVectorClock) - Method in class org.mpi_sws.jmc.util.LamportVectorClock

Returns the string representation of the vector clock.

equalsEdges(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

error(Long, Exception) - Method in class org.mpi_sws.jmc.runtime.TaskManager

error(String) - Static method in exception class org.mpi_sws.jmc.runtime.HaltCheckerException

Constructs a new HaltCheckerException indicating that the exploration was halted due to an error.

error(String) - Static method in exception class org.mpi_sws.jmc.runtime.HaltExecutionException

Constructs a new HaltExecutionException of type error with the given message.

error(String) - Static method in class org.mpi_sws.jmc.strategies.trust.Event

Creates a new error event with the given message.

error(String, Throwable) - Static method in exception class org.mpi_sws.jmc.runtime.HaltCheckerException

Constructs a new HaltCheckerException indicating that the exploration was halted due to an error, with a cause.

ERROR - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

Event - Class in org.mpi_sws.jmc.strategies.trust

Represents an event object used by the algorithm.

Event(Long, Integer, Event.Type) - Constructor for class org.mpi_sws.jmc.strategies.trust.Event

Creates a new event with the given task ID, location, and type.

Event.EventPredicate - Interface in org.mpi_sws.jmc.strategies.trust

A generic event predicate.

Event.Key - Class in org.mpi_sws.jmc.strategies.trust

Unique key for the event.

Event.Type - Enum Class in org.mpi_sws.jmc.strategies.trust

Represents the type of the event according to the algorithm.

EventFactory - Class in org.mpi_sws.jmc.strategies.trust

EventFactory() - Constructor for class org.mpi_sws.jmc.strategies.trust.EventFactory

EventUtils - Class in org.mpi_sws.jmc.strategies.trust

EventUtils() - Constructor for class org.mpi_sws.jmc.strategies.trust.EventUtils

ExceptionUtil - Class in org.mpi_sws.jmc.util

Utility class for exception handling.

ExceptionUtil() - Constructor for class org.mpi_sws.jmc.util.ExceptionUtil

execute() - Method in interface org.mpi_sws.jmc.integrations.junit5.descriptors.JmcExecutableTestDescriptor

execute() - Method in class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcMethodTestDescriptor

Executes the JMC test method.

execute(Method, Object, JmcCheckerConfiguration) - Static method in class org.mpi_sws.jmc.integrations.junit5.engine.JmcTestExecutor

Executes a JMC test method and returns the report generated by the model checker.

execute(Runnable) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

execute(ExecutionRequest) - Method in class org.mpi_sws.jmc.integrations.junit5.engine.JmcTestEngine

Executes the discovered tests in the JMC test engine.

executeReplay(Method, Object, JmcCheckerConfiguration) - Static method in class org.mpi_sws.jmc.integrations.junit5.engine.JmcTestExecutor

Replays a previously executed JMC test method to verify its behavior against recorded traces.

ExecutionGraph - Class in org.mpi_sws.jmc.strategies.trust

Represents an execution graph.

ExecutionGraph() - Constructor for class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Initializes a new execution graph.

ExecutionGraph.ExecutionGraphNodeVisitor - Interface in org.mpi_sws.jmc.strategies.trust

Generic visitor interface for the execution graph nodes.

ExecutionGraph.TopologicalSorter - Class in org.mpi_sws.jmc.strategies.trust

Topological sorter for the execution graph.

ExecutionGraph.TopologicalSorter.GraphCycleException - Exception Class in org.mpi_sws.jmc.strategies.trust

Exception thrown when the graph has cycles.

ExecutionGraphNode - Class in org.mpi_sws.jmc.strategies.trust

Represents a node in the execution graph.

ExecutionGraphNode(Event, LamportVectorClock) - Constructor for class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Constructs a new ExecutionGraphNode with the given event.

ExecutionGraphSimulator - Class in org.mpi_sws.jmc.strategies.trust

ExecutionGraphSimulator() - Constructor for class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

EXIT_MONITOR_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

ExplorationStack - Class in org.mpi_sws.jmc.strategies.trust

The exploration stack used in the Trust algorithm.

ExplorationStack() - Constructor for class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Creates a new exploration stack.

ExplorationStack.Item - Class in org.mpi_sws.jmc.strategies.trust

Represents an item in the exploration stack.

ExplorationStack.ItemType - Enum Class in org.mpi_sws.jmc.strategies.trust

Represents the item type in the exploration stack.

F

FIFO - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.TrustStrategy.SchedulingPolicy

FileUtil - Class in org.mpi_sws.jmc.util

Utility class for file operations related to storing and reading task schedules.

FileUtil() - Constructor for class org.mpi_sws.jmc.util.FileUtil

findTasksWithStatus(TaskManager.TaskState) - Method in class org.mpi_sws.jmc.runtime.TaskManager

Return all the tasks with the specified state.

FINISH_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

FLW - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.ExplorationStack.ItemType

forEachPredecessor(BiConsumer<Relation, List<Event.Key>>) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

forEachSuccessor(BiConsumer<Relation, List<Event.Key>>) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

forwardLW(ExecutionGraphNode, ExecutionGraph) - Static method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

forwardRW(ExecutionGraphNode, ExecutionGraphNode, ExecutionGraph) - Static method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Creates a forward revisit item for a read revisiting an alternative write.

forwardWW(ExecutionGraphNode, ExecutionGraphNode, ExecutionGraph) - Static method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Creates a forward revisit item for a write revisiting an alternative concurrent write.

FR - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Relation

fromAnnotation(JmcCheckConfiguration) - Static method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Creates a JmcCheckerConfiguration from the given annotation.

fromJson(JsonElement) - Method in class org.mpi_sws.jmc.runtime.scheduling.PrimitiveValueAdapter

fromRuntimeEvent(JmcRuntimeEvent) - Static method in class org.mpi_sws.jmc.strategies.trust.EventFactory

Creates a new event mapping the runtime event to the trust event.

fromRuntimeEvent(JmcRuntimeEvent) - Static method in class org.mpi_sws.jmc.strategies.trust.Location

FRW - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.ExplorationStack.ItemType

FUTURE_EXCEPTION_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

FUTURE_SET_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

FUTURE_START_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

FWW - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.ExplorationStack.ItemType

G

get() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicBoolean

Returns the current value of this atomic boolean.

get() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger

Returns the current value of this atomic integer.

get() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReference

get() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

get(int) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReferenceArray

get(int[]) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicStampedReference

get(long, TimeUnit) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

GET_FUTURE_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

getActiveTasks() - Method in class org.mpi_sws.jmc.runtime.TaskManager

Return custom IDs of all the tasks.

getActiveTasks() - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

Returns the set of active tasks.

getAdditionalEventsToProcess() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

getAlias(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.LocationStore

Returns the location alias for the given hash code.

getAllPredecessors() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns all the predecessors of this node.

getAllSuccessors() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the edges of this node.

getAllWrites() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns all the writes in the execution graph.

getAlternativeLockReads(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the alternative reads to the given write event.

getAlternativeLockWrites(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the potential alternative writes to the given lock read.

getAlternativeWrites(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the alternative writes (in reverse CO order) to the given read event.

getAndIncrement() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger

Atomically increments the current value by 1 and returns the previous value.

getAndSet(int) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger

Atomically sets the value to the given new value and returns the previous value.

getAndSet(int, V) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReferenceArray

getAndSet(V) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReference

getAttribute(String) - Method in class org.mpi_sws.jmc.strategies.trust.Event

Returns the attribute of the event with the given key in the type T.

getAttribute(String) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the attribute with the given key.

getCoherentPlacings(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the coherency placings of the given write event under sequential consistency.

getCoMax(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the last write event to the given location.

getConfigAnnotation() - Method in class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcClassTestDescriptor

getCoverageGraph() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

getDebug() - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Returns the debug mode status.

getDebug() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration

getDebug() - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration

getEdges() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the edges of this node.

getErrorIteration() - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

getErrorMessage() - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

getEvent() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the Event that this node represents.

getEvent1() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Gets the first event of the item.

getEvent2() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Gets the second event of the item.

getEventNode(Event.Key) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the event node with the given key.

getExecutionGraph() - Method in class org.mpi_sws.jmc.strategies.trust.Algo

getExecutionGraph() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

getExecutionGraph() - Method in class org.mpi_sws.jmc.strategies.trust.TrustStrategy

getGraph() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Gets the graph associated with the item.

getGraph(ExplorationStack.Item) - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Gets the graph associated with the item.

getId() - Method in class org.mpi_sws.jmc.integrations.junit5.engine.JmcTestEngine

getInDegree() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the number of incoming edges of this node.

getInnerStackIndex() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Gets the inner stack index of the item.

getJoinedTask(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

getKey() - Method in class org.mpi_sws.jmc.strategies.trust.Event

getLocation() - Method in class org.mpi_sws.jmc.strategies.trust.Event

Returns the location of the event.

getMeasuringFrequency() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig

getNumIterations() - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Returns the number of iterations to run the checker.

getParam(String) - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

getParam(String) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Returns the value of the parameter with the specified key as an object of the specified class.

getParams() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Returns the parameters of the event.

getPoPredecessor() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the predecessor of this node in the program order.

getPotentialReads(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the potential alternative reads to the given write event.

getPredecessors(Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the back edges of this node.

getRead() - Method in class org.mpi_sws.jmc.strategies.trust.BackwardRevisitView

getRecordPath() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig

getReference() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicStampedReference

getReplaySeed() - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

getReportPath() - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Returns the path where the report will be saved.

getReportPath() - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

getReportPath() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration

getReportPath() - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration

getRestrictedGraph() - Method in class org.mpi_sws.jmc.strategies.trust.BackwardRevisitView

Gets the restricted graph.

getSchedulableTasks() - Method in class org.mpi_sws.jmc.strategies.trust.Algo

getSchedulerTries() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration

getSchedulerTrySleepTimeNanos() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration

getSeed() - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Returns the seed for the checker.

getSeed() - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration

getSize() - Method in class org.mpi_sws.jmc.util.LamportVectorClock

Returns the size of the vector clock.

getStamp() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicStampedReference

getStartedBy(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

getStatus(Long) - Method in class org.mpi_sws.jmc.runtime.TaskManager

Return the state of the task with the specified custom ID.

getStrategy() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration

getStrategyType() - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Returns the type of scheduling strategy to be used.

getSuccessors(Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the neighbours of this node that have the given adjacency.

getTaskId() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

getTaskId() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcThread

Returns the task ID of this thread.

getTaskId() - Method in exception class org.mpi_sws.jmc.runtime.HaltTaskException

Returns the ID of the task which should be halted.

getTaskId() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Returns the ID of the task that generated the event.

getTaskId() - Method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Returns the ID of the task associated with this scheduling choice.

getTaskId() - Method in class org.mpi_sws.jmc.strategies.trust.Event

Returns the task ID of the event.

getTaskId() - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

getTaskSchedule(List<ExecutionGraphNode>) - Static method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Generate a task Schedule from a given sorted list of event nodes.

getTimeout() - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Returns the timeout duration for the checker.

getTimestamp() - Method in class org.mpi_sws.jmc.strategies.trust.Event

Returns the timestamp of the event.

getTimestamp() - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

getTOIndex(Event.Key) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the index of the given key in the TO order.

getTOIndex(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the index of the given node in the TO order.

getToStamp() - Method in class org.mpi_sws.jmc.strategies.trust.Event

Returns the total order timestamp of the event.

getToStamp() - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

getTotalIterations() - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

getTotalTimeMillis() - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

getTrustSchedulingPolicy() - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration

getType() - Method in class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcClassTestDescriptor

getType() - Method in class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcMethodTestDescriptor

getType() - Method in exception class org.mpi_sws.jmc.runtime.HaltExecutionException

getType() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Returns the type of the event.

getType() - Method in class org.mpi_sws.jmc.strategies.trust.Event

Returns the type of the event.

getType() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Gets the type of the item.

getUnblockedTasks() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the list of task identifiers in the execution graph where a new event can be added.

getValue() - Method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Returns the value associated with this scheduling choice.

getVector() - Method in class org.mpi_sws.jmc.util.LamportVectorClock

Returns the vector clock.

getVectorClock() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns the vector clock of this node.

getWrite() - Method in class org.mpi_sws.jmc.strategies.trust.BackwardRevisitView

getWrites(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns the writes to the given location.

GraphCycleException(String) - Constructor for exception class org.mpi_sws.jmc.strategies.trust.ExecutionGraph.TopologicalSorter.GraphCycleException

Initializes a new graph cycle exception with the given message.

GT - Enum constant in enum class org.mpi_sws.jmc.util.PartialOrder.Relation

GT - Enum constant in enum class org.mpi_sws.jmc.util.TotalOrder.Relation

H

HALT_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

HaltCheckerException - Exception Class in org.mpi_sws.jmc.runtime

Exception thrown to halt execution of the current and all subsequent executions.

HaltExecutionException - Exception Class in org.mpi_sws.jmc.runtime

Exception thrown to halt execution of the current execution.

HaltExecutionException(HaltExecutionException.Type, String) - Constructor for exception class org.mpi_sws.jmc.runtime.HaltExecutionException

Constructs a new HaltExecutionException with the given type and message.

HaltExecutionException.Type - Enum Class in org.mpi_sws.jmc.runtime

Error type when the model checker stops the execution.

HaltTaskException - Exception Class in org.mpi_sws.jmc.runtime

Exception thrown to halt execution of the current task.

HaltTaskException(Long) - Constructor for exception class org.mpi_sws.jmc.runtime.HaltTaskException

Constructs a new HaltTaskException object.

HaltTaskException(Long, String) - Constructor for exception class org.mpi_sws.jmc.runtime.HaltTaskException

Constructs a new HaltTaskException object.

handleBot(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

handleLockAcquired(Event) - Method in class org.mpi_sws.jmc.strategies.trust.Algo

handleLockAwait(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

handleNoop(Event) - Method in class org.mpi_sws.jmc.strategies.trust.Algo

Handles the NOOP event.

handleNoop(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

handleRead(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

handleReadEx(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

handleWrite(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

handleWriteEx(Event) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

happensBefore(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Check if `this` node is happens-before (_porf_ relation) the `other` node.

happensBefore(LamportVectorClock) - Method in class org.mpi_sws.jmc.util.LamportVectorClock

Checks if this vector clock happens before the other vector clock.

hasAttribute(String) - Method in class org.mpi_sws.jmc.strategies.trust.Event

hasEdge(Event.Key, Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Returns whether this node has an edge to the given node with the given adjacency.

hasEventNode(Event.Key) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns true if the execution graph has an event node with the given key.

hashCode() - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

hashCode() - Method in class org.mpi_sws.jmc.strategies.trust.Location

hashCode() - Method in record class org.mpi_sws.jmc.strategies.trust.SchedulingChoiceWrapper

Returns a hash code value for this object.

hasLocation() - Method in record class org.mpi_sws.jmc.strategies.trust.SchedulingChoiceWrapper

Returns whether the scheduling choice has a location.

hasPredecessor(Event.Key, Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Checks if this node has a predecessor with the given key and relation.

I

init() - Static method in class org.mpi_sws.jmc.strategies.trust.Event

Creates an init event.

init(TaskManager, Long) - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Initializes the scheduler with the task manager and the main thread.

INIT - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

initIteration(int, JmcModelCheckerReport) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Initializes the runtime with the main thread for a given iteration.

initIteration(int, JmcModelCheckerReport) - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Initializes the strategy for a new iteration.

initIteration(int, JmcModelCheckerReport) - Method in class org.mpi_sws.jmc.strategies.RandomSchedulingStrategy

initIteration(int, JmcModelCheckerReport) - Method in interface org.mpi_sws.jmc.strategies.SchedulingStrategy

Initializes the strategy for a new iteration.

initIteration(int, JmcModelCheckerReport) - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

initIteration(int, JmcModelCheckerReport) - Method in class org.mpi_sws.jmc.strategies.trust.Algo

Initializes the iteration.

initIteration(int, JmcModelCheckerReport) - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategy

initIteration(int, JmcModelCheckerReport) - Method in class org.mpi_sws.jmc.strategies.trust.TrustStrategy

InvalidComparisonException(String) - Constructor for exception class org.mpi_sws.jmc.util.TotalOrder.InvalidComparisonException

invoke() - Method in class org.mpi_sws.jmc.checker.JmcFunctionalTestTarget

invoke() - Method in interface org.mpi_sws.jmc.checker.JmcFunctionalTestTarget.Target

invoke() - Method in interface org.mpi_sws.jmc.checker.JmcTestTarget

Invokes the target.

invokeAll(Collection<? extends Callable<T>>) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

invokeAll(Collection<? extends Callable<T>>, long, TimeUnit) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

invokeAny(Collection<? extends Callable<T>>) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

invokeAny(Collection<? extends Callable<T>>, long, TimeUnit) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

isActive(Long) - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

Returns whether the given thread is active.

isAssertionError(Throwable) - Static method in class org.mpi_sws.jmc.util.ExceptionUtil

Checks if the given Throwable is an AssertionError or contains an AssertionError in its cause chain.

isBackwardRevisit() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Checks if the item is a forward revisit.

isBlockExecution() - Method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Checks if this scheduling choice blocks execution.

isBlockingLabel(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isBlockTask() - Method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Checks if this scheduling choice is a blocking task.

isCancelled() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

isDebugEnabled() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig

isDone() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

isEmpty() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns true if the graph contains only the initial event.

isEmpty() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Checks if the stack is empty.

isEnd() - Method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Checks if this scheduling choice is the end of the schedule.

isExclusiveRead(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isExclusiveWrite(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isFinalLockWrite(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isInit() - Method in class org.mpi_sws.jmc.strategies.trust.Event

Returns true if the event is an init event.

isLockAcquired(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isLockAcquireRead(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isLockAcquireWrite(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isLockReleaseWrite(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isMaximalExtension() - Method in class org.mpi_sws.jmc.strategies.trust.BackwardRevisitView

Checks if the restricted view is a maximal extension

isOkay() - Method in exception class org.mpi_sws.jmc.runtime.HaltCheckerException

Returns whether the exploration was successful without any errors.

isRead() - Method in class org.mpi_sws.jmc.strategies.trust.Event

isRead(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isReadEx() - Method in class org.mpi_sws.jmc.strategies.trust.Event

isRecordPerIteration() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig

isRevisit(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isRfConsistent() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

isShutdown() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

Returns whether the executor service is shutdown.

isTaskBlocked(Long) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Checks if the task with the given ID is blocked.

isTaskOfStatus(Long, TaskManager.TaskState) - Method in class org.mpi_sws.jmc.runtime.TaskManager

Return true if the task with the specified system task ID is in the task pool and with status provided.

isTerminated() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

Returns whether the executor service is terminated.

isThreadFinish(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isThreadJoin(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isThreadStart(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isTimeout() - Method in exception class org.mpi_sws.jmc.runtime.HaltCheckerException

Returns whether the exploration was halted due to a timeout.

isValidStrategy(String) - Static method in class org.mpi_sws.jmc.strategies.SchedulingStrategyFactory

Checks if a strategy is valid.

isWrite() - Method in class org.mpi_sws.jmc.strategies.trust.Event

isWrite(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

isWriteEx() - Method in class org.mpi_sws.jmc.strategies.trust.Event

iterator() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns an iterator walking through the nodes in a topological sort order.

J

JmcAssume - Class in org.mpi_sws.jmc.api.util.statements

The JmcAssume class provides a method to assert conditions in the JMC runtime environment.

JmcAssume() - Constructor for class org.mpi_sws.jmc.api.util.statements.JmcAssume

JmcAsyncRunnable(Supplier<? extends T>, JmcCompletableFuture<T>) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture.JmcAsyncRunnable

JmcAtomicBoolean - Class in org.mpi_sws.jmc.api.util.concurrent

A redefinition of AtomicBoolean that communicates with JMC runtime to perform read, write, and compare-and-set operations.

JmcAtomicBoolean() - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicBoolean

Constructs a new JmcAtomicBoolean with an initial value of false.

JmcAtomicBoolean(boolean) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicBoolean

Constructs a new JmcAtomicBoolean with the specified initial value.

JmcAtomicInteger - Class in org.mpi_sws.jmc.api.util.concurrent

A redefinition of AtomicInteger for JMC model checking.

JmcAtomicInteger() - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger

Constructs a new JmcAtomicInteger with an initial value of 0.

JmcAtomicInteger(int) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger

Constructs a new JmcAtomicInteger with the specified initial value.

JmcAtomicReference<V> - Class in org.mpi_sws.jmc.api.util.concurrent

A redefinition of AtomicReference to support JMC model checking.

JmcAtomicReference(V) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReference

Constructs a new JmcAtomicReference with the specified initial value.

JmcAtomicReferenceArray<V> - Class in org.mpi_sws.jmc.api.util.concurrent

A redefinition of the AtomicReferenceArray class.

JmcAtomicReferenceArray(int) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReferenceArray

JmcAtomicStampedReference<V> - Class in org.mpi_sws.jmc.api.util.concurrent

JmcAtomicStampedReference(V, int) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicStampedReference

JmcCheck - Annotation Interface in org.mpi_sws.jmc.annotations

A mandatory annotation to mark a test method or class to be run with the JMC model checker.

JmcCheckConfiguration - Annotation Interface in org.mpi_sws.jmc.annotations

Configuration annotation for JMC checks.

JmcCheckerConfiguration - Class in org.mpi_sws.jmc.checker

Configuration for the JMC checker.

JmcCheckerConfiguration.Builder - Class in org.mpi_sws.jmc.checker

Builder for JmcCheckerConfiguration

JmcCheckerException - Exception Class in org.mpi_sws.jmc.checker.exceptions

Exception class for JMC checker errors.

JmcCheckerException(String) - Constructor for exception class org.mpi_sws.jmc.checker.exceptions.JmcCheckerException

Constructs a new JmcCheckerException with the specified detail message.

JmcCheckerException(String, Throwable) - Constructor for exception class org.mpi_sws.jmc.checker.exceptions.JmcCheckerException

Constructs a new JmcCheckerException with the specified detail message and cause.

JmcCheckerTimeoutException - Exception Class in org.mpi_sws.jmc.checker.exceptions

Exception class for JMC checker timeout errors.

JmcCheckerTimeoutException(String) - Constructor for exception class org.mpi_sws.jmc.checker.exceptions.JmcCheckerTimeoutException

Constructs a new JmcCheckerTimeoutException with the specified detail message.

JmcClassTestDescriptor - Class in org.mpi_sws.jmc.integrations.junit5.descriptors

A JUnit 5 test descriptor for a JMC class test.

JmcClassTestDescriptor(Class<?>, TestDescriptor, boolean) - Constructor for class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcClassTestDescriptor

JmcCompletableFuture<T> - Class in org.mpi_sws.jmc.api.util.concurrent

A JMC-specific version of CompletableFuture that allows for custom execution and provides a way to set an underlying JmcFuture.

JmcCompletableFuture() - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture

JmcCompletableFuture.JmcAsyncRunnable<T> - Class in org.mpi_sws.jmc.api.util.concurrent

JmcDescriptorUtil - Class in org.mpi_sws.jmc.integrations.junit5.descriptors

Utility class for handling JMC descriptor configurations.

JmcDescriptorUtil() - Constructor for class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcDescriptorUtil

JmcEngineDescriptor - Class in org.mpi_sws.jmc.integrations.junit5.descriptors

A JUnit 5 engine descriptor for the JMC engine.

JmcEngineDescriptor(UniqueId) - Constructor for class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcEngineDescriptor

JmcExecutableTestDescriptor - Interface in org.mpi_sws.jmc.integrations.junit5.descriptors

A JMC executable test descriptor for JUnit 5.

JmcExecutors - Class in org.mpi_sws.jmc.api.util.concurrent

A replacement for Executors.

JmcExecutors() - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcExecutors

JmcExecutorService - Class in org.mpi_sws.jmc.api.util.concurrent

An executor service that runs tasks in new threads.

JmcExecutorService(int) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

JmcExpectAssertionFailure - Annotation Interface in org.mpi_sws.jmc.annotations

This annotation is used to mark a test method or class to expect an assertion failure in the JMC model checker.

JmcExpectExecutions - Annotation Interface in org.mpi_sws.jmc.annotations

This annotation is used to mark a test method or class to expect a certain number of executions in the JMC model checker.

JmcFunctionalTestTarget - Class in org.mpi_sws.jmc.checker

A functional test target for JMC that allows invoking a target method.

JmcFunctionalTestTarget(String, JmcFunctionalTestTarget.Target) - Constructor for class org.mpi_sws.jmc.checker.JmcFunctionalTestTarget

JmcFunctionalTestTarget.Target - Interface in org.mpi_sws.jmc.checker

Represents a target for JMC.

JmcFuture<T> - Class in org.mpi_sws.jmc.api.util.concurrent

A future that runs a callable function in a new thread.

JmcFuture(Runnable, Long) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

JmcFuture(Runnable, T, Long) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

JmcFuture(Callable<T>, Long) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

JmcFuture(JmcThread) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

JmcFuture(JmcThread, T) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

JmcIgnoreInstrumentation - Annotation Interface in org.mpi_sws.jmc.annotations

This annotation is used to mark methods or classes that should be ignored by the JMC instrumentation.

JmcInvalidConfigurationException - Exception Class in org.mpi_sws.jmc.checker.exceptions

Exception class for JMC invalid configuration errors.

JmcInvalidConfigurationException(String) - Constructor for exception class org.mpi_sws.jmc.checker.exceptions.JmcInvalidConfigurationException

Constructs a new JmcInvalidConfigurationException with the specified detail message.

JmcInvalidStrategyException - Exception Class in org.mpi_sws.jmc.strategies

Exception thrown when an invalid strategy is encountered.

JmcInvalidStrategyException(String) - Constructor for exception class org.mpi_sws.jmc.strategies.JmcInvalidStrategyException

JmcLockSupport - Class in org.mpi_sws.jmc.api.util.concurrent

The LockSupport class is the replacement for LockSupport class.

JmcLockSupport() - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcLockSupport

JmcMeasureGraphCoverage - Annotation Interface in org.mpi_sws.jmc.annotations.strategies

This annotation is used to configure the JMC graph coverage measurement for a test method or class.

JmcMethodTestDescriptor - Class in org.mpi_sws.jmc.integrations.junit5.descriptors

A JUnit 5 test descriptor for a JMC method test.

JmcMethodTestDescriptor(Method, JmcClassTestDescriptor) - Constructor for class org.mpi_sws.jmc.integrations.junit5.descriptors.JmcMethodTestDescriptor

JmcModelChecker - Class in org.mpi_sws.jmc.checker

The JmcModelChecker class is responsible for managing the model checking process.

JmcModelChecker(JmcCheckerConfiguration) - Constructor for class org.mpi_sws.jmc.checker.JmcModelChecker

Constructs a new JMC model checker with the given configuration.

JmcModelCheckerReport - Class in org.mpi_sws.jmc.checker

The JmcModelCheckerReport class represents a report generated by the JMC model checker.

JmcModelCheckerReport(String) - Constructor for class org.mpi_sws.jmc.checker.JmcModelCheckerReport

Constructs a new JmcModelCheckerReport object.

JmcRandom - Class in org.mpi_sws.jmc.api.util

A JMC-specific implementation of java.util.Random that allows for model checking.

JmcRandom() - Constructor for class org.mpi_sws.jmc.api.util.JmcRandom

Default constructor for JmcRandom.

JmcRandom(long) - Constructor for class org.mpi_sws.jmc.api.util.JmcRandom

To ensure compatibility with the java.util.Random API, this constructor is provided.

JmcReentrantLock - Class in org.mpi_sws.jmc.api.util.concurrent

A reentrant lock that can be used to synchronize access to shared resources.

JmcReentrantLock() - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcReentrantLock

JmcReentrantLock(Object) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcReentrantLock

JmcReplay - Annotation Interface in org.mpi_sws.jmc.annotations

This annotation is used to mark a test method or class to be replayed in the JMC model checker.

JmcReplayUnsupported - Exception Class in org.mpi_sws.jmc.strategies

Exception thrown when replay is not supported by the current strategy.

JmcReplayUnsupported() - Constructor for exception class org.mpi_sws.jmc.strategies.JmcReplayUnsupported

JmcRuntime - Class in org.mpi_sws.jmc.runtime

The Runtime environment complete with a scheduler and configuration options used by the model checker.

JmcRuntime() - Constructor for class org.mpi_sws.jmc.runtime.JmcRuntime

JmcRuntimeConfiguration - Class in org.mpi_sws.jmc.runtime

Represents the configuration for the JMC runtime.

JmcRuntimeConfiguration.Builder - Class in org.mpi_sws.jmc.runtime

JmcRuntimeEvent - Class in org.mpi_sws.jmc.runtime

Represents an event that occurs during the execution of a program.

JmcRuntimeEvent(JmcRuntimeEvent.Type, Long) - Constructor for class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Constructs a new runtime event with the specified type and task ID.

JmcRuntimeEvent(JmcRuntimeEvent.Type, Long, Map<String, Object>) - Constructor for class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Constructs a new runtime event with the specified type, task ID, and parameters.

JmcRuntimeEvent.Builder - Class in org.mpi_sws.jmc.runtime

A builder for constructing a JmcRuntimeEvent object.

JmcRuntimeEvent.Type - Enum Class in org.mpi_sws.jmc.runtime

Enum representing the different types of runtime events that can occur.

JmcRuntimeUtils - Class in org.mpi_sws.jmc.runtime

Utility class for JMC runtime operations.

JmcRuntimeUtils() - Constructor for class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

JmcTestEngine - Class in org.mpi_sws.jmc.integrations.junit5.engine

A custom JUnit 5 test engine for running JMC tests.

JmcTestEngine() - Constructor for class org.mpi_sws.jmc.integrations.junit5.engine.JmcTestEngine

JmcTestExecutor - Class in org.mpi_sws.jmc.integrations.junit5.engine

Executes a JMC test method using the JMC Model Checker.

JmcTestExecutor() - Constructor for class org.mpi_sws.jmc.integrations.junit5.engine.JmcTestExecutor

JmcTestTarget - Interface in org.mpi_sws.jmc.checker

Represents a target for JMC.

JmcThread - Class in org.mpi_sws.jmc.api.util.concurrent

This class is a wrapper around the Java Thread class - Thread.

JmcThread() - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThread

Constructs a new JmcThread object.

JmcThread(Long) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThread

Constructs a new JmcThread object with the given JMC thread ID.

JmcThread(Runnable) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThread

Constructs a new JmcThread object with the given Runnable.

JmcThread(Runnable, Long) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThread

Constructs a new JmcThread object with the given Runnable and JMC thread ID.

JmcThreadFactory - Class in org.mpi_sws.jmc.api.util.concurrent

A thread factory that creates JmcThread instances.

JmcThreadFactory() - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThreadFactory

Default JmcThread factory.

JmcThreadFactory(ThreadFactory) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThreadFactory

Create a new thread factory that wraps the given base factory.

JmcThreadPoolExecutor - Class in org.mpi_sws.jmc.api.util.concurrent

A thread pool executor that runs tasks in new threads.

JmcThreadPoolExecutor(int, int, long, TimeUnit, BlockingQueue<Runnable>) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThreadPoolExecutor

JmcThreadPoolExecutor(int, int, long, TimeUnit, BlockingQueue<Runnable>, RejectedExecutionHandler) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThreadPoolExecutor

JmcThreadPoolExecutor(int, int, long, TimeUnit, BlockingQueue<Runnable>, ThreadFactory) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThreadPoolExecutor

JmcThreadPoolExecutor(int, int, long, TimeUnit, BlockingQueue<Runnable>, ThreadFactory, RejectedExecutionHandler) - Constructor for class org.mpi_sws.jmc.api.util.concurrent.JmcThreadPoolExecutor

JmcTimeout - Annotation Interface in org.mpi_sws.jmc.annotations

This annotation is used to specify a timeout for a test method or class when using the JMC model checker.

JmcTrustStrategy - Annotation Interface in org.mpi_sws.jmc.annotations.strategies

This annotation is used to configure the JMC trust strategy for a test method or class.

join(Long) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Updates the TaskManager to terminate the task with the given ID and yields control to the scheduler to schedule other tasks.

join(Thread) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Joins the specified thread, waiting indefinitely for it to finish.

join(Thread, long) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Joins the specified thread, waiting for it to finish for a specified time.

join(Thread, long, int) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Joins the specified thread, waiting for it to finish for a specified time and nanoseconds.

JOIN_COMPLETE_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

JOIN_REQUEST_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

join1() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcThread

Replacing the thread join to intercept the join Event

join1(Long) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcThread

Replacing the Thread join to intercept the join Event.

K

key() - Method in class org.mpi_sws.jmc.strategies.trust.Event

The key of the event.

key() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

key() - Method in enum class org.mpi_sws.jmc.strategies.trust.Relation

Key(Long) - Constructor for class org.mpi_sws.jmc.strategies.trust.Event.Key

Creates a new key with the given task ID and timestamp.

Key(Event.Key) - Constructor for class org.mpi_sws.jmc.strategies.trust.Event.Key

L

LamportVectorClock - Class in org.mpi_sws.jmc.util

Represents a Lamport vector clock used by the algorithm.

LamportVectorClock(int) - Constructor for class org.mpi_sws.jmc.util.LamportVectorClock

Creates a new Lamport vector clock with the given size.

LamportVectorClock(int[]) - Constructor for class org.mpi_sws.jmc.util.LamportVectorClock

Creates a new Lamport vector clock with the given vector.

LamportVectorClock(LamportVectorClock, int) - Constructor for class org.mpi_sws.jmc.util.LamportVectorClock

Creates a new Lamport vector clock with the given vector, incrementing the value at the given index.

LamportVectorClock.Component - Class in org.mpi_sws.jmc.util

Represents a component of the Lamport vector clock.

location() - Method in record class org.mpi_sws.jmc.strategies.trust.SchedulingChoiceWrapper

Returns the value of the location record component.

Location - Class in org.mpi_sws.jmc.strategies.trust

Location(Object, String) - Constructor for class org.mpi_sws.jmc.strategies.trust.Location

LocationStore - Class in org.mpi_sws.jmc.strategies.trust

A single class to store references to locations and to keep track of location aliases.

LocationStore() - Constructor for class org.mpi_sws.jmc.strategies.trust.LocationStore

Constructs a new location store.

lock() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcReentrantLock

Acquires the lock.

LOCK_ACQUIRE - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

LOCK_ACQUIRE_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

LOCK_ACQUIRED_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

LOCK_RELEASE - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

LOCK_RELEASE_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

lockAcquiredEventWithoutYield(Object, String, String, Object, String, Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Creates a lock acquired event for the specified instance, owner, name, value, descriptor, and new value without yielding.

lockAcquireEvent(String, String, Object, String, Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Creates a lock acquire event for the specified owner, name, value, descriptor, and instance.

lockBackwardRevisit(ExecutionGraphNode, ExecutionGraphNode, ExecutionGraph) - Static method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Creates a backward revisit item for a lock read revisiting another lock read.

lockReleaseEvent(Object, String, String, Object, String, Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Creates a lock release event for the specified instance, owner, name, value, descriptor, and new value.

logStackState() - Method in class org.mpi_sws.jmc.strategies.trust.Algo

logStackState() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Logs the current state of the stack.

LT - Enum constant in enum class org.mpi_sws.jmc.util.PartialOrder.Relation

LT - Enum constant in enum class org.mpi_sws.jmc.util.TotalOrder.Relation

M

makeRevistable(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

makeUnRevistable(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

markActive(Long) - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

Marks the given thread as active.

markInactive(Long) - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

Marks the given thread as inactive.

markLockWriteFinal(Event) - Static method in class org.mpi_sws.jmc.strategies.trust.EventUtils

markStatus(Long, TaskManager.TaskState) - Method in class org.mpi_sws.jmc.runtime.TaskManager

Update the state of the task with the specified custom ID.

max() - Method in class org.mpi_sws.jmc.util.LamportVectorClock

Returns the maximum value in the vector clock.

MeasureGraphCoverageStrategy - Class in org.mpi_sws.jmc.strategies.trust

A scheduling strategy that measures the coverage of execution graphs during the model checking process.

MeasureGraphCoverageStrategy(SchedulingStrategy, MeasureGraphCoverageStrategyConfig) - Constructor for class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategy

MeasureGraphCoverageStrategyConfig - Class in org.mpi_sws.jmc.strategies.trust

Configuration class for the MeasureGraphCoverageStrategy.

MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder - Class in org.mpi_sws.jmc.strategies.trust

MeasureGraphCoverageStrategyConfigBuilder() - Constructor for class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder

N

name() - Method in class org.mpi_sws.jmc.checker.JmcFunctionalTestTarget

name() - Method in interface org.mpi_sws.jmc.checker.JmcTestTarget

Returns the name of the target.

newFixedThreadPool(int) - Static method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutors

Creates a fixed thread pool with the specified number of threads that uses a JMC executor service.

newIncompleteFuture() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture

newSingleThreadExecutor() - Static method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutors

Creates a single-threaded executor that uses a JMC executor service.

newThread(Runnable) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcThreadFactory

next(int) - Method in class org.mpi_sws.jmc.api.util.JmcRandom

This method is overridden to yield control to the JMC runtime.

nextTask() - Method in class org.mpi_sws.jmc.strategies.RandomSchedulingStrategy

Returns the next task to be scheduled.

nextTask() - Method in interface org.mpi_sws.jmc.strategies.SchedulingStrategy

Returns the ID of the next thread to be scheduled.

nextTask() - Method in class org.mpi_sws.jmc.strategies.trust.Algo

Returns the next task to be scheduled according to the execution graph set in place.

nextTask() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategy

nextTask() - Method in class org.mpi_sws.jmc.strategies.trust.TrustStrategy

NOOP - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

NoSuchEventException - Exception Class in org.mpi_sws.jmc.strategies.trust

Exception thrown when an event does not exist.

NoSuchEventException(Event.Key) - Constructor for exception class org.mpi_sws.jmc.strategies.trust.NoSuchEventException

numIterations() - Element in annotation interface org.mpi_sws.jmc.annotations.JmcCheckConfiguration

The number of iterations to run for the JMC check.

numIterations(Integer) - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

O

ok() - Static method in exception class org.mpi_sws.jmc.runtime.HaltCheckerException

Constructs a new HaltCheckerException indicating that the exploration stopped naturally without any errors.

ok() - Static method in exception class org.mpi_sws.jmc.runtime.HaltExecutionException

Constructs a new HaltExecutionException of type ALL_OK with the given message.

org.mpi_sws.jmc.annotations - package org.mpi_sws.jmc.annotations

Defines annotations used by users of the JMC library.

org.mpi_sws.jmc.annotations.strategies - package org.mpi_sws.jmc.annotations.strategies

Defines annotations for specific strategies used in the JMC library.

org.mpi_sws.jmc.api.util - package org.mpi_sws.jmc.api.util

Provides Redefinitions of java.utl classes with plugs to support JMC model checking.

org.mpi_sws.jmc.api.util.concurrent - package org.mpi_sws.jmc.api.util.concurrent

Redefinitions of classes in the java.util.concurrent package.

org.mpi_sws.jmc.api.util.statements - package org.mpi_sws.jmc.api.util.statements

Defines additional statements of the JMC API to be used in JMC tests.

org.mpi_sws.jmc.checker - package org.mpi_sws.jmc.checker

Defines core classes of the JMC checker framework.

org.mpi_sws.jmc.checker.exceptions - package org.mpi_sws.jmc.checker.exceptions

Defines exceptions used in the JMC Checker module.

org.mpi_sws.jmc.integrations.junit5.descriptors - package org.mpi_sws.jmc.integrations.junit5.descriptors

Defines JUnit 5 descriptors for JMC tests.

org.mpi_sws.jmc.integrations.junit5.engine - package org.mpi_sws.jmc.integrations.junit5.engine

Defines a custom JUnit 5 engine for running JMC tests.

org.mpi_sws.jmc.runtime - package org.mpi_sws.jmc.runtime

This package contains the core runtime components of the JMC framework.

org.mpi_sws.jmc.runtime.scheduling - package org.mpi_sws.jmc.runtime.scheduling

Defines the classes and interfaces for scheduling in the JMC runtime.

org.mpi_sws.jmc.strategies - package org.mpi_sws.jmc.strategies

Defines the strategies used by JMC to check and validate code.

org.mpi_sws.jmc.strategies.trust - package org.mpi_sws.jmc.strategies.trust

Defines the strategy for complete exhaustive model checking of the input program.

org.mpi_sws.jmc.util - package org.mpi_sws.jmc.util

Utility classes for the JMC project.

P

param(String, Object) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Builder

Adds a parameter to the event.

params(Map<String, Object>) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Builder

Sets the parameters of the event.

park() - Static method in class org.mpi_sws.jmc.api.util.concurrent.JmcLockSupport

Park the current thread.

PARK_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

PartialOrder<T> - Interface in org.mpi_sws.jmc.util

Represents a generic partial order relation.

PartialOrder.Relation - Enum Class in org.mpi_sws.jmc.util

Represents the relation between two objects.

pause(Long) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Pauses the task.

pause(Long) - Method in class org.mpi_sws.jmc.runtime.TaskManager

Pauses the task with the specified custom ID.

peek() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Peeks at the item at the top of the stack.

pop() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Pops an item from the stack.

PrimitiveValue - Class in org.mpi_sws.jmc.runtime.scheduling

Represents a primitive value that is returned by a strategy.

PrimitiveValue(Object) - Constructor for class org.mpi_sws.jmc.runtime.scheduling.PrimitiveValue

PrimitiveValueAdapter - Class in org.mpi_sws.jmc.runtime.scheduling

Represents a primitive (Number|String|Boolean) value used in scheduling choices.

PrimitiveValueAdapter() - Constructor for class org.mpi_sws.jmc.runtime.scheduling.PrimitiveValueAdapter

printCO() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

printGraph() - Method in class org.mpi_sws.jmc.strategies.trust.CoverageGraph

printGraph() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

PROGRAM_ERROR - Enum constant in enum class org.mpi_sws.jmc.runtime.HaltExecutionException.Type

ProgramOrder - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Relation

push(ExplorationStack.Item) - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Pushes an item onto the stack.

R

RACE_CONDITION - Enum constant in enum class org.mpi_sws.jmc.runtime.HaltExecutionException.Type

RANDOM - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.TrustStrategy.SchedulingPolicy

RandomSchedulingStrategy - Class in org.mpi_sws.jmc.strategies

A random scheduling strategy that selects the next thread to be scheduled randomly.

RandomSchedulingStrategy(Long, String) - Constructor for class org.mpi_sws.jmc.strategies.RandomSchedulingStrategy

Constructs a new RandomSchedulingStrategy object.

REACTIVE_EVENT_RANDOM_VALUE - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

READ - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

READ_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

READ_EX - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

readEvent(String, String, String, Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Creates a read event for the specified instance, owner, name, and descriptor.

readEventWithoutYield(Object, String, String, String) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Creates a read event for the specified instance, owner, name, and descriptor without yielding.

ReadsFrom - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Relation

readTaskSchedule(String) - Static method in class org.mpi_sws.jmc.util.FileUtil

Reads a task schedule from a JSON file.

recomputeVectorClocks() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Recomputes the vector clocks of all nodes in the execution graph.

recordFrequency() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcMeasureGraphCoverage

The frequency at which the graph coverage will be measured, in milliseconds.

recordGraphs() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcMeasureGraphCoverage

Enable recording of the execution graphs.

recordGraphs(boolean) - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder

recordPath() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcMeasureGraphCoverage

The path where the execution graphs will be recorded.

recordPath(String) - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder

recordPerIteration() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcMeasureGraphCoverage

Record the graph coverage per iteration of the test.

recordPerIteration() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder

recordTaskSchedule(String) - Method in class org.mpi_sws.jmc.strategies.trust.Algo

Records the task schedule generated by the execution graph to the specified filePath.

recordTrace() - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

recordTrace() - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

recordTrace() - Method in class org.mpi_sws.jmc.strategies.RandomSchedulingStrategy

recordTrace() - Method in interface org.mpi_sws.jmc.strategies.ReplayableSchedulingStrategy

Records the current execution trace of the scheduling strategy.

recordTrace() - Method in class org.mpi_sws.jmc.strategies.trust.TrustStrategy

recordUnit() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcMeasureGraphCoverage

The frequency at which the graph coverage will be measured.

RECV_BLOCKING_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

RECV_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

registerAdapter(String, SchedulingChoiceValueAdapter<? extends SchedulingChoiceValue>) - Static method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoiceValueFactory

Registers an adapter for a specific type of SchedulingChoiceValue.

registerSyncLock(Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Registers a synchronization lock for the given instance.

registerSyncLock(String) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Registers a synchronization lock for the given class name.

Relation - Enum Class in org.mpi_sws.jmc.strategies.trust

removeAllEdgesFrom(Event.Key) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Removes all edges from the given node.

removeAllEdgesTo(Event.Key) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

removeAllPredecessors(Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Removes all the predecessors with the given adjacency from this node.

removeEdge(ExecutionGraphNode, Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Removes the edge with the given adjacency from this node.

removeEdge(Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Removes the edge with the given relation from this node.

removeEdgeTo(Event.Key, Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

removeNode(Event.Key) - Method in class org.mpi_sws.jmc.strategies.trust.BackwardRevisitView

Just marks the node as removed, does not update the graph

removePredecessor(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

removePredecessor(ExecutionGraphNode, Relation) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Removes the predecessor with the given adjacency from this node.

replay(JmcTestTarget) - Method in class org.mpi_sws.jmc.checker.JmcModelChecker

Replays the given test target.

ReplayableSchedulingStrategy - Interface in org.mpi_sws.jmc.strategies

A ReplayableSchedulingStrategy is a scheduling strategy that can record and replay its execution trace.

replayRecordedTrace() - Method in class org.mpi_sws.jmc.strategies.RandomSchedulingStrategy

replayRecordedTrace() - Method in interface org.mpi_sws.jmc.strategies.ReplayableSchedulingStrategy

Replays the recorded execution trace of the scheduling strategy.

replayRecordedTrace() - Method in class org.mpi_sws.jmc.strategies.trust.TrustStrategy

reportPath() - Element in annotation interface org.mpi_sws.jmc.annotations.JmcCheckConfiguration

The path where the JMC report will be generated.

reportPath() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcTrustStrategy

The path to store the execution graphs explored.

reportPath(String) - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

reportPath(String) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration.Builder

reportPath(String) - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration.Builder

reset() - Method in class org.mpi_sws.jmc.runtime.TaskManager

Resets the TaskManager object.

reset() - Method in interface org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy.Tracker

Resets the tracker.

reset() - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy.TrackLocks

reset() - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy.TrackTasks

reset() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

resetIteration(int) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Resets the runtime for a new iteration.

resetIteration(int) - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Resets the TaskManager and the scheduling strategy for a new iteration.

resetIteration(int) - Method in interface org.mpi_sws.jmc.strategies.SchedulingStrategy

Resets the strategy for the current Iteration.

resetIteration(int) - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

resetIteration(int) - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategy

resetIteration(int) - Method in class org.mpi_sws.jmc.strategies.trust.TrustStrategy

restrict(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

restrictBySet(Set<Event.Key>) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

resume(Long) - Method in class org.mpi_sws.jmc.runtime.TaskManager

Resumes the task with the specified custom ID.

resume(Long, T) - Method in class org.mpi_sws.jmc.runtime.TaskManager

revisitView(ExecutionGraphNode, ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Constructs a backward revisit view of the ExecutionGraph.

run() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture.JmcAsyncRunnable

run() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcFuture

Run the underlying callable function in a new thread.

run() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcThread

run1() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcThread

This method is overridden by the user.

runAsync(Runnable) - Static method in class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture

RUNNING - Enum constant in enum class org.mpi_sws.jmc.runtime.TaskManager.TaskState

runWithoutJoin() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcThread

Used to run just the function in a wrapped thread and not as a separate thred.

S

Scheduler - Class in org.mpi_sws.jmc.runtime.scheduling

The scheduler is responsible for managing the execution of threads.

Scheduler(SchedulingStrategy, int, long) - Constructor for class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Constructs a new Scheduler object.

schedulerTries(int) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration.Builder

schedulerTrySleepTimeNanos(long) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration.Builder

scheduleTask(SchedulingChoice<T>) - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Performs the scheduling choice (instance of SchedulingChoice) indicated.

SchedulingChoice<T> - Class in org.mpi_sws.jmc.runtime.scheduling

Represents a scheduling choice in the JMC runtime.

SchedulingChoice(Long, T) - Constructor for class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Constructs a new SchedulingChoice object with a value.

SchedulingChoiceValue - Class in org.mpi_sws.jmc.runtime.scheduling

A value that the strategy uses to communicate with the runtime yields.

SchedulingChoiceValue() - Constructor for class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoiceValue

SchedulingChoiceValueAdapter<T> - Class in org.mpi_sws.jmc.runtime.scheduling

An adapter to convert a JSON object to a SchedulingChoiceValue.

SchedulingChoiceValueAdapter() - Constructor for class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoiceValueAdapter

SchedulingChoiceValueFactory - Class in org.mpi_sws.jmc.runtime.scheduling

A factory for creating instances of SchedulingChoiceValue.

SchedulingChoiceValueFactory() - Constructor for class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoiceValueFactory

SchedulingChoiceWrapper - Record Class in org.mpi_sws.jmc.strategies.trust

Represents a scheduling choice with an optional location.

SchedulingChoiceWrapper(SchedulingChoice<?>) - Constructor for record class org.mpi_sws.jmc.strategies.trust.SchedulingChoiceWrapper

Creates a new scheduling choice with the given choice and empty location.

SchedulingChoiceWrapper(SchedulingChoice<?>, Integer) - Constructor for record class org.mpi_sws.jmc.strategies.trust.SchedulingChoiceWrapper

Creates an instance of a SchedulingChoiceWrapper record class.

schedulingPolicy() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcTrustStrategy

The scheduling policy for the trust strategy.

SchedulingStrategy - Interface in org.mpi_sws.jmc.strategies

The scheduling strategy is responsible for deciding which thread to schedule next.

SchedulingStrategyConfiguration - Class in org.mpi_sws.jmc.strategies

Configuration class for scheduling strategies.

SchedulingStrategyConfiguration.Builder - Class in org.mpi_sws.jmc.strategies

SchedulingStrategyConfiguration.SchedulingStrategyConstructor - Interface in org.mpi_sws.jmc.strategies

SchedulingStrategyFactory - Class in org.mpi_sws.jmc.strategies

Factory class for creating scheduling strategies.

SchedulingStrategyFactory() - Constructor for class org.mpi_sws.jmc.strategies.SchedulingStrategyFactory

seed() - Element in annotation interface org.mpi_sws.jmc.annotations.JmcCheckConfiguration

The seed for the random number generator used in the JMC check.

seed() - Element in annotation interface org.mpi_sws.jmc.annotations.strategies.JmcTrustStrategy

The seed for the scheduling strategy.

seed(Long) - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

seed(Long) - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration.Builder

SEND_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

set(boolean) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicBoolean

Sets the value of this atomic boolean to the given value.

set(int) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger

Sets the value of this atomic integer to the given value.

set(int, V) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReferenceArray

set(V) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicReference

set(V, int) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcAtomicStampedReference

setAttribute(String, Object) - Method in class org.mpi_sws.jmc.strategies.trust.Event

Sets the attribute of the event with the given key and value.

setAttributes(Map<String, Object>) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Updates the attributes of this node.

setCurrentTask(Long) - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Sets the ID of the current task.

setErrorIteration(Integer) - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

setErrorMessage(String) - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

setInnerStackIndex(int) - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

Sets the inner stack index of the item.

setLocation(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.Event

setParam(String, Object) - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

setParam(String, Object) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Sets the value of the parameter with the specified key.

setParams(Map<String, Object>) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Sets the parameters of the event.

setReadsFrom(ExecutionGraphNode, ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Sets the reads from relation between the given read and write events.

setReplaySeed(Long) - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

setSeed(Long) - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Sets the seed for the checker.

setTaskId(Long) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Sets the ID of the task that generated the event.

setTimestamp(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

setTimestamp(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.Event

Sets the timestamp of the event.

setToStamp(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

setToStamp(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.Event

Sets the total order timestamp of the event.

setTotalIterations(Integer) - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

setTotalTimeMillis(Long) - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

setType(JmcRuntimeEvent.Type) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

Sets the type of the event.

setUnderlyingFuture(JmcFuture<T>) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture.JmcAsyncRunnable

setUnderlyingFuture(JmcFuture<T>) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture

setup(JmcRuntimeConfiguration) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Sets up the runtime with the given configuration.

setupReplay(JmcRuntimeConfiguration) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

setupReportPath() - Method in class org.mpi_sws.jmc.checker.JmcModelCheckerReport

setVectorClock(LamportVectorClock) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

Updates the vector clock of this node.

sha256Hash(String) - Static method in class org.mpi_sws.jmc.util.StringUtil

Generates a SHA-256 hash of the given input string.

shouldInstrumentThreadCall(Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Checks if the given object is an instance of JmcThread and should be instrumented for thread calls.

shouldRecordGraphs() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig

shutdown() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

Stops the executor service.

shutdown() - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Shuts down the scheduler.

shutdownNow() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

Stops the executor service.

size() - Method in class org.mpi_sws.jmc.runtime.TaskManager

Return the size of the task pool.

size() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack

Gets the size of the stack.

sort() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph.TopologicalSorter

Sorts the graph in topological order.

sortWithVisitor(ExecutionGraph.ExecutionGraphNodeVisitor) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph.TopologicalSorter

Sorts the graph in topological order and visits each node using the given visitor.

start() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcThread

start() - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Starts the scheduler thread.

START_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

stopAll() - Method in class org.mpi_sws.jmc.runtime.TaskManager

Stop all the tasks in the task pool.

storeTaskSchedule(String, List<? extends SchedulingChoice<?>>) - Static method in class org.mpi_sws.jmc.util.FileUtil

Stores the task schedule to a file in JSON format.

strategy() - Element in annotation interface org.mpi_sws.jmc.annotations.JmcCheckConfiguration

The strategy to use for the JMC check.

strategy(SchedulingStrategy) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration.Builder

strategyConstructor(SchedulingStrategyConfiguration.SchedulingStrategyConstructor) - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

strategyType(String) - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

StringUtil - Class in org.mpi_sws.jmc.util

Utility class for string operations.

StringUtil() - Constructor for class org.mpi_sws.jmc.util.StringUtil

submit(Runnable) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

submit(Runnable, T) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

submit(Callable<T>) - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcExecutorService

Submits a callable task to the executor service.

supplyAsync(Supplier<U>) - Static method in class org.mpi_sws.jmc.api.util.concurrent.JmcCompletableFuture

swapCoherency(ExecutionGraphNode, ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Resets the coherency order between the given write events.

SYM_ASSUME_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

SYMB_ARTH_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

SYMB_ASSERT_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

SYMB_ASSUME_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

SYMB_OP_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

syncBlockLock(Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Locks the block for the given instance.

syncBlockUnLock(Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Unlocks the block for the given instance.

syncMethodLock(Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Locks the corresponding lock of the given instance.

syncMethodLock(String) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Locks the corresponding lock of the given class's static synchronized method.

syncMethodUnLock(Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Unlocks the corresponding lock of the given instance.

syncMethodUnLock(String) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Unlocks the corresponding lock of the given class's static synchronized method.

T

TAKE_WORK_QUEUE - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

task(Long) - Static method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Creates a scheduling choice for a specific task without any value.

task(Long, T) - Static method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

Creates a scheduling choice for a specific task with a value.

TASK_ASSIGNED_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

TASK_CREATED_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

TaskAlreadyPaused - Exception Class in org.mpi_sws.jmc.runtime

Exception thrown when a task is already paused.

TaskAlreadyPaused() - Constructor for exception class org.mpi_sws.jmc.runtime.TaskAlreadyPaused

taskId(Long) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Builder

Sets the ID of the task that generated the event.

TaskManager - Class in org.mpi_sws.jmc.runtime

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.

TaskManager() - Constructor for class org.mpi_sws.jmc.runtime.TaskManager

Constructs a new TaskManager object.

TaskManager.TaskState - Enum Class in org.mpi_sws.jmc.runtime

The state of each task managed by the @RuntimeEnvironment is represented by one of the following.

TaskNotExists - Exception Class in org.mpi_sws.jmc.runtime

Exception thrown when a task does not exist.

TaskNotExists(Long) - Constructor for exception class org.mpi_sws.jmc.runtime.TaskNotExists

Constructs a new TaskNotExists exception with the specified thread ID.

teardown() - Method in interface org.mpi_sws.jmc.strategies.SchedulingStrategy

Teardown the strategy.

teardown() - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

teardown() - Method in class org.mpi_sws.jmc.strategies.trust.Algo

Cleans up the execution graph and the task schedule.

teardown() - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategy

teardown() - Method in class org.mpi_sws.jmc.strategies.trust.TrustStrategy

tearDown() - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Tears down the runtime by shutting down the scheduler adn clearing the task manager.

terminate(Long) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Terminates the task with the given ID.

terminate(Long) - Method in class org.mpi_sws.jmc.runtime.TaskManager

Terminates the task with the specified custom ID.

TERMINATED - Enum constant in enum class org.mpi_sws.jmc.runtime.TaskManager.TaskState

test(Event) - Method in interface org.mpi_sws.jmc.strategies.trust.Event.EventPredicate

Tests the event.

THREAD_POOL_CREATED - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

ThreadCreation - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Relation

ThreadJoin - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Relation

ThreadJoinCompletion - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Relation

ThreadLocation - Static variable in class org.mpi_sws.jmc.strategies.trust.LocationStore

ThreadStart - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Relation

timeout() - Static method in exception class org.mpi_sws.jmc.runtime.HaltCheckerException

Constructs a new HaltCheckerException indicating that the exploration was halted due to a timeout.

timeout(Duration) - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration.Builder

toJson() - Method in class org.mpi_sws.jmc.runtime.scheduling.PrimitiveValue

toJson() - Method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoiceValue

Converts this value to a JSON object.

toJson() - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

toJson() - Method in class org.mpi_sws.jmc.strategies.trust.Event

toJson() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

toJsonIgnoreLocation() - Method in class org.mpi_sws.jmc.strategies.trust.Event

toJsonIgnoreLocation() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphNode

toJsonString() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

toJsonStringIgnoreLocation() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

TopologicalSorter(ExecutionGraph) - Constructor for class org.mpi_sws.jmc.strategies.trust.ExecutionGraph.TopologicalSorter

Initializes a new topological sorter for the given graph.

toRuntimeConfiguration() - Method in class org.mpi_sws.jmc.checker.JmcCheckerConfiguration

Converts this configuration to a runtime configuration.

toString() - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent

toString() - Method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoice

toString() - Method in class org.mpi_sws.jmc.strategies.trust.CoverageGraph

toString() - Method in class org.mpi_sws.jmc.strategies.trust.Event.Key

toString() - Method in class org.mpi_sws.jmc.strategies.trust.Event

toString() - Method in class org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item

toString() - Method in enum class org.mpi_sws.jmc.strategies.trust.Relation

toString() - Method in record class org.mpi_sws.jmc.strategies.trust.SchedulingChoiceWrapper

Returns a string representation of this record class.

TotalOrder<T> - Interface in org.mpi_sws.jmc.util

Represents a generic total order relation.

TotalOrder.InvalidComparisonException - Exception Class in org.mpi_sws.jmc.util

Represents an exception thrown when an invalid comparison is attempted.

TotalOrder.Relation - Enum Class in org.mpi_sws.jmc.util

Represents the relation between two objects.

toVerboseString() - Method in class org.mpi_sws.jmc.strategies.trust.Event

TrackActiveTasksStrategy - Class in org.mpi_sws.jmc.strategies

A strategy that tracks the active tasks.

TrackActiveTasksStrategy() - Constructor for class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

Constructs a new TrackActiveTasksStrategy object.

TrackActiveTasksStrategy(List<TrackActiveTasksStrategy.Tracker>) - Constructor for class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

Constructs a new TrackActiveTasksStrategy object with the given trackers.

TrackActiveTasksStrategy.Tracker - Interface in org.mpi_sws.jmc.strategies

Tracks the active tasks based on events.

TrackActiveTasksStrategy.TrackLocks - Class in org.mpi_sws.jmc.strategies

Tracks the locks acquired and released events of tasks.

TrackActiveTasksStrategy.TrackTasks - Class in org.mpi_sws.jmc.strategies

Tracks the tasks start finish and join request events.

trackCoherency(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Tracks the coherency order between the given write event and the previous write event to the same location.

TrackLocks() - Constructor for class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy.TrackLocks

Constructs a new TrackLocks object.

TrackTasks() - Constructor for class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy.TrackTasks

Constructs a new TrackTasks object.

trackThreadCreates(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Tracks the thread starts in the execution graph as a total order

trackThreadJoinCompletion(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

trackThreadJoins(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Tracks thread join events in the execution graph.

trackThreadStarts(ExecutionGraphNode) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

trustSchedulingPolicy(TrustStrategy.SchedulingPolicy) - Method in class org.mpi_sws.jmc.strategies.SchedulingStrategyConfiguration.Builder

TrustStrategy - Class in org.mpi_sws.jmc.strategies.trust

A wrapper around the Algo algorithm that implements a scheduling strategy based on trust.

TrustStrategy() - Constructor for class org.mpi_sws.jmc.strategies.trust.TrustStrategy

TrustStrategy(Long, TrustStrategy.SchedulingPolicy, boolean, String) - Constructor for class org.mpi_sws.jmc.strategies.trust.TrustStrategy

TrustStrategy.SchedulingPolicy - Enum Class in org.mpi_sws.jmc.strategies.trust

type() - Method in class org.mpi_sws.jmc.runtime.scheduling.PrimitiveValue

type() - Method in class org.mpi_sws.jmc.runtime.scheduling.SchedulingChoiceValue

Returns the type of this value.

type(JmcRuntimeEvent.Type) - Method in class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Builder

Sets the type of the event.

U

unblockAllTasksForLock(Integer) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

unBlockTask(Long) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Unblocks the task with the given ID.

unit() - Element in annotation interface org.mpi_sws.jmc.annotations.JmcTimeout

The time unit for the timeout value.

unlock() - Method in class org.mpi_sws.jmc.api.util.concurrent.JmcReentrantLock

Releases the lock.

unpark(Thread) - Static method in class org.mpi_sws.jmc.api.util.concurrent.JmcLockSupport

Unpark the given thread.

UNPARK_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

UNRELATED - Enum constant in enum class org.mpi_sws.jmc.util.PartialOrder.Relation

unsafeCreateFile(String) - Static method in class org.mpi_sws.jmc.util.FileUtil

Creates a new file at the specified path, deleting it if it already exists.

unsafeEnsurePath(String) - Static method in class org.mpi_sws.jmc.util.FileUtil

Ensure the path exists, creating it if it does not.

unsafeIterator() - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

Returns List of nodes while silently ignoring any errors with cycles *

unsafeStoreToFile(String, String) - Static method in class org.mpi_sws.jmc.util.FileUtil

Stores the given content to a file at the specified path.

update(LamportVectorClock) - Method in class org.mpi_sws.jmc.util.LamportVectorClock

Updates the vector clock with the given vector clock.

updateEvent(JmcRuntimeEvent) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Adds a new event to the scheduler which is passed to the strategy.

updateEvent(JmcRuntimeEvent) - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Updates the event in the scheduling strategy.

updateEvent(JmcRuntimeEvent) - Method in class org.mpi_sws.jmc.strategies.RandomSchedulingStrategy

updateEvent(JmcRuntimeEvent) - Method in interface org.mpi_sws.jmc.strategies.SchedulingStrategy

Updates the strategy with the event that has occurred.

updateEvent(JmcRuntimeEvent) - Method in interface org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy.Tracker

Updates the event.

updateEvent(JmcRuntimeEvent) - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy.TrackLocks

Updates based on lock acquire and release events.

updateEvent(JmcRuntimeEvent) - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy.TrackTasks

updateEvent(JmcRuntimeEvent) - Method in class org.mpi_sws.jmc.strategies.TrackActiveTasksStrategy

updateEvent(JmcRuntimeEvent) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraphSimulator

updateEvent(JmcRuntimeEvent) - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategy

updateEvent(JmcRuntimeEvent) - Method in class org.mpi_sws.jmc.strategies.trust.TrustStrategy

updateEvent(Event) - Method in class org.mpi_sws.jmc.strategies.trust.Algo

Handles the visit with this event.

updateEventAndYield(JmcRuntimeEvent) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Adds a new event to the runtime and yields the control to the scheduler.

V

value() - Element in annotation interface org.mpi_sws.jmc.annotations.JmcExpectExecutions

The expected number of executions for the annotated test method or class.

value() - Element in annotation interface org.mpi_sws.jmc.annotations.JmcTimeout

The timeout value for the annotated test method or class.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.runtime.HaltExecutionException.Type

Returns the enum constant of this class with the specified name.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

Returns the enum constant of this class with the specified name.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.runtime.TaskManager.TaskState

Returns the enum constant of this class with the specified name.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

Returns the enum constant of this class with the specified name.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.strategies.trust.ExplorationStack.ItemType

Returns the enum constant of this class with the specified name.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.strategies.trust.Relation

Returns the enum constant of this class with the specified name.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.strategies.trust.TrustStrategy.SchedulingPolicy

Returns the enum constant of this class with the specified name.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.util.PartialOrder.Relation

Returns the enum constant of this class with the specified name.

valueOf(String) - Static method in enum class org.mpi_sws.jmc.util.TotalOrder.Relation

Returns the enum constant of this class with the specified name.

values() - Static method in enum class org.mpi_sws.jmc.runtime.HaltExecutionException.Type

Returns an array containing the constants of this enum class, in the order they are declared.

values() - Static method in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

Returns an array containing the constants of this enum class, in the order they are declared.

values() - Static method in enum class org.mpi_sws.jmc.runtime.TaskManager.TaskState

Returns an array containing the constants of this enum class, in the order they are declared.

values() - Static method in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

Returns an array containing the constants of this enum class, in the order they are declared.

values() - Static method in enum class org.mpi_sws.jmc.strategies.trust.ExplorationStack.ItemType

Returns an array containing the constants of this enum class, in the order they are declared.

values() - Static method in enum class org.mpi_sws.jmc.strategies.trust.Relation

Returns an array containing the constants of this enum class, in the order they are declared.

values() - Static method in enum class org.mpi_sws.jmc.strategies.trust.TrustStrategy.SchedulingPolicy

Returns an array containing the constants of this enum class, in the order they are declared.

values() - Static method in enum class org.mpi_sws.jmc.util.PartialOrder.Relation

Returns an array containing the constants of this enum class, in the order they are declared.

values() - Static method in enum class org.mpi_sws.jmc.util.TotalOrder.Relation

Returns an array containing the constants of this enum class, in the order they are declared.

visit(ExecutionGraphNode) - Method in interface org.mpi_sws.jmc.strategies.trust.ExecutionGraph.ExecutionGraphNodeVisitor

W

wait(Long) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

wait(Long) - Method in class org.mpi_sws.jmc.runtime.TaskManager

Wait for the task with the specified custom ID to complete.

WAIT_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

waitingForLock(Integer, Long) - Method in class org.mpi_sws.jmc.strategies.trust.ExecutionGraph

withFrequency(Duration) - Method in class org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder

WRITE - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

WRITE_EVENT - Enum constant in enum class org.mpi_sws.jmc.runtime.JmcRuntimeEvent.Type

WRITE_EX - Enum constant in enum class org.mpi_sws.jmc.strategies.trust.Event.Type

writeEvent(Object, String, String, String, Object) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Creates a write event for the specified value, owner, name, descriptor, and instance.

writeEventWithoutYield(Object, Object, String, String, String) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntimeUtils

Creates a write event for the specified value, owner, name, descriptor, and instance without yielding.

writeExecutionGraphToFile(String) - Method in class org.mpi_sws.jmc.strategies.trust.Algo

Writes the execution graph to a file.

Y

yield() - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Pauses the current task that invokes this method and yields the control to the scheduler.

yield() - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Pauses the current task and yields the control to the scheduler.

yield(Long) - Static method in class org.mpi_sws.jmc.runtime.JmcRuntime

Pauses the task with the given ID and yields the control to the scheduler.

yield(Long) - Method in class org.mpi_sws.jmc.runtime.scheduling.Scheduler

Pauses the task with the given ID and yields the control to the scheduler.

A B C D E F G H I J K L M N O P R S T U V W Y
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form