Draft : Explicit policy in [respects_policy_at_preemption_point]

Currently there are two issues with this new definition.

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.

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

Draft : Explicit policy in [respects_policy_at_preemption_point]

Merge request reports

Activity