Project Page Index Table of Contents

# Library prosa.analysis.facts.model.uniprocessor

Require Export prosa.model.processor.platform_properties.
Require Export prosa.util.tactics.
This file serves to collect basic facts about uniprocessors.
Section UniquenessOfTheScheduledJob.
Consider any type of jobs, ...
Context {Job : JobType}.
... any uniprocessor model, ...
Context {PState : ProcessorState Job}.
Hypothesis H_uni : uniprocessor_model PState.
... and any schedule.
Variable sched : schedule PState.
By definition, if one job is scheduled on a uniprocessor, then no other job is scheduled at the same time.
Lemma scheduled_job_at_neq :
∀ j j' t,
j != j' →
scheduled_at sched j t →
~~ scheduled_at sched j' t.
Proof.
move⇒ j j' t /eqP NEQ SCHED; apply/negP ⇒ SCHED'.
by have: j = j' by apply: H_uni.
Qed.
End UniquenessOfTheScheduledJob.