WIP: Partitioned

This is a draft of the concepts needed to work on partitioned schedules. It is driven by the ongoing work in Grenoble on generic CPA but we want aim to formalize partitioned scheduling in a manner that makes sense on its own and can be reused, as such we would like to get some feedback before we integrate it into the CPA analysis.

The intuition is that we rely on the Cores defined in ProcessorState to project per-core arrival sequences and schedules on which scheduling models can be applied.

The main design choice is to provide the definitions for any ProcessorState. An alternative would have been to only consider multiprocessor schedules in the sense of model/processor/multiprocessor.v for which the construction can be made nicer but is not as generic. It seems to me that since we have a notion of core in the definition of ProcessorState we might as well rely on it to provide a generic construction as long as it is readable.

The roadmap before we can integrate this is as follows:

• Fixing the omission of service on a core in behavior/schedule.v
• Definition of the projections
• Per-core specification of a model
• Specific definitions related to job and task partitioned schedules (no migration)
• Examples to show how to define a simple model using the provided utilities
• Basic theory of partitioned schedules (this will probably come with the developments related to CPA)

The current state implied some changes to the behavior/schedule.v files, I have fixed the related proofs so that it compiles but I still have some work to make the CI happy on all supported pairs of coq/ssreflect versions we cover.

The rest of the relevant changes are collected in model/schedule/partitioned.v

I will be away until July 27th, so this will be stable for a week after which I will continue as this is on the critical path for the CPA proof.