Explicit policy in [respects_policy_at_preemption_point]

As Björn noted, from a readability PoV, it's quite unfortunate that the policy that is being respected doesn't show up in the code. The subject of definitions should show up as an explicit argument, even if it is implicit everywhere else.

Currently we have:

  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.

However, ideally, we need:

  Hypothesis H_respects_policy : respects_policy_at_preemption_point FP arr_seq sched.
                                                                     ^^ --- new, explicit, argument here

changed the description

The current definition of respects_policy_at_preemption_point is stated for all JLDP policies. If the policy were to be added as an explicit parameter (instead of being implicitly passed as is currently done) then, a JLDP policy would have to be explicitly passed to respects_policy_at_preemption_time. This complicates instantiating respects_policy_at_preemption_time for JLFP policies since JLFP policies can not be passed as JLDP policies. Is there any workaround for this?

P.S. : In order to pass the policy as a parameter, we have to remove the JLDP policy from context of the definition and add it as a variable instead.

JLFP policies can not be passed as JLDP policies

Oh, really? I thought we have coercions for this in place? Don't they work in this case?

Oh so I checked and yes there is an automatic conversion from JLFP to JLDP defined here. However since the scheduling policy is implicitly passed to JLFP_toJLDP as well, this does not solve our problem. So now, we have this : respects_policy_at_preemption_point arr_seq sched (JLFP_to_JLDP Job). So I guess we need to either use JLFP_to_JLDP with a @ prefix or redefine it to make the scheduling policy explicit in JLFP_to_JLDP as well. But, I guess the latter would break a lot of automatic conversions that are currently happening in other files.

Note that coercions are not the same as typeclasses resolutions

So what's a good solution?

I would say we make policy an explicit parameter in JLFP_to_JLDP. This will not break too much things.

Sorry, I don't fully understand the problem yet. Could you please explain why a coercion cannot be used here? In C terms, all that we want is a cast from one type to another, and we'd like to have this happen automatically. Is there no way to express this in Gallina?

If there's no other way, what about defining type-specific validity conditions?

• respects_fp_policy_at_preemption_point arr_seq sched
• respects_jlfp_policy_at_preemption_point arr_seq sched
• respects_jldp_policy_at_preemption_point arr_seq sched

A coercion could be used. I don't know how we would define and use this but I can look into this.

Okay, suppose I do something like this

1. Change this definition to the following:

  Definition respects_policy_at_preemption_point (_: JLDP_policy Job) :=
    forall j j_hp t,
      arrives_in arr_seq j ->
      preemption_time sched t ->
      backlogged sched j t ->
      scheduled_at sched j_hp t ->
      hep_job_at t j_hp j.

2. Here add the following:

Coercion JLFP_to_JLDP : JLFP_policy >-> JLDP_policy.
Coercion FP_to_JLFP : FP_policy >-> JLFP_policy.

Then, the conversion seems to be working (at least one example I tried), e.g.:

  (** We first show that a schedule that satisfies the standalone
      [EDF_schedule] predicate is also compliant with the generic notion of EDF
      policy defined in Prosa, namely the [respects_policy_at_preemption_point]
      predicate. *)
  Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
    EDF_schedule sched ->
    respects_policy_at_preemption_point arr_seq sched (EDF Job).

Nice!

Is there a way to explicitly connect the parameter of respects_policy_at_preemption_point to hep_job_at? Ideally, the reader should see where the given priority policy is "used".

FYI : Please check the current status of the code here

Please open a draft MR; that’s a lot easier to work with. Thanks!

mentioned in merge request !188 (closed)

closed with commit 98e1a897

mentioned in commit 98e1a897