re-organize analysis module

This sequence of commits reorganizes the rt.restructuring.analysis module as follows.

• rt.restructuring.results — instead of having high-level results in the analysis module, there's now a new top-level module exclusively for main results.
• analysis.abstract — abstract RTA
• analysis.concepts — reserved for definitions of key analysis concepts that are well-known in the literature (e.g., busy window, priority inversion).
• analysis.definitions — all other auxiliary definitions used in the analysis (i.e., minor stuff and technicalities that we need, but that readers are unlikely to be interested in specifically).
• analysis.transform — schedule transformation definitions (this will grow over time with things like suspension-oblivious reduction, overhead accounting reductions, etc.)
• analysis.facts — where all the lemmas live
• analysis.facts.behavior — all basic facts that follow directly from the trace-based semantics
• analysis.facts.* — various lemmas and proofs (this will grow over time and eventually need more structure, but for now it's not clear what this structure should be)

Why do you use folder facts/behavior for this file? These are "model" facts

You are totally correct; facts.behavior still needs to be cleaned up. But I didn't throw this all together; this came as one bunch. I didn't yet have time to split it up and have focused on the top-level structure so far. Feel free to push patches to clean this up.

Generally speaking, I'm not happy with the facts "pile of lemmas" yet, but don't have a clear idea yet for how to best structure it.

changed the description

Also I'm not sure we want to differentiate "concepts" and "definitions".

For the presentation purpose, it’s good to have a folder containing definitions that can be found in the real-time literature. But the difference is too subtle, for example I'd say the notion of carry_in is as natural as the notion of busy_interval

Carry-in as a term is used commonly only in the context of multiprocessor analysis. It's not part of the common uniprocessor literature, at least to my knowledge.

Deciding where each definition should go is clearly a judgement call, and may require some discussion. However, I would trust us to collectively get this right (eventually).

The alternative is to have just one folder with analysis definitions. This is going to quickly become littered with small things. Obviously, something like job_cost_positive is not quite as interesting as the definition of a busy interval.

I think we should make sure that the key concepts that people are likely interested in remain uncluttered. Hence the separation based on "importance", as determined by our collective gut feeling.

Hi there, I would suggest the following structure for the analysis folder:

• lib
• abstract_rta
• edf_optimality
• ...

where lib would contain concepts/lemmas/whatever that are reused (or likely to be reused) within several analyses. Inside lib, I would rather opt for a structure like:

• transform
• busy_interval
• rbf
• ... rather than splitting between definitions and lemmas.

What do you think?

Just to clarify: the high-level EDF optimality theorem is now in results.edf; do you mean to suggest to revert splitting out the results module?

No, sorry for the confusion. What I mean is that there are files that are specific to the edf_optimality analysis, and these would be grouped into one folder.

Question: why not continue splitting definitions and lemmas? We have been careful so far to make sure the spec (definitions) is readable without encountering proofs; why should we give this up in the analysis module?

This would be the case but at the last level of hierarchy.

So something like

• analysis.lib.busy_interval.definition,
• analysis.lib.busy_interval.lemmas,
• analysis.lib.rbf.definition,
• analysis.lib.rbf.lemmas,
• analysis.lib.transform.swap.definition,
• analysis.lib.transform.swap.lemmas,

and so on?

Yup.

Hmmm... that would at least do away with the "pile of facts" we have now and give it some structure.

@sbozhko, @mlesourd what do you think about this alternative structure?

This structure works for well-known notions (like busy_interval and so on), but what to do with small technical definitions like job_cost_positive or task_service?

@sophie

@sophie, what do you think about pulling out well-known, "famous" concepts such as busy window, RBFs, etc. into a analysis.concepts (or differently named) namespace to avoid them being easily overlooked in a general lib folder?

I like the idea of having everything generic in one place but we can try different things if you want.

There is certainly some neatness to having everything in one place and following one organizational principle.

I guess a README.md that highlights and directly points to the most well-known concepts could suffice to make sure they are easy to find.

We discussed the proposal with Sophie and I am okay with it.

I think we can rely on READMEs once the hierarchy stabilizes to remove any ambiguity on what goes where.

Ok, thanks for the feedback. Can either of you help with patches to move things into place?

Sure. I'll discuss this with Maxime this afternoon.

@bbb

I'm not how to proceed in practice. Should I branch from this branch? From model-reorg? Can I directly work on this branch? Sorry for the basic question.

Either works. If you are unsure, I would suggest to create a new branch based on model-reorg and then create a merge request New-branch→model-reorg.

added 57 commits

• e8820591...ddcd2790 - 39 commits from branch model-reorg
• 1902344a - move two key analysis definitions to analysis.definitions
• 1b2e8adc - split RBF definition and facts into separate files
• e265727a - move RBF def to analysis.definitions.task, facts to analysis.facts
• fd2ad088 - move basic_facts to facts.behavior
• 9a68a406 - move facts about ideal schedule to ideal_schedule.v
• 531b6273 - def. of transformation should not depend on analysis facts
• af093128 - move facts about transforms to analysis.facts.transform
• d36562d2 - move schedule transforms to definitions.schedule.transform
• e9d0115e - move definitions.task_schedule to definitions.task.schedule
• 09130c41 - move preemption facts to facts.preemption
• d529e26b - flatten EDF high-level results folder
• 80bcda4d - flatten fixed-priority results folder
• ef8d3d85 - move main high-level results to separate top-level `results` module
• 0f15a31f - reorganize abstract RTA module
• e25cb38d - move transformations to analysis.transform
• 4201b3d1 - split analysis.definitions into core concepts and aux. defs.
• 8c663db9 - shorten long facts file names
• f888dea4 - switch back to old 'definitions' name

Compare with previous version

changed target branch from model-reorg to master

@sophie: FYI, I've rebased the branch on top of the latest master. It's ready for you to branch off.