Make resources explicit in ProcessorState

Added unfolding lemmas to basic_facts/ideal Fixed proofs depending on the previous definition using unfolding lemmas

The changes follow the discussion in Paris. @bbb @sbozhko @sophie could you have a look at the changes and tell me if everything looks ok?

This cleverly exploits type inference. That's not so obvious to someone new to this — probably worth a comment.

Applies similarly to all processor state instances.

changed this line in version 2 of the diff

Hi Maxime,

thanks a lot for preparing this MR! This looks generally good to me. We should add a few more comments; this is getting increasingly tricky.

One concern I have is about the naming of the lemmas: scheduled_inE, service_inE, and service_atE. On the one hand, I get that this naming convention matches what's in ssreflect, so that's good for experienced coders. On the other hand, this makes absolutely no sense to a RT person just getting started with this. At the very least, it will require a comment that explains the naming convention.

Personally I think it's a bit ugly. I don't mind exists_unitE, which is a very technical thing anyway and "hidden away" in rt.util, but scheduled_inE touches a rather central concept: the definition of an ideal uniprocessor schedule. That's a core definition and something that I'd like to be able to show to newbies without having to explain too much ssreflect baggage. I would prefer to pick some other convention, even if it does not match what ssreflect does (which we don't typically follow anyway).

How about scheduled_in_def, service_in_def, service_at_def, since these are conceptually replacing the abstract functions with their concrete definitions?

If that seems not quite precise enough, how about scheduled_in_elim, service_in_elim, service_at_elim, since I presume 'E' stands for "elimination"?

Rebasing on top of master proved to be a lot of pain and I wanted to try using Opaque directives for ProcessorState fields to see how it affects existing proofs.

I am currently on the process of re-implementing these changes on top of the current master with more comments.

I am ok with changing the names to something less ssreflect-flavored, *_def sounds good for the existing lemmas.

Thanks for doing this! I'm sorry for the rebasing pain... :-/

Opaque would just forcefully prevent unfolding the type-class instances?

mentioned in issue #52 (closed)

Indeed, Opaque blocks computation and unfolding. It is not irreversible in any case as we can locally force computation by specifying the right reduction parameters to simpl and unfolding would be replaced by elimination lemmas which we plan to use anyway. It is also possible to disable this annotation in a development by using Transparent commands. In addition, the definition is still available to Coq and the opaque definition is still definitionally equal to its expanded form (their equality can be proved using reflexivity).

My goal is to use it as a way to check that we do not rely on the actual definition. Once I have that in place we can discuss the usefulness of the command and removing it shouldn't change anything.

That sounds promising to me, thanks for investigating this and for the explanation.

added 7 commits

• 14b43ae0...47c0d32f - 6 commits from branch master
• 2b9022e2 - Make resources explicit in processor state

Compare with previous version

added 4 commits

• 2b9022e2...00a56667 - 2 commits from branch master
• 3f265b6d - Make resources explicit in processor state
• d342d6e9 - Merge branch 'resources_v2' of gitlab.mpi-sws.org:RT-PROOFS/rt-proofs into resources_v2

Compare with previous version

Okay this should address the basic problems. I think we would need to think some more if we want to make our developments more robust against such changes but I don't see a clear strategy for now. I have spotted a few things that we could improve while going over the impacted files and I will add these notes as issues.

I did not give a resource aware definition of service in behavior/schedule.v. Do we want to add it now?

Thanks for the update!

I did not give a resource aware definition of service in behavior/schedule.v. Do we want to add it now?

I would say no, let's add it when and if we actually need it. I don't foresee a need to reason about per-core service any time soon.

We'll need the per-core view primarily to define work conservation for multiprocessors, but let's do that once this MR has gone it.

mentioned in issue #56

Then you can merge this if everyone is ok.

Well, the CI check failed, which prevents a merge. Somehow the proof length checker was triggered?

A proof in abstract_seq_rta.v grew from 40 lines to 42.

@sbozhko Could you please have a look at this?

Terminology-wise, I guess you strongly prefer "Resource" to "Core"?

I have no strong preference on naming, Core would actually fit with ProcessorState.

Unless @sophie complains, I would prefer to name it "Core". This is not going to show up in any network calculus proofs anyway because network elements (output ports of switches, wires) are typically uniprocessors.

I don't think I will complain, but can wait until tomorrow before taking a decision?

Thanks, Sophie

I've turned my proposed name change into a MR for this branch. Please see !57 (merged).

Naive question: why do you use ideal_proc_model_ as a prefix here? Isn't this going to be clear based on which module the lemma resides in? Do you think there is ever going to be a name clash?

changed this line in version 6 of the diff

I'll look at it tomorrow, sorry for slowing down the process.

Cheers, Sophie

No worries, we can certainly wait until tomorrow.

added 2 commits

• bbefcd16 - 1 commit from branch master
• 481471a1 - Make resources explicit in processor state

Compare with previous version

added 1 commit

• 38c40d42 - tweak proof formatting

Compare with previous version

I tweaked the proof formatting so that we can get nice HTML docs on https://prosa.mpi-sws.org/branches .

• schedule definition: http://prosa.mpi-sws.org/branches/resources_v2/pretty/rt.restructuring.behavior.schedule.html

mentioned in merge request !57 (merged)

mentioned in merge request !35 (closed)

added 3 commits

• e8040e68 - rename Resource -> Core and add documentation
• 0bec2e15 - rename basic structure lemmas about ideal schedules
• f63ff2ca - documentation improvements

Compare with previous version

I've finally managed to look at this MR. This looks good to me, thanks a lot Maxime and Björn!

Regarding the naming convention: considering we use the term ProcessorState at the moment, it makes sense to use the term Core rather than Resource. I haven't found a good alternative to that so far, so let's leave it at that until it becomes problematic.

added 1 commit

• 586406c4 - update comment: Resource -> Core

Compare with previous version

I'll merge this now. This is a big step forward — thanks a lot everyone!

merged