Skip to content

Modifications to ideal uniprocessor schedule

Ghost User requested to merge sbozhko/rt-proofs:scheduler_validity into master
  • We modified prev_job_nonpreemptive, as currently does respect jobs_must_be_ready_to_execute
  • We do not prove schedule_respects_preemption_model anymore.
  • We slightly changed valid_nonpreemptive_readiness so that sched is a parameter. This way, the proposition can be assumed to hold only for a certain schedule (making weaker assumptions).
  • We proved more facts for the preemption-aware scheduler
Edited by Ghost User

Merge request reports