Library prosa.model.processor.platform_properties

To reason about classes of schedule types / processor models, we define the following properties that group processor models into classes of similar models.

Consider any job type and any processor state. Note: we make the processor state an explicit variable (rather than implicit context) because it is the primary subject of the following definitions.

We say that a processor model provides unit service if no job ever receives more than one unit of service at any time.

We say that a processor model offers ideal progress if a scheduled job always receives non-zero service.

In a uniprocessor model, the scheduled job is always unique.