Library prosa.model.processor.restricted_supply

Require Export prosa.behavior.all.

The Restricted Supply Model

In the following, we define a processor state that includes the possibility of the processor becoming unavailable, where the jobs executing in the unavailable state do not progress (= don't get any service). We allow jobs to be scheduled in unavailable states in order to preserve work-conservation.
Section State.

We define the state of a processor at a given time to be one of four possible cases:
  Inductive processor_state {Job : JobType} :=
  
The processor is idle. We could service a job, so we are wasting the capacity of the supply.
  | Idle
  
A job is being executed.
  | Active (j : Job)
  
A job is scheduled, but the processor is unavailable and yields no service.
  | Unavailable (j : Job)
  
The processor is unavailable, and no job is being scheduled.
  | Inactive.

Consider any type of jobs.
  Context (Job : JobType).

Next, we define the semantics of the processor state with restricted supply.
  Section Service.

Let j denote any job.
    Variable j : Job.

It is scheduled in a given state s iff j is the job mentioned in the state.
    Definition rs_scheduled_on (s : processor_state) : bool :=
      match s with
      | Idle | Inactivefalse
      | Active j' | Unavailable j'j' == j
      end.

Processor states Idle and Active _ indicate that the processor is ready to produce 1 unit of supply. If the processor is in state Unavailable _ or Inactive, it produces 0 unit of work.
    Definition rs_supply_on (s : @processor_state Job) : work :=
      match s with
      | Idle | Active _ ⇒ 1
      | _ ⇒ 0
      end.

Job j receives service only if the given state s is Active j.
    Definition rs_service_on (s : processor_state) : work :=
      if s is Active j'
      then if j' == j then 1 else 0
      else 0.

  End Service.

Finally, we connect the above definitions with the generic Prosa interface for abstract processor states.
  Program Definition rs_processor_state : ProcessorState Job :=
    {|
      State := processor_state;
      scheduled_on j s (_ : unit) := rs_scheduled_on j s;
      supply_on s (_ : unit) := rs_supply_on s;
      service_on j s (_ : unit) := rs_service_on j s
    |}.
  Next Obligation. by movej s r; case s, r ⇒ //=; case: (_ == _). Qed.
  Next Obligation. by movej s r; case s, r ⇒ //=; case: (_ == _). Qed.

End State.