Dear TLA+ community,
I have written an OS model that schedules tasks, but I am not sure that I wrote its properties correctly.
I can see that it behaves correctly (p2 preemts p1, and p1 is only terminated when p2 is not ready)
<os.png>But I need to verify in code that "ready" higher priority task will preempt currently "running" lower priority task.
Could you please tell me if it's the right way to do it? This is the temporal property I came up with:
ReadyHigherPriorityTaskPreemptsRunningLowerPriorityTask ==
runningTask # "" =>
\A t \in TaskPool :
tasks[t].state = "running" /\ \E u \in TaskPool :
tasks[u].state = "ready" /\ tasks[u].priority > tasks[t].priority
~> (IsLastElement(readyQueue, t) /\ runningTask = u)Full spec of my OS:
Tasks free up the processor in two cases:
- The task has completed.
- There was a switch to a higher priority task.
States:
- running: The task is running (only one task can be running at a time).
- ready: The task is ready for execution and is awaiting selection by the scheduler.
- suspended: The task is suspended and can be activated.
Transitions between states:
activate: from suspended to ready (activation of a new task).
start: from ready to running (the scheduler starts the task).
preempt: from running to ready (the scheduler switches the task).
terminate: from running to suspended.
Model requirements
- Priority: A high priority task should not wait for the completion of a low priority one.
- Task selection: if the priority of tasks is the same, the task that came first is assigned.- Uniqueness of execution: only one task can be in the running state at any given time.
- Queue limit: no more than N tasks can be in the ready state.
Thanks for your help.
Best,
Dmitriy
p.s. I also have no idea how to check the Task selection requirement. I would be very grateful if you could tell me this point too.
Full code:
OS.cfg
\* CONSTANTS "t1", "t2", "t3", "t4", "t5", "t6", "t7"
CONSTANTS
N = 3
TaskPool = { "t1", "t2", "t3", "t4"}
MaxPriority = 3
\* SPECIFICATION
SPECIFICATION Spec
\* INVARIANTS
INVARIANT TypeInvariant
INVARIANT NoDuplicateInReadyQueue
\* PROPERTIES TO CHECK
PROPERTY RunningTaskCorrect
PROPERTY ReadyTasksInQueue
PROPERTY SingleRunningTask
PROPERTY PriorityInvariant
PROPERTY ReadyQueueLimit
PROPERTY ReadyHigherPriorityTaskPreemptsRunningLowerPriorityTask
OS.tla
---------------------------- MODULE OS ----------------------------
EXTENDS Integers, Sequences, FiniteSets
CONSTANT N, TaskPool, MaxPriority
ASSUME N \in Nat \ {0} /\ MaxPriority \in Nat \ {0}
ASSUME IsFiniteSet(TaskPool) /\ TaskPool # {}
(* Task states *)
VARIABLES tasks, readyQueue, runningTask
vars == <<tasks, readyQueue, runningTask>>
TaskState == {"running", "ready", "suspended"}
InitialState ==
/\ runningTask = ""
/\ readyQueue = <<>>
/\ tasks = [t \in TaskPool |-> [state |-> "suspended",
priority |-> CASE t = "t1" -> 1
[] t = "t2" -> 2
[] t = "t3" -> 3
[] t = "t4" -> 0
[] t = "t5" -> 1
[] t = "t6" -> 2
[] t = "t7" -> 3]]
SeqContains(seq, elem) == \E i \in 1..Len(seq) : seq[i] = elem
IsLastElement(seq, elem) ==
IF Len(seq) = 0
THEN FALSE
ELSE seq[Len(seq)] = elem
(* Properties *)
RunningTaskCorrect == \A t \in TaskPool : (tasks[t].state = "running") => (runningTask = t)
ReadyTasksInQueue == \A t \in TaskPool : (tasks[t].state = "ready") => SeqContains(readyQueue, t)
SingleRunningTask == \A t \in TaskPool : tasks[t].state = "running" => \A u \in TaskPool \ {t} : tasks[u].state # "running"
PriorityInvariant == \A t \in TaskPool : (tasks[t].state = "ready" /\ runningTask # "") => (tasks[t].priority <= tasks[runningTask].priority)
ReadyQueueLimit == Len(readyQueue) <= N
ReadyHigherPriorityTaskPreemptsRunningLowerPriorityTask ==
runningTask # "" =>
\A t \in TaskPool :
tasks[t].state = "running" /\ \E u \in TaskPool :
tasks[u].state = "ready" /\ tasks[u].priority > tasks[t].priority
~> (IsLastElement(readyQueue, t) /\ runningTask = u)
(* Invariants *)
TypeInvariant ==
/\ tasks \in [TaskPool -> [state : TaskState, priority : 0..MaxPriority]]
/\ readyQueue \in Seq(TaskPool)
/\ runningTask \in TaskPool \union {""}
/\ (runningTask # "" => tasks[runningTask].state = "running")
/\ \A t \in TaskPool:
/\ tasks[t].state \in TaskState
/\ (tasks[t].state = "running" => runningTask = t)
/\ (tasks[t].state = "ready" => SeqContains(readyQueue, t))
/\ (tasks[t].state \in {"running", "suspended"} => ~SeqContains(readyQueue, t))
NoDuplicateInReadyQueue == \A i,j \in 1..Len(readyQueue) : i # j => readyQueue[i] # readyQueue[j]
CanActivate(t) ==
/\ tasks[t].state = "suspended"
/\ Len(readyQueue) < N
Activate(t) ==
/\ CanActivate(t)
/\ tasks' = [tasks EXCEPT ![t].state = "ready"]
/\ readyQueue' = Append(readyQueue, t)
/\ runningTask' = runningTask
/\ UNCHANGED <<>>
(* Returns the highest priority task that's been in readyQueue longest *)
SelectTaskToRun ==
LET readyTasks == {t \in TaskPool : tasks[t].state = "ready"}
maxPriority == CHOOSE p \in {tasks[t].priority : t \in readyTasks} :
\A t \in readyTasks : tasks[t].priority <= p
candidates == {t \in readyTasks : tasks[t].priority = maxPriority}
IN CHOOSE t \in candidates :
\A u \in candidates :
LET t_pos == CHOOSE i \in 1..Len(readyQueue) : readyQueue[i] = t
u_pos == CHOOSE i \in 1..Len(readyQueue) : readyQueue[i] = u
IN t_pos <= u_pos
CanStart(t) ==
/\ tasks[t].state = "ready"
/\ runningTask = ""
/\ t = SelectTaskToRun
Start(t) ==
/\ CanStart(t)
/\ tasks' = [tasks EXCEPT ![t].state = "running"]
/\ readyQueue' = SelectSeq(readyQueue, LAMBDA u: u # t)
/\ runningTask' = t
/\ UNCHANGED <<>>
CanPreempt(t) ==
/\ tasks[t].state = "ready"
/\ runningTask # ""
/\ t = SelectTaskToRun
/\ tasks[t].priority > tasks[runningTask].priority
Preempt(t) ==
/\ CanPreempt(t)
/\ tasks' = [tasks EXCEPT ![runningTask].state = "ready", ![t].state = "running"]
/\ readyQueue' = Append(SelectSeq(readyQueue, LAMBDA u: u # t), runningTask)
/\ runningTask' = t
/\ UNCHANGED <<>>
CanTerminate(t) ==
/\ tasks[t].state = "running"
/\ ~(\E u \in TaskPool : tasks[u].state = "ready" /\ tasks[u].priority > tasks[t].priority)
Terminate(t) ==
/\ CanTerminate(t)
/\ tasks' = [tasks EXCEPT ![t].state = "suspended"]
/\ readyQueue' = readyQueue
/\ runningTask' = ""
/\ UNCHANGED <<>>
Next ==
\/ \E t \in TaskPool : Preempt(t)
\/ \E t \in TaskPool : Start(t)
\/ \E t \in TaskPool : Activate(t)
\/ \E t \in TaskPool : Terminate(t)
Spec ==
/\ InitialState
/\ [][Next]_vars
=============================================================================
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
.