Skip to content

feat: add SimpleTaskScheduling specification #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
qdelamea-aneo merged 1 commit into from
Oct 17, 2025
Merged

feat: add SimpleTaskScheduling specification #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 60 additions & 0 deletions .docs/modeling.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
# ArmoniK Modeling Using TLA+

## Introduction

**ArmoniK** is a production-grade system with a complex codebase, components, and configurations. The purpose of this TLA+ specification is to formally describe the existing system, ensuring correctness and clarity. Since ArmoniK was developed without prior formal specification, many aspects require clarification and justification.

This document discusses and documents the assumptions and modeling choices made to formalize ArmoniK’s design and algorithms. It details the model design based on the actual implementation, specifying and justifying omissions and simplifications.

> **ℹ️ NOTE**
> The state-of-the-art modeling approach in TLA+ is iterative refinement. We start with an abstract description of ArmoniK’s operation and progressively refine it.

---

## Table of Contents

* [An Abstract Decentralized Online Scheduling System](#an-abstract-decentralized-online-scheduling-system)

---

## An Abstract Decentralized Online Scheduling System

At a high level, ArmoniK can be seen as a **decentralized online task scheduler**. It consists of a set of **Scheduling Agents** (whose number is unknown and may vary over time) responsible for executing tasks submitted to the system.

System constraints:
- **Task Submission**: New tasks can be submitted at any time. Each task must be unique and cannot be submitted more than once.
- **Task Acquisition**: An agent can acquire a set of available tasks (uncompleted and not being processed by any other agent) for execution.
- **Task Release**: An agent can release all or part of the tasks it is processing, making them available again.
- **Task Completion**: An agent can complete all or part of the tasks it is processing, notifying the system to avoid future re-executions.

System properties:
- **Exclusivity**: A task cannot be executed simultaneously by two distinct agents.
- **Completion**: Every submitted task must eventually be completed.
- **Persistence**: Once completed, a task remains completed forever.

> **ℹ️ REMARK**
> A *task* abstracts a request to perform a computation, i.e., executing a set of instructions.

**A status is associated with each task to track its position in the scheduling process.** Based on the previous informal description, it is possible to scheme the life-cycle of a task as shown in the following figure.

```mermaid
stateDiagram-v2
direction LR
[*] --> Submitted : Submit
Submitted --> Started : Schedule
Started --> Completed : Release
Started --> Submitted : Complete
classDef completed fill:#006400
class Completed completed
```

**In this diagram, each state corresponds to a given status for a task, and the transitions describe the system as a transition system.** This transition system, associated with the desired properties, is specified in [SimpleTaskScheduling](../specs/SimpleTaskScheduling.tla).

> **ℹ️ NOTE**
> The set of tasks and agents is represented by unique identifiers from an implicit, potentially infinite set. For model checking, these sets are materialized and made finite. A dedicated specification, [MCSimpleTaskScheduling](../specs/MCSimpleTaskScheduling.tla), introduces a dummy terminating action to avoid deadlocks.

---

Here’s the corrected and expanded section for **Considering Task Inputs/Outputs**, restoring the two-step refinement and clarifying the role of task I/Os:

---
28 changes: 28 additions & 0 deletions specs/MCSimpleTaskScheduling.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
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
45 changes: 45 additions & 0 deletions specs/MCSimpleTaskScheduling.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
------------------------ 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

ASSUME IsFiniteSet(TaskId)
ASSUME IsFiniteSet(AgentId)

--------------------------------------------------------------------------------

(**
* Dummy action representing the terminal state of the system, reached once all
* tasks have been completed.
*)
Terminating ==
/\ IsCompleted(TaskId)
/\ UNCHANGED vars

(**
* Modified next-state action. Extends the original system behavior with the
* Terminating action to avoid artificial deadlocks due to the bounded task set.
*)
MCNext ==
\/ Next
\/ Terminating

(**
* Modified full system specification.
*)
MCSpec ==
/\ Init
/\ [][MCNext]_vars
/\ Fairness

================================================================================
191 changes: 191 additions & 0 deletions specs/SimpleTaskScheduling.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,191 @@
------------------------- 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

================================================================================