diff --git a/.gitignore b/.gitignore index 50cd5a5..5d73a4c 100644 --- a/.gitignore +++ b/.gitignore @@ -2,12 +2,14 @@ .tla # Ignore modules build directories -modules/tlc/ modules/build/ modules/dist/ +modules/lib/ +modules/tlc/ # Ignore TTrace specs *_TTrace_*.tla +*_TTrace_*.bin # Ignore TLC generated files *.out diff --git a/modules/src/GraphsExt.tla b/modules/src/GraphsExt.tla index a77ce82..7f87f56 100644 --- a/modules/src/GraphsExt.tla +++ b/modules/src/GraphsExt.tla @@ -15,7 +15,7 @@ LOCAL INSTANCE Naturals (******************************************************************************) ACGraphs(T, O) == UNION { - { g \in [node: {t \cup o}, edge: SUBSET ((t \X o) \cup (o \X t))] : + { g \in [node: {t \union o}, edge: SUBSET ((t \X o) \union (o \X t))] : /\ IsDag(g) /\ Roots(g) \subseteq o /\ Leaves(g) \subseteq o diff --git a/specs/GraphProcessing.tla b/specs/GraphProcessing.tla new file mode 100644 index 0000000..6dddaab --- /dev/null +++ b/specs/GraphProcessing.tla @@ -0,0 +1,436 @@ +---------------------------- MODULE GraphProcessing ---------------------------- +(*****************************************************************************) +(* This module specifies an abstract decentralized distributed task graph *) +(* processing system. *) +(* *) +(* - Tasks produce and consume data objects. *) +(* - Task and object dependencies form a directed acyclic bipartite graph. *) +(* - Agents (workers) dynamically process tasks. *) +(* - Tasks and objects may be dynamically registred over time. *) +(* *) +(* The specification defines the allowable transitions of the system, *) +(* together with its key safety and liveness properties. *) +(*****************************************************************************) + +EXTENDS FiniteSets, Graphs, Naturals, Sequences + +CONSTANTS + AgentId, \* Set of agent identifiers (theoretically infinite) + ObjectId, \* Set of object identifiers (theoretically infinite) + TaskId \* Set of task identifiers (theoretically infinite) + +ASSUME + \* Agent, task, and object identifiers are pairwise disjoint. + /\ AgentId \intersect ObjectId = {} + /\ AgentId \intersect TaskId = {} + /\ ObjectId \intersect TaskId = {} + +VARIABLES + agentTaskAlloc, \* agentTaskAlloc[a] is the set of tasks currently assigned to agent a + deps, \* deps is the directed dependency graph over task and object identifiers + objectState, \* objectState[o] records the current lifecycle state of object o + objectTargets, \* objectTargets is the set of objects currently marked as targets + taskState \* taskState[t] records the current lifecycle state of task t + +vars == << agentTaskAlloc, deps, objectState, objectTargets, taskState >> + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* MODULE INSTANCES *) +(*****************************************************************************) + +(** + * Instance of the ObjectStates module with SetOfObjectsIn operator provided. + *) +INSTANCE ObjectStates + WITH SetOfObjectsIn <- LAMBDA s : {o \in ObjectId: objectState[o] = s} + +(** + * Instance of the TaskStates module with SetOfTasksIn operator provided. + *) +INSTANCE TaskStates + WITH SetOfTasksIn <- LAMBDA s : {t \in TaskId: taskState[t] = s} + +(** + * Instance of the TaskProcessing specification. + *) +TP == INSTANCE TaskProcessing + +(** + * Instance of the ObjectProcessing specification. + *) +OP == INSTANCE ObjectProcessing + +------------------------------------------------------------------------------- + +(** + * TYPE INVARIANT + * Claims that all state variables always take values of the expected form. + * - Each agent is associated with a subset of tasks. + * - Each object has one of the defined object lifecycle states. + * - Targeted objects are valid object identifiers. + * - Each task has one of the defined task lifecycle states. + * - The dependency graph links only valid task and object identifiers + * and is a proper graph object (i.e., a record with 'node' and 'edge' + * as fields). + *) +TypeInv == + /\ agentTaskAlloc \in [AgentId -> SUBSET TaskId] + /\ objectState \in [ObjectId -> { + OBJECT_UNKNOWN, + OBJECT_REGISTERED, + OBJECT_FINALIZED + }] + /\ objectTargets \subseteq ObjectId + /\ taskState \in [TaskId -> { + TASK_UNKNOWN, + TASK_REGISTERED, + TASK_STAGED, + TASK_ASSIGNED, + TASK_PROCESSED, + TASK_FINALIZED + }] + /\ LET Nodes == TaskId \union ObjectId IN + deps \in [node: SUBSET Nodes, edge: SUBSET (Nodes \X Nodes)] + +(** + * Returns all nodes in graph 'G' labeled with task IDs. + *) +TaskNode(G) == G.node \intersect TaskId + +(** + * Returns all nodes in graph 'G' labeled with object IDs. + *) +ObjectNode(G) == G.node \intersect ObjectId + +(** + * Checks whether a graph is ArmoniK-compliant for the given task/object sets. + * A valid dependency graph must: + * - Be directed and acyclic. + * - Be bipartite with partitions (TaskId, ObjectId). + * - Have roots and leaves labeled by object identifiers. + * - Contain no isolated task nodes. + * - Not necessarily be connected. + *) +IsACGraph(G) == + /\ IsDag(G) + /\ IsBipartiteWithPartitions(G, TaskId, ObjectId) + /\ Roots(G) \subseteq ObjectId + /\ Leaves(G) \subseteq ObjectId + +(** + * A directed graph is unilaterally connected if, for every pair of vertices u + * and v, there is a directed path from u to v or a directed path from v to u + * (but not necessarily both). + *) +IsUnilaterallyConnectedGraph(G) == + \A u, v \in G.node : + u /= v => + \/ ConnectionsIn(G)[u, v] + \/ ConnectionsIn(G)[v, u] + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* SYSTEM INITIAL STATE AND TRANSITIONS *) +(*****************************************************************************) + +(** + * INITIAL STATE + * Initially, no tasks, objects, or dependencies exist. + *) +Init == + /\ TP!Init + /\ OP!Init + /\ deps = EmptyGraph + +(** + * GRAPH REGISTRATION + * A new graph 'G' of tasks and objects is submitted to the system. This + * registration must not affect the compliance of the dependency graph. + * In addition, it is not possible to modify the dependencies of tasks that have + * already been submitted, nor to submit tasks for which all output objects have + * already been finalized. + *) +RegisterGraph(G) == + LET + newDeps == GraphUnion(deps, G) + IN + /\ G /= EmptyGraph + /\ TaskNode(G) \subseteq UnknownTask + /\ \A t \in TaskNode(G): + ~(Successors(G, t) \subseteq FinalizedObject) + /\ IsACGraph(newDeps) + /\ deps' = newDeps + /\ objectState' = + [o \in ObjectId |-> + IF o \in G.node \intersect UnknownObject + THEN OBJECT_REGISTERED + ELSE objectState[o]] + /\ taskState' = + [t \in TaskId |-> + IF t \in G.node + THEN TASK_REGISTERED + ELSE taskState[t]] + /\ UNCHANGED << agentTaskAlloc, objectTargets >> + +(** + * OBJECT TARGETING + * A set 'O' of existing objects is marked as being targeted. Root objects + * cannot be targeted. + *) +TargetObjects(O) == + /\ OP!TargetObjects(O) + /\ UNCHANGED << agentTaskAlloc, deps, objectState, taskState >> + +(** + * OBJECT UNTARGETING + * A set 'O' of targeted objects is unmarked. + *) +UntargetObjects(O) == + /\ OP!UntargetObjects(O) + /\ UNCHANGED << agentTaskAlloc, deps, objectState, taskState >> + +(** + * OBJECT FINALIZATION + * A set 'O' of objects is finalized. Objects can be finalized if: + * - They have no producing tasks i.e., they are roots (external finalization), or + * - At least one of their producing tasks has been processed. + *) +FinalizeObjects(O) == + /\ \/ O \subseteq Roots(deps) + \/ \A o \in O: \E t \in Predecessors(deps, o): t \in ProcessedTask + /\ OP!FinalizeObjects(O) + /\ UNCHANGED << agentTaskAlloc, deps, objectTargets, taskState >> + +(** + * TASK STAGING + * A set 'T' of registered tasks becomes staged once all input objects + * are finalized. + *) +StageTasks(T) == + /\ T /= {} /\ T \subseteq RegisteredTask + /\ AllPredecessors(deps, T) \subseteq FinalizedObject + /\ taskState' = + [t \in TaskId |-> + IF t \in T THEN TASK_STAGED ELSE taskState[t]] + /\ UNCHANGED << agentTaskAlloc, deps, objectState, objectTargets >> + +(** + * TASK ASSIGNMENT + * An agent 'a' takes responsibility for processing a set 'T' of staged tasks. + *) +AssignTasks(a, T) == + /\ TP!AssignTasks(a, T) + /\ UNCHANGED << deps, objectState, objectTargets >> + +(** + * TASK RELEASE + * An agent 'a' postpones a set 'T' of tasks it currently holds. + *) +ReleaseTasks(a, T) == + /\ TP!ReleaseTasks(a, T) + /\ UNCHANGED << deps, objectState, objectTargets >> + +(** + * TASK PROCESSING + * An agent 'a' completes the processing of a set 'T' of tasks it currently + * holds. + *) +ProcessTasks(a, T) == + /\ TP!ProcessTasks(a, T) + /\ UNCHANGED << deps, objectState, objectTargets >> + +(** + * TASK FINALIZATION + * A set 'T' of processed tasks is finalized (i.e., post-processed) when all + * their output objects that can now only be produced by them are finalized. + * Indeed, an output object may have multiple parent tasks. So as long as there + * is at least one parent that has not been finalized, the others can ignore the + * object and finalize. + *) +FinalizeTasks(T) == + /\ T /= {} /\ T \subseteq ProcessedTask + /\ \A o \in AllSuccessors(deps, T) : + o \notin FinalizedObject + => \E t \in (Predecessors(deps, o) \ T) : t \notin FinalizedTask + /\ taskState' = + [t \in TaskId |-> + IF t \in T THEN TASK_FINALIZED ELSE taskState[t]] + /\ UNCHANGED << agentTaskAlloc, deps, objectState, objectTargets >> + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* FULL SYSTEM SPECIFICATION *) +(*****************************************************************************) + +(** + * NEXT-STATE RELATION + * Defines all atomic transitions of the system. + *) +Next == + \/ \E G \in Graphs(TaskId \union ObjectId): RegisterGraph(G) + \/ \E O \in SUBSET ObjectId: + \/ TargetObjects(O) + \/ UntargetObjects(O) + \/ FinalizeObjects(O) + \/ \E T \in SUBSET TaskId: + \/ StageTasks(T) + \/ \E a \in AgentId: + \/ AssignTasks(a, T) + \/ ReleaseTasks(a, T) + \/ ProcessTasks(a, T) + \/ FinalizeTasks(T) + +(** + * Returns TRUE iff task 't' is upstream on an open (i.e., fully unexecuted) + * production path toward an unfinalized target object 'o'. + * + * In other words, 't' can still produce (directly or indirectly) an output that + * may contribute to producing the target object 'o'. + *) +IsTaskUpstreamOnOpenPathToTarget(t, o) == + /\ o \in objectTargets + /\ o \in RegisteredObject + /\ t \in StagedTask + /\ \E p \in SimplePath(deps) : + /\ p[1] = t + /\ p[Len(p)] = o + /\ \A i \in 2..(Len(p) - 1) : + \/ (p[i] \in TaskId /\ p[i] \in RegisteredTask) + \/ (p[i] \in ObjectId /\ p[i] \in RegisteredObject) + +(** + * FAIRNESS CONDITIONS + * These conditions guarantee eventual progress for all eligible objects + * and tasks in the system: + * - Every object that becomes eligible for finalization is eventually finalized. + * - Every registered task whose input objects are finalized is eventually staged. + * - Every task that lies upstream on an open path toward some unfinalized + * target object is eventually assigned to an agent. + * - Every assigned task is eventually processed by some agent. + * - Every processed task whose outputs become eligible for finalization is + * eventually finalized. + *) +Fairness == + /\ \A o \in ObjectId : + WF_vars(FinalizeObjects({o})) + /\ \A t \in TaskId : + WF_vars(StageTasks({t})) + /\ \A t \in TaskId : + WF_vars( + /\ \E o \in ObjectId : + IsTaskUpstreamOnOpenPathToTarget(t, o) + /\ \E a \in AgentId : + AssignTasks(a, {t}) + ) + /\ \A t \in TaskId : + SF_vars( + \E a \in AgentId : + ProcessTasks(a, {t}) + ) + /\ \A t \in TaskId : + WF_vars(FinalizeTasks({t})) + +(** + * Full system specification. + *) +Spec == + /\ Init + /\ [][Next]_vars + /\ Fairness + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* SAFETY AND LIVENESS PROPERTIES *) +(*****************************************************************************) + +(** + * SAFETY + * The dependency graph is always ArmoniK-compliant. + *) +DependencyGraphCompliant == + IsACGraph(deps) + +(** + * SAFETY + * Ensures consistent relationships between graph structure and task/object + * states. + *) +GraphStateConsistent == + /\ TaskNode(deps) \intersect UnknownTask = {} + /\ ObjectNode(deps) \intersect UnknownObject = {} + /\ \A t \in TaskNode(deps): + t \notin RegisteredTask + => Predecessors(deps, t) \subseteq FinalizedObject + \* /\ \A o \in ObjectNode(deps) \ Roots(deps): + \* o \in FinalizedObject + \* => \E t \in Predecessors(deps, o): + \* t \in (ProcessedTask \union FinalizedTask) + +(** + * SAFETY + * Ensures that all targeted objects derive from root objects through a + * connected finalized subgraph. + *) +TargetsDerivedFromRoots == + \A o \in objectTargets: + o \in FinalizedObject => + \E subDeps \in DirectedSubgraph(deps): + /\ Roots(subDeps) \subseteq Roots(deps) + /\ Leaves(subDeps) = {o} + /\ IsUnilaterallyConnectedGraph(subDeps) + /\ (TaskNode(subDeps) \ Predecessors(subDeps, o)) \subseteq FinalizedTask + /\ Predecessors(subDeps, o) \subseteq (ProcessedTask \union FinalizedTask) + /\ ObjectNode(subDeps) \subseteq FinalizedObject + +(** + * SAFETY + * The data dependencies of each task remain immutable throughout execution. + *) +TaskDataDependenciesInvariant == + [][ + \A t \in TaskNode(deps): + /\ Predecessors(deps, t) = Predecessors(deps', t) + /\ Successors(deps, t) = Successors(deps', t) + ]_deps + +(** + * LIVENESS + * This specification refines the TaskProcessing specification. + *) +Mapping == + INSTANCE TaskProcessing WITH + taskState <- [t \in TaskId |-> + IF t \in RegisteredTask + THEN TASK_UNKNOWN + ELSE taskState[t]] + +TaskProcessingRefined == + Mapping!Spec + +(** + * LIVENESS + * This specification refines the ObjectProcessing specification. + *) +ObjectProcessingRefined == + OP!Spec + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* THEOREMS *) +(*****************************************************************************) + +THEOREM Spec => []TypeInv +THEOREM Spec => []DependencyGraphCompliant +THEOREM Spec => []GraphStateConsistent +THEOREM Spec => []TargetsDerivedFromRoots +THEOREM Spec => TaskDataDependenciesInvariant +THEOREM Spec => TaskProcessingRefined +THEOREM Spec => ObjectProcessingRefined + +================================================================================ \ No newline at end of file diff --git a/specs/GraphProcessing_mc.cfg b/specs/GraphProcessing_mc.cfg new file mode 100644 index 0000000..ee5122e --- /dev/null +++ b/specs/GraphProcessing_mc.cfg @@ -0,0 +1,29 @@ +CONSTANTS + \* Agent identifiers (model values) + AgentId = {a, b} + + \* Object identifiers (model values) + ObjectId = {o, p, q} + + \* Task identifiers (model values) + TaskId = {t, u, v} + + \* Override the Graphs operator with ACGraphs operator + Graphs <- MCGraphs + +SPECIFICATION + MCSpec + +INVARIANTS + TypeInv + DependencyGraphCompliant + GraphStateConsistent + \* TargetsDerivedFromRoots + +PROPERTIES + TaskDataDependenciesInvariant + TaskProcessingRefined + ObjectProcessingRefined + +\* SYMMETRY +\* Symmetry \ No newline at end of file diff --git a/specs/GraphProcessing_mc.tla b/specs/GraphProcessing_mc.tla new file mode 100644 index 0000000..018ae7d --- /dev/null +++ b/specs/GraphProcessing_mc.tla @@ -0,0 +1,83 @@ +-------------------------- MODULE GraphProcessing_mc -------------------------- +(*******************************************************************************) +(* Bounded model-checking extension of GraphProcessing. *) +(* *) +(* For model checking, the sets of task, objects and agent identifiers must *) +(* be finite and explicitly materialized. Since the number of tasks and *) +(* objects are finite, the system eventually reaches a state where no new *) +(* graph can be registered, which leads to an artificial deadlock. *) +(* *) +(* To avoid this spurious deadlock, the next-state action is overridden to *) +(* include a dummy terminal state, allowing the model checker to terminate *) +(* exploration gracefully. *) +(* *) +(* In addition, optimizations are provided to speed up model checking. *) +(*******************************************************************************) + +EXTENDS GraphsExt, GraphProcessing, Randomization, TLC + +ASSUME IsFiniteSet(AgentId) +ASSUME IsFiniteSet(ObjectId) +ASSUME IsFiniteSet(TaskId) + +-------------------------------------------------------------------------------- + +(** + * Returns the set of ArmoniK-compliant graphs on the set of object IDs and + * unused task IDs. This set is used with the 'RegisterGraph' action to avoid + * enumerating the set of all graphs for a given set of nodes that grows + * super-exponentially. By using this restricted set, only relevant cases are + * enumerated; indeed, if the subgraph is not ArmoniK-compliant, then it cannot + * be registered. + * + * Note: The ACGraphs operator is provided by the GraphsExt module. + *) +MCGraphs(Nodes) == + ACGraphs(Nodes \intersect UnknownTask, Nodes \intersect ObjectId) + +\* MCGraphsRand(Nodes) == +\* UNION { +\* { +\* g \in [ +\* node : {t \union o}, +\* edge : SUBSET ((t \X o) \union (o \X t)) +\* ] : IsACGraph(g) +\* } : t \in SUBSET T, o \in SUBSET O +\* } + +-------------------------------------------------------------------------------- + +(** + * Dummy action representing the terminal state of the system, reached once all + * targeted objects have been finalized. + *) +Terminating == + /\ objectTargets \subseteq FinalizedObject + /\ UNCHANGED vars + +(** + * Modified next-state action. Extends the original system behavior with the + * Terminating action to avoid artificial deadlocks due to the bounded task + * and object sets. + *) +MCNext == + \/ Next + \/ Terminating + +(** + * Modified full system specification. + *) +MCSpec == + /\ Init + /\ [][MCNext]_vars + /\ Fairness + +-------------------------------------------------------------------------------- + +(** + * Symmetry relation between task, object and agent identifiers. + *) +Symmetry == + Permutations(TaskId) \union Permutations(ObjectId) \union Permutations(AgentId) + +================================================================================ \ No newline at end of file diff --git a/specs/MCSimpleObjectProcessing.cfg b/specs/MCSimpleObjectProcessing.cfg deleted file mode 100644 index f608e8c..0000000 --- a/specs/MCSimpleObjectProcessing.cfg +++ /dev/null @@ -1,22 +0,0 @@ -CONSTANTS - \* Object identifiers (model values) - ObjectId = {o, p, q} - - \* Object status values (model values) - NULL = NULL - CREATED = CREATED - COMPLETED = COMPLETED - LOCKED = LOCKED - - -SPECIFICATION - MCSpec - - -INVARIANTS - TypeInv - - -PROPERTIES - EventualCompletion - Quiescence diff --git a/specs/MCSimpleTaskScheduling.cfg b/specs/MCSimpleTaskScheduling.cfg deleted file mode 100644 index 83f5849..0000000 --- a/specs/MCSimpleTaskScheduling.cfg +++ /dev/null @@ -1,28 +0,0 @@ -CONSTANTS - \* Agent identifiers (model values) - AgentId = {a, b, c} - - \* Task identifiers (model values) - TaskId = {t, u, v} - - \* Task status values (model values) - NULL = NULL - SUBMITTED = SUBMITTED - STARTED = STARTED - COMPLETED = COMPLETED - - -SPECIFICATION - MCSpec - - -INVARIANTS - TypeOk - ExecutionConsistency - StatusConsistency - NoExecutionConcurrency - - -PROPERTY - EventualCompletion - Quiescence diff --git a/specs/ObjectProcessing.tla b/specs/ObjectProcessing.tla new file mode 100644 index 0000000..385d3e1 --- /dev/null +++ b/specs/ObjectProcessing.tla @@ -0,0 +1,171 @@ +--------------------------- MODULE ObjectProcessing --------------------------- +(*****************************************************************************) +(* This module specifies an abstract data management system. *) +(* Objects represent data units with associated metadata and lifecycle *) +(* states. The specification abstracts away from object contents and focuses *) +(* solely on the allowed transitions between lifecycle states and targeting *) +(* behaviors. It also defines and asserts key safety and liveness properties *) +(* of the system. *) +(*****************************************************************************) + +CONSTANTS + ObjectId \* Set of object identifiers (theoretically infinite) + +VARIABLES + objectState, \* objectState[o] records the current lifecycle state of object o + objectTargets \* objectTargets is the set of objects currently marked as targets + +vars == << objectState, objectTargets >> + +------------------------------------------------------------------------------- + +(** + * Instance of the ObjectStates module with SetOfObjectsIn operator provided. + *) +INSTANCE ObjectStates + WITH SetOfObjectsIn <- LAMBDA s : {o \in ObjectId: objectState[o] = s} + +(** + * TYPE INVARIANT + * Claims that all state variables always take values of the expected form. + * - objectState is a function mapping each object to one of the defined states. + * - objectTargets is a subset of valid object identifiers. + *) +TypeInv == + /\ objectState \in [ObjectId -> { + OBJECT_UNKNOWN, + OBJECT_REGISTERED, + OBJECT_FINALIZED + }] + /\ objectTargets \in SUBSET ObjectId + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* SYSTEM INITIAL STATE AND TRANSITIONS *) +(*****************************************************************************) + +(** + * INITIAL STATE + * Initially, all objects are unknown and none are marked as targets. + *) +Init == + /\ objectState = [o \in ObjectId |-> OBJECT_UNKNOWN] + /\ objectTargets = {} + +(** + * OBJECT REGISTRATION + * A new set 'O' of objects is registered in the system, i.e., it is created + * with the metadata provided and empty data. + *) +RegisterObjects(O) == + /\ O /= {} /\ O \subseteq UnknownObject + /\ objectState' = + [o \in ObjectId |-> IF o \in O THEN OBJECT_REGISTERED ELSE objectState[o]] + /\ UNCHANGED objectTargets + +(** + * OBJECT TARGETING + * A set 'O' of existing objects is marked as targeted, meaning that the user + * wants these objects to be finalized. + *) +TargetObjects(O) == + /\ O /= {} /\ O \subseteq (RegisteredObject \union FinalizedObject) + /\ objectTargets' = objectTargets \union O + /\ UNCHANGED objectState + +(** + * OBJECT UNTARGETING + * A set 'O' of currently targeted objects is unmarked. + *) +UntargetObjects(O) == + /\ O /= {} /\ O \subseteq objectTargets + /\ objectTargets' = objectTargets \ O + /\ UNCHANGED objectState + +(** + * OBJECT FINALIZATION + * A set 'O' of objects is finalized, meaning that these objects are now + * immutable (will never be modified). + *) +FinalizeObjects(O) == + /\ O /= {} /\ O \subseteq RegisteredObject + /\ objectState' = + [o \in ObjectId |-> IF o \in O THEN OBJECT_FINALIZED ELSE objectState[o]] + /\ UNCHANGED objectTargets + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* FULL SYSTEM SPECIFICATION *) +(*****************************************************************************) + +(** + * NEXT-STATE RELATION + * Defines all possible atomic transitions of the system. + *) +Next == + \E O \in SUBSET ObjectId: + \/ RegisterObjects(O) + \/ TargetObjects(O) + \/ UntargetObjects(O) + \/ FinalizeObjects(O) + +(** + * FAIRNESS CONDITIONS + * Ensure that progress is eventually made for actionable objects. + * - A targeted object cannot remain indefinitely registered without being + * eventually finalized. + *) +Fairness == + /\ \A o \in ObjectId: WF_vars(o \in objectTargets /\ FinalizeObjects({o})) + +(** + * Full system specification. + *) +Spec == + /\ Init + /\ [][Next]_vars + /\ Fairness + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* SAFETY AND LIVENESS PROPERTIES *) +(*****************************************************************************) + +(** + * SAFETY + * An object can only be targeted if it is known to the system. + *) +TargetStateConsistent == + objectTargets \intersect UnknownObject = {} + +(** + * LIVENESS + * Every targeted object is eventually either finalized or untargeted. + *) +EventualTargetFinalization == + \A o \in ObjectId: + o \in objectTargets ~> (o \in FinalizedObject \/ o \notin objectTargets) + +(** + * LIVENESS + * Once an object reaches the FINALIZED state, it remains there permanently. + *) +PermanentFinalization == + \A o \in ObjectId: + [](o \in FinalizedObject => [](o \in FinalizedObject)) + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* THEOREMS *) +(*****************************************************************************) + +THEOREM Spec => []TypeInv +THEOREM Spec => []TargetStateConsistent +THEOREM Spec => EventualTargetFinalization +THEOREM Spec => PermanentFinalization + +=============================================================================== \ No newline at end of file diff --git a/specs/ObjectProcessing_mc.cfg b/specs/ObjectProcessing_mc.cfg new file mode 100644 index 0000000..636832e --- /dev/null +++ b/specs/ObjectProcessing_mc.cfg @@ -0,0 +1,14 @@ +CONSTANTS + \* Object identifiers (model values) + ObjectId = {o, p, q} + +SPECIFICATION + MCSpec + +INVARIANTS + TypeInv + TargetStateConsistent + +PROPERTIES + EventualTargetFinalization + PermanentFinalization diff --git a/specs/MCSimpleObjectProcessing.tla b/specs/ObjectProcessing_mc.tla similarity index 77% rename from specs/MCSimpleObjectProcessing.tla rename to specs/ObjectProcessing_mc.tla index c83780a..7d16269 100644 --- a/specs/MCSimpleObjectProcessing.tla +++ b/specs/ObjectProcessing_mc.tla @@ -1,17 +1,18 @@ ------------------------ MODULE MCSimpleObjectProcessing ------------------------ +-------------------------- MODULE ObjectProcessing_mc -------------------------- (******************************************************************************) -(* Bounded model-checking extension of SimpleObjectScheduling. *) +(* Bounded model-checking extension of ObjectProcessing. *) (* *) (* For model checking, the set of object identifiers must be finite and *) (* explicitly materialized. Since the number of objects is finite, the system *) -(* eventually reaches a state where all objects are completed, which leads to *) -(* an artificial deadlock. *) +(* eventually reaches a state where no new objects can be registered which, *) +(* leads to an artificial deadlock. *) (* *) (* To avoid this spurious deadlock, the next-state action is overridden to *) (* include a dummy terminal state, allowing the model checker to terminate *) (* exploration gracefully. *) (******************************************************************************) -EXTENDS FiniteSets, SimpleObjectProcessing + +EXTENDS FiniteSets, ObjectProcessing ASSUME IsFiniteSet(ObjectId) @@ -19,10 +20,10 @@ ASSUME IsFiniteSet(ObjectId) (** * Dummy action representing the terminal state of the system, reached once all - * objects have been completed. + * targeted objects have been finalized. *) Terminating == - /\ \A o \in ObjectId: IsCompleted({o}) \/ IsLocked({o}) + /\ objectTargets \subseteq FinalizedObject /\ UNCHANGED vars (** diff --git a/specs/ObjectStates.tla b/specs/ObjectStates.tla new file mode 100644 index 0000000..0a4efe6 --- /dev/null +++ b/specs/ObjectStates.tla @@ -0,0 +1,48 @@ +----------------------------- MODULE ObjectStates ----------------------------- +(*****************************************************************************) +(* This module defines the possible states of an object in the scheduling *) +(* system. A state represents a phase in the object lifecycle, from *) +(* registration to finalization. *) +(* *) +(* The module also provides definitions of object sets in each state, *) +(* allowing other specifications to reason about groups of objects sharing *) +(* the same lifecycle phase. *) +(*****************************************************************************) + +LOCAL INSTANCE FiniteSets + +(** + * Abstract operator returning the set of objects in a given state. + *) +CONSTANT + SetOfObjectsIn(_) \* To be implemented by modules extending this one with + \* state variables. + +(** + * Object states in their lifecycle. + *) +OBJECT_UNKNOWN == "OBJECT_UNKNOWN" \* Object is virtual, not yet known to the system +OBJECT_REGISTERED == "OBJECT_REGISTERED" \* Object created with only its metadata and empty data. +OBJECT_FINALIZED == "OBJECT_FINALIZED" \* Object has been successfully generated + +(** + * Set of all object states. + *) +ObjectState == + {OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED} + +(** + * SetOfObjectsIn must return a finite set for each object state. + *) +AXIOM + \A s \in ObjectState: + IsFiniteSet(SetOfObjectsIn(s)) + +(** + * Sets of objects by state. + *) +UnknownObject == SetOfObjectsIn(OBJECT_UNKNOWN) +RegisteredObject == SetOfObjectsIn(OBJECT_REGISTERED) +FinalizedObject == SetOfObjectsIn(OBJECT_FINALIZED) + +=============================================================================== \ No newline at end of file diff --git a/specs/SimpleObjectProcessing.tla b/specs/SimpleObjectProcessing.tla deleted file mode 100644 index 38d0664..0000000 --- a/specs/SimpleObjectProcessing.tla +++ /dev/null @@ -1,139 +0,0 @@ ------------------------- MODULE SimpleObjectProcessing ------------------------- -(******************************************************************************) -(* This specification models an abstract data management system. Data are *) -(* represented as uniquely identified objects. The specification abstracts *) -(* from the internal contents of objects and focuses solely on their *) -(* lifecycle and processing. *) -(******************************************************************************) -EXTENDS FiniteSets - -CONSTANT - \* @type: Set(Str); - ObjectId \* Set of object identifiers (theoretically infinite). - -CONSTANTS - \* @type: Str; - NULL, \* Status of an object not yet known to the system. - \* @type: Str; - CREATED, \* Status of a known object whose data is empty. - \* @type: Str; - COMPLETED, \* Status of an object whose data has been completed. - \* @type: Str; - LOCKED \* Status of an object whose data can no longer be overwritten. - -ObjectStatus == {NULL, CREATED, COMPLETED, LOCKED} - -ASSUME Assumptions == - \* The statuses are different from one another. - Cardinality(ObjectStatus) = 4 - -VARIABLES - \* @type: Str -> Str; - status \* status[o] is the status of object o. - -(** - * @type: < Str>>; - * Tuple of all variables. - *) -vars == << status >> - --------------------------------------------------------------------------------- - -(** - * Type invariant property. - *) -TypeInv == - \* Each object is always in one of the four possible states. - status \in [ObjectId -> ObjectStatus] - -(** - * Helpers to check the uniform status of a set of objects. - *) -IsInStatus(S, STATUS) == - \A x \in S: status[x] = STATUS - -IsUnknown(S) == IsInStatus(S, NULL) -IsCreated(S) == IsInStatus(S, CREATED) -IsCompleted(S) == IsInStatus(S, COMPLETED) -IsLocked(S) == IsInStatus(S, LOCKED) - --------------------------------------------------------------------------------- - -(** - * Initial state predicate: No objects are stored in the system. - *) -Init == - status = [o \in ObjectId |-> NULL] - -(** - * Action predicate: A non-empty set S of new objects is created. - *) -Create(S) == - /\ S /= {} /\ IsUnknown(S) - /\ status' = [o \in ObjectId |-> IF o \in S THEN CREATED ELSE status[o]] - -(** - * Action predicate: A non-empty set S of objects is completed, i.e., their data - * is written. For objects whose data already exists, it is overwritten. - *) -Complete(S) == - /\ S /= {} /\ (\A o \in S: IsCreated({o}) \/ IsCompleted({o})) - /\ status' = [o \in ObjectId |-> IF o \in S THEN COMPLETED ELSE status[o]] - -(** - * Action predicate: A non-empty set S of objects are locked, preventing the - * associated data from being overwritten. - *) -Lock(S) == - /\ S /= {} /\ (\A o \in S: IsCompleted({o}) \/ IsLocked({o})) - /\ status' = [o \in ObjectId |-> IF o \in S THEN LOCKED ELSE status[o]] - -(** - * Next-state relation. - *) -Next == - \E S \in SUBSET ObjectId: - \/ Create(S) - \/ Complete(S) - \/ Lock(S) - --------------------------------------------------------------------------------- - -(** - * Fairness properties. - *) -Fairness == - \* Weak fairness property: All objects stored in the system have their data - \* eventually completed. - /\ \A o \in ObjectId: WF_vars(Complete({o})) - -(** - * Full system specification with fairness properties. - *) -Spec == - /\ Init - /\ [][Next]_vars - /\ Fairness - --------------------------------------------------------------------------------- - -(** - * Liveness property: Every created object is eventually completed. - *) -EventualCompletion == - \A o \in ObjectId: IsCreated({o}) ~> IsCompleted({o}) - -(** - * Liveness property: Once an object (or set of objects) is locked, it stays - * locked forever. - *) -Quiescence == - \A o \in ObjectId: [](IsLocked({o}) => []IsLocked({o})) - --------------------------------------------------------------------------------- - -THEOREM Spec => []TypeInv -THEOREM Spec => EventualCompletion -THEOREM Spec => Quiescence - -================================================================================ \ No newline at end of file diff --git a/specs/SimpleTaskScheduling.tla b/specs/SimpleTaskScheduling.tla deleted file mode 100644 index 7c95075..0000000 --- a/specs/SimpleTaskScheduling.tla +++ /dev/null @@ -1,191 +0,0 @@ -------------------------- MODULE SimpleTaskScheduling -------------------------- -(******************************************************************************) -(* This specification models a decentralized online task scheduling system** *) -(* in which dynamically submitted tasks are executed by a varying unknown *) -(* number of agents. *) -(* *) -(* The specification abstracts away from concrete execution policies, *) -(* focusing on the possible behaviors of task assignment and progress. *) -(******************************************************************************) -EXTENDS FiniteSets - -CONSTANTS - \* @type: Set(Str); - AgentId, \* Set of agent identifiers (theoretically infinite). - \* @type: Set(Str); - TaskId \* Set of task identifiers (theoretically infinite). - -CONSTANTS \* Describe this block of constants (same above) - \* @type: Str; - NULL, \* Status of a task not yet known to the system. - \* @type: Str; - SUBMITTED, \* Status of a task ready for execution. - \* @type: Str; - STARTED, \* Status of a task currently being processed. - \* @type: Str; - COMPLETED \* Status of a task that has been successfully processed. - -TaskStatus == {NULL, SUBMITTED, STARTED, COMPLETED} - -ASSUME Assumptions == - \* AgentId and TaskId are two disjoint sets - /\ AgentId \cap TaskId = {} - \* The statuses are different from one another. - /\ Cardinality(TaskStatus) = 4 - -VARIABLES - \* @type: Str -> Set(Str); - alloc, \* alloc[a] is the set of tasks currently scheduled on agent a. - \* @type: Str -> Str; - status \* status[t] is the execution status of task t. - -(** - * Tuple of all variables. - *) -vars == << alloc, status >> - --------------------------------------------------------------------------------- - -(** - * Type invariant property. - *) -TypeOk == - \* Each agent is associated with a subset of tasks. - /\ alloc \in [AgentId -> SUBSET TaskId] - \* Each task has one of the four possible states. - /\ status \in [TaskId -> TaskStatus] - -(** - * Helpers to check the uniform status of a set of tasks. - *) -IsInStatus(S, STATUS) == - \A t \in S: status[t] = STATUS - -IsUnknown(S) == IsInStatus(S, NULL) -IsSubmitted(S) == IsInStatus(S, SUBMITTED) -IsStarted(S) == IsInStatus(S, STARTED) -IsCompleted(S) == IsInStatus(S, COMPLETED) - --------------------------------------------------------------------------------- - -(** - * Initial state predicate: No tasks are submitted or scheduled. - *) -Init == - /\ alloc = [a \in AgentId |-> {}] - /\ status = [t \in TaskId |-> NULL] - -(** - * Action predicate: A non-empty set S of previously unknown tasks is submitted, - * i.e., made available for scheduling. - *) -Submit(S) == - /\ S /= {} /\ IsUnknown(S) - /\ status' = [t \in TaskId |-> IF t \in S THEN SUBMITTED ELSE status[t]] - /\ UNCHANGED alloc - -(** - * Action predicate: A non-empty set S of submitted tasks are scheduled on - * agent a. - *) -Schedule(a, S) == - /\ S /= {} /\ IsSubmitted(S) - /\ alloc' = [alloc EXCEPT ![a] = @ \union S] - /\ status' = [t \in TaskId |-> IF t \in S THEN STARTED ELSE status[t]] - -(** - * Action predicate: Agent a releases a non-empty set S of tasks that it - * currently holds. - *) -Release(a, S) == - /\ S /= {} /\ S \subseteq alloc[a] - /\ alloc' = [alloc EXCEPT ![a] = @ \ S] - /\ status' = [t \in TaskId |-> IF t \in S THEN SUBMITTED ELSE status[t]] - -(** - * Action predicate: Agent a completes the execution of a non-empty set S of - * tasks that it currently holds. - *) -Complete(a, S) == - /\ S /= {} /\ S \subseteq alloc[a] - /\ alloc' = [alloc EXCEPT ![a] = @ \ S] - /\ status' = [t \in TaskId |-> IF t \in S THEN COMPLETED ELSE status[t]] - -(** - * Next-state relation. - *) -Next == - \E S \in SUBSET TaskId: - \/ Submit(S) - \/ \E a \in AgentId: - \/ Schedule(a, S) - \/ Release(a, S) - \/ Complete(a, S) - --------------------------------------------------------------------------------- - -(** - * Fairness properties. - *) -Fairness == - \* Weak fairness property: Ready tasks cannot wait indefinitely and end up - \* being scheduled on an agent. - /\ \A t \in TaskId: WF_vars(\E a \in AgentId: Schedule(a, {t})) - \* Strong fairness property: Tasks cannot run indefinitely or be - \* systematically released. - /\ \A t \in TaskId: SF_vars(\E a \in AgentId: Complete(a, {t})) - -(** - * Full system specification. - *) -Spec == - /\ Init - /\ [][Next]_vars - /\ Fairness - --------------------------------------------------------------------------------- - -(** - * Invariant: The set of all scheduled tasks is always a subset of the - * overall task set. - *) -ExecutionConsistency == - UNION {alloc[a]: a \in AgentId} \subseteq {t: t \in TaskId} - -(** - * Invariant: A task is assigned to some agent if and only if it is in the - * STARTED state. - *) -StatusConsistency == - \A t \in TaskId: - \/ IsStarted({t}) /\ \E a \in AgentId: t \in alloc[a] - \/ ~IsStarted({t}) /\ \A a \in AgentId: t \notin alloc[a] - -(** - * Invariant: A task cannot be executed simultaneously by multiple agents. - *) -NoExecutionConcurrency == - \A a, b \in AgentId: a /= b => alloc[a] \intersect alloc[b] = {} - -(** - * Liveness property: Any submitted task is eventually completed. - *) -EventualCompletion == - \A t \in TaskId: IsSubmitted({t}) ~> IsCompleted({t}) - -(** - * Liveness property: Once a task is completed, it remains completed forever. - *) -Quiescence == - \A t \in TaskId: [](IsCompleted({t}) => []IsCompleted({t})) - --------------------------------------------------------------------------------- - -THEOREM Spec => []TypeOk -THEOREM Spec => []ExecutionConsistency -THEOREM Spec => []StatusConsistency -THEOREM Spec => []NoExecutionConcurrency -THEOREM Spec => EventualCompletion -THEOREM Spec => Quiescence - -================================================================================ \ No newline at end of file diff --git a/specs/TaskProcessing.tla b/specs/TaskProcessing.tla new file mode 100644 index 0000000..cdc8078 --- /dev/null +++ b/specs/TaskProcessing.tla @@ -0,0 +1,213 @@ +---------------------------- MODULE TaskProcessing ---------------------------- +(*****************************************************************************) +(* This module specifies an abstract distributed task scheduling system. *) +(* Tasks are dynamically submitted and executed by a varying, unknown set of *) +(* agents. The specification models the allowed behaviors of task assignment *) +(* and processing, abstracting away from concrete scheduling or coordination *) +(* mechanisms. It also defines and asserts key safety and liveness *) +(* properties of the system. *) +(*****************************************************************************) + +CONSTANTS + AgentId, \* Set of agent identifiers (theoretically infinite) + TaskId \* Set of task identifiers (theoretically infinite) + +ASSUME + \* Agent and task identifier sets are disjoint + AgentId \intersect TaskId = {} + +VARIABLES + agentTaskAlloc, \* agentTaskAlloc[a] is the set of tasks currently assigned to agent a + taskState \* taskState[t] records the current lifecycle state of task t + +vars == << agentTaskAlloc, taskState >> + +------------------------------------------------------------------------------- + +(** + * Instance of the TaskStates module with SetOfTasksIn operator provided. + *) +INSTANCE TaskStates + WITH SetOfTasksIn <- LAMBDA s : {t \in TaskId: taskState[t] = s} + +(** + * TYPE INVARIANT + * Claims that all state variables always take values of the expected form. + * - agentTaskAlloc is a function mapping each agent to a subset of tasks. + * - taskState is a function mapping each task to one of the defined states. + *) +TypeInv == + /\ agentTaskAlloc \in [AgentId -> SUBSET TaskId] + /\ taskState \in [TaskId -> { + TASK_UNKNOWN, + TASK_STAGED, + TASK_ASSIGNED, + TASK_PROCESSED, + TASK_FINALIZED + }] + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* SYSTEM INITIAL STATE AND TRANSITIONS *) +(*****************************************************************************) + +(** + * INITIAL STATE + * Initially, no task has been registered and no agent holds any task. + *) +Init == + /\ agentTaskAlloc = [a \in AgentId |-> {}] + /\ taskState = [t \in TaskId |-> TASK_UNKNOWN] + +(** + * TASK STAGING + * A new set 'T' of tasks is staged i.e., made available to the system for processing. + *) +StageTasks(T) == + /\ T /= {} /\ T \subseteq UnknownTask + /\ taskState' = + [t \in TaskId |-> IF t \in T THEN TASK_STAGED ELSE taskState[t]] + /\ UNCHANGED agentTaskAlloc + +(** + * TASK ASSIGNMENT + * An agent 'a' takes responsibility for processing a set 'T' of staged + * tasks. + *) +AssignTasks(a, T) == + /\ T /= {} /\ T \subseteq StagedTask + /\ agentTaskAlloc' = [agentTaskAlloc EXCEPT ![a] = @ \union T] + /\ taskState' = + [t \in TaskId |-> IF t \in T THEN TASK_ASSIGNED ELSE taskState[t]] + +(** + * TASK RELEASE + * An agent 'a' postpones a set 'T' of tasks it currently holds. + *) +ReleaseTasks(a, T) == + /\ T /= {} /\ T \subseteq agentTaskAlloc[a] + /\ agentTaskAlloc' = [agentTaskAlloc EXCEPT ![a] = @ \ T] + /\ taskState' = + [t \in TaskId |-> IF t \in T THEN TASK_STAGED ELSE taskState[t]] + +(** + * TASK PROCESSING + * An agent 'a' completes the processing of a set 'T' of tasks it currently + * holds. + *) +ProcessTasks(a, T) == + /\ T /= {} /\ T \subseteq agentTaskAlloc[a] + /\ agentTaskAlloc' = [agentTaskAlloc EXCEPT ![a] = @ \ T] + /\ taskState' = + [t \in TaskId |-> IF t \in T THEN TASK_PROCESSED ELSE taskState[t]] + +(** + * TASK POST-PROCESSING + * A set 'T' of tasks is post-processed. + *) +FinalizeTasks(T) == + /\ T /= {} /\ T \subseteq ProcessedTask + /\ taskState' = + [t \in TaskId |-> IF t \in T THEN TASK_FINALIZED ELSE taskState[t]] + /\ UNCHANGED agentTaskAlloc + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* FULL SYSTEM SPECIFICATION *) +(*****************************************************************************) + +(** + * NEXT-STATE RELATION + * Defines all possible atomic transitions of the system. + *) +Next == + \E T \in SUBSET TaskId: + \/ StageTasks(T) + \/ \E a \in AgentId: + \/ AssignTasks(a, T) + \/ ReleaseTasks(a, T) + \/ ProcessTasks(a, T) + \/ FinalizeTasks(T) + +(** + * FAIRNESS CONDITIONS + * Ensure that progress is eventually made for tasks that can act. + * - A task cannot be assigned to an agent an infinite number of times + * without eventually being processed. + * - A task cannot remain indefinitely processed without being eventually + * finalized. + *) +Fairness == + /\ \A t \in TaskId: SF_vars(\E a \in AgentId : ProcessTasks(a, {t})) + /\ \A t \in TaskId: WF_vars(FinalizeTasks({t})) + +(** + * Full system specification. + *) +Spec == + /\ Init + /\ [][Next]_vars + /\ Fairness + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* SAFETY AND LIVENESS PROPERTIES *) +(*****************************************************************************) + +(** + * SAFETY + * The set of all allocated tasks always belongs to the universe of tasks. + *) +AllocConsistent == + UNION {agentTaskAlloc[a] : a \in AgentId} \subseteq TaskId + +(** + * SAFETY + * A task is assigned to an agent if and only if it is in the ASISGNED state. + *) +AllocStateConsistent == + \A t \in TaskId: + t \in AssignedTask <=> \E a \in AgentId: t \in agentTaskAlloc[a] + +(** + * SAFETY + * No task is held by multiple agents at the same time* + *) +ExclusiveAssignment == + \A a, b \in AgentId : + a /= b => agentTaskAlloc[a] \intersect agentTaskAlloc[b] = {} + +(** + * LIVENESS + * Any staged task ultimately remains in the STAGED or FINALIZED state. + *) +EventualQuiescence == + \A t \in TaskId : + t \notin UnknownTask ~> + \/ [](t \in StagedTask) + \/ [](t \in FinalizedTask) + +(** + * LIVENESS + * Once a task reaches the FINALIZED state, it remains there permanently. + *) +PermanentFinalization == + \A t \in TaskId: [](t \in FinalizedTask => [](t \in FinalizedTask)) + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* THEOREMS *) +(*****************************************************************************) + +THEOREM Spec => []TypeInv +THEOREM Spec => []AllocConsistent +THEOREM Spec => []AllocStateConsistent +THEOREM Spec => []ExclusiveAssignment +THEOREM Spec => EventualQuiescence +THEOREM Spec => PermanentFinalization + +============================================================================= \ No newline at end of file diff --git a/specs/TaskProcessing_mc.cfg b/specs/TaskProcessing_mc.cfg new file mode 100644 index 0000000..270bebe --- /dev/null +++ b/specs/TaskProcessing_mc.cfg @@ -0,0 +1,19 @@ +CONSTANTS + \* Agent identifiers (model values) + AgentId = {a, b, c} + + \* Task identifiers (model values) + TaskId = {t, u, v} + +SPECIFICATION + MCSpec + +INVARIANTS + TypeInv + AllocConsistent + AllocStateConsistent + ExclusiveAssignment + +PROPERTY + EventualQuiescence + PermanentFinalization diff --git a/specs/MCSimpleTaskScheduling.tla b/specs/TaskProcessing_mc.tla similarity index 65% rename from specs/MCSimpleTaskScheduling.tla rename to specs/TaskProcessing_mc.tla index 9822ffc..c04caaf 100644 --- a/specs/MCSimpleTaskScheduling.tla +++ b/specs/TaskProcessing_mc.tla @@ -1,17 +1,18 @@ ------------------------- MODULE MCSimpleTaskScheduling ------------------------- -(******************************************************************************) -(* Bounded model-checking extension of SimpleTaskScheduling. *) -(* *) -(* For model checking, both the sets of task identifiers and agent *) -(* identifiers must be finite and explicitly materialized. Since the *) -(* number of tasks is finite, the system eventually reaches a state where all *) -(* tasks are executed, which leads to an artificial deadlock. *) -(* *) -(* To avoid this spurious deadlock, the next-state action is overridden to *) -(* include a dummy terminal state, allowing the model checker to terminate *) -(* exploration gracefully. *) -(******************************************************************************) -EXTENDS FiniteSets, SimpleTaskScheduling +--------------------------- MODULE TaskProcessing_mc --------------------------- +(*****************************************************************************) +(* Bounded model-checking extension of TaskProcessing. *) +(* *) +(* For model checking, both the sets of task identifiers and agent *) +(* identifiers must be finite and explicitly materialized. Since the *) +(* number of tasks is finite, the system may eventually reaches a state *) +(* where no new tasks can be staged, which leads to an artificial deadlock. *) +(* *) +(* To avoid this spurious deadlock, the next-state action is overridden to *) +(* include a dummy terminal state, allowing the model checker to complete *) +(* exploration gracefully. *) +(*****************************************************************************) + +EXTENDS FiniteSets, TaskProcessing ASSUME IsFiniteSet(TaskId) ASSUME IsFiniteSet(AgentId) @@ -19,11 +20,12 @@ ASSUME IsFiniteSet(AgentId) -------------------------------------------------------------------------------- (** - * Dummy action representing the terminal state of the system, reached once all - * tasks have been completed. + * Dummy action representing the terminal state of the system, reached when + * there are no more tasks being processed (i.e., assigned to an agent or not + * yet finalized). *) Terminating == - /\ IsCompleted(TaskId) + /\ TaskId = UnknownTask \union StagedTask \union FinalizedTask /\ UNCHANGED vars (** diff --git a/specs/TaskStates.tla b/specs/TaskStates.tla new file mode 100644 index 0000000..549e6f3 --- /dev/null +++ b/specs/TaskStates.tla @@ -0,0 +1,61 @@ +------------------------------ MODULE TaskStates ------------------------------ +(*****************************************************************************) +(* This module defines the possible states of a task in the scheduling *) +(* system. A state represents a phase in the task lifecycle, from submission *) +(* to final post-processing. *) +(* *) +(* The module also provides definitions of task sets in each state, allowing *) +(* other specifications to reason about groups of tasks sharing the same *) +(* lifecycle phase. *) +(*****************************************************************************) + +LOCAL INSTANCE FiniteSets + +(** + * Abstract operator returning the set of tasks in a given state. + *) +CONSTANT + SetOfTasksIn(_) \* To be implemented by modules extending this one with + \* state variables. + +(** + * Task states in their lifecycle. + *) +TASK_UNKNOWN == "TASK_UNKNOWN" \* Task is virtual, not yet known to the system +TASK_REGISTERED == "TASK_REGISTERED" \* Task is known to the system and pending readiness for processing +TASK_STAGED == "TASK_STAGED" \* Task is ready for processing +TASK_ASSIGNED == "TASK_ASSIGNED" \* Task is assigned to an agent for processing +TASK_PROCESSED == "TASK_PROCESSED" \* Task processing completed +TASK_FINALIZED == "TASK_FINALIZED" \* Task post-processing is completed + +(** + * Set of all task states. + *) +TaskState == + { + TASK_UNKNOWN, + TASK_REGISTERED, + TASK_STAGED, + TASK_ASSIGNED, + TASK_PROCESSED, + TASK_FINALIZED + } + +(** + * SetOfTasksIn must return a finite set for each task state. + *) +AXIOM + \A s \in TaskState: + IsFiniteSet(SetOfTasksIn(s)) + +(** + * Sets of tasks by state. + *) +UnknownTask == SetOfTasksIn(TASK_UNKNOWN) +RegisteredTask == SetOfTasksIn(TASK_REGISTERED) +StagedTask == SetOfTasksIn(TASK_STAGED) +AssignedTask == SetOfTasksIn(TASK_ASSIGNED) +ProcessedTask == SetOfTasksIn(TASK_PROCESSED) +FinalizedTask == SetOfTasksIn(TASK_FINALIZED) + +=============================================================================== \ No newline at end of file