This is a purely accidental dependency; purge it.

All "kinds of schedules" and associated validity conditions are being
collected in model.schedule.

The Prosa notion of priority-driven scheduling depends on the
preemption model. That is ok; any theory that doesn't want to deal
with non-preemptive sections can simply Require Export the fully
preemptive model and be done with it.

This fixes all warnings about ambiguous module names and resolves #49.

It also highlights that we still need to cut down on superfluous
Require Import commands in recently ported files.

Rationale: reserve the behavior folder for trace-based semantics.

These lemmas really constitute an analysis of the basic consequences
arising from the chosen semantics and hence logically belong to the
"analysis" part of Prosa.

Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago

Also removes an unnecessary module in rt.util.epsilon.

Add a [job_ready] parameter to the job model, akin to [pending], that
defines whether a job can be scheduled at a given time in a given schedule.

Then use this new general notion of readiness to define [backlogged].

A pending job may not be ready, whereas (under any reasonable
definition) a ready job ought to be pending, so this definition is
more precise and captures effects such as jitter and self-suspensions.

This patch adds the classic EDF optimality argument: by swapping
allocations, any schedule in which no job misses a deadline can be
transformed into an EDF schedule in which also no job misses a deadline.

Maxime Lesourd authored 5 years ago and Björn Brandenburg committed 5 years ago

Add model definitions for work-conserving and priority-based preemptive schedules.

simplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to model