Draft : Explicit policy in [respects_policy_at_preemption_point]

Currently, the policy under consideration is implicitly passed to respects_policy_at_preemption_point. This is unhelpful from a readability POV. The goal of this MR is to change the definition of respects_policy_at_preemption_point such that the policy has to be explicitly passed to it.

Currently there are two issues with this new definition.

1. In the case of FP, the hypothesis looks as follows :

Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched (FP_to_JLFP Job Task ).

This shows that the coercion from fp to jldp is not working.

2. Secondly, on compiling the file model/schedule/priority/classes.v, the following warning is generated :

Warning: FP_to_JLFP does not respect the uniform inheritance condition
[uniform-inheritance,typechecker]

My guess is that this warning is issued because Task is a parameter of FP but not of JLFP and this does not comply with the rules stated here : https://coq.inria.fr/refman/addendum/implicit-coercions.html#id1 However, I am not sure this is the reason since I do not understand the rules for defining a coercion fully.

To address the issue 1, I tried to add the following coercion :

Instance FP_to_JLDP (Job: JobType) (Task: TaskType)
         `{JobTask Job Task} `{FP_policy Task} : JLDP_policy Job :=
  fun _ j1 j2 => hep_task (job_task j1) (job_task j2).
Coercion FP_to_JLDP : FP_policy >-> JLDP_policy.

This generates this warning :

Warning:
New coercion path [FP_to_JLDP] : FP_policy >-> JLDP_policy is ambiguous with existing 
[FP_to_JLFP; JLFP_to_JLDP] : FP_policy >-> JLDP_policy.
[ambiguous-paths,typechecker]

I thought this was important to mention since it shows that Coq knows there is a conversion from FP to JLDP.

My guess is that this warning is issued because Task is a parameter of FP but not of JLFP and this does not comply with the rules stated here : https://coq.inria.fr/refman/addendum/implicit-coercions.html#id1 However, I am not sure this is the reason since I do not understand the rules for defining a coercion fully.

Your diagnosis is right. Indeed, in order to apply FP_to_JLFP as a coercion, Coq need to infer a Job : JobType, a Task : TaskType and a JobTask Job Task (according to About FP_to_JLFP) and the Coercion mechanism needs those to be exactly the arguments of the source class FP_policy (that's the uniform inheritance condition). This is not the case, so FP_to_JLFP cannot be used as a coercion.

AFAIK, there is no other solution than to explicitly use FP_to_JLFP. To make this more convenient, you can change the implicit status of the arguments in the definition, changing

Instance FP_to_JLFP (Job: JobType) (Task: TaskType)
         `{JobTask Job Task} `{FP_policy Task} : JLFP_policy Job :=

to

Instance FP_to_JLFP {Job: JobType} {Task: TaskType}
         `{JobTask Job Task} (_ : FP_policy Task) : JLFP_policy Job :=

(you may also have to change a few FP_to_JLFP Job Task to FP_to_JLFP _ here and there)

You can also define a notation to write policy%:JLFP instead of FP_to_JLFP policy, as follows

Reserved Notation "p %:JLFP" (at level 2, left associativity, format "p %:JLFP").
Notation "p %:JLFP" := (FP_to_JLFP p).

but not sure it helps much.

Thanks Pierre! In light of this clarification, I guess it makes sense to define type-specific validity conditions as suggested by Bjorn here. I will update this branch with this change soon.

Well, in fact, thank you for pointing that quirk of Coq. This prompted an interesting discussion on Zulip: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Identity.20Coercions and a pull request that may solve this long standing issue (we found bug reports from 2012) in next Coq release: https://github.com/coq/coq/pull/15789

Anyway, meanwhile Björn's suggestion is probably the best solution.

That's awesome Pierre, thanks for getting this fixed upstream!

mentioned in merge request !201 (merged)

I created a new MR with three different definitions of priority policy compliance !201 (merged)

mentioned in commit 98e1a897

closed