Skip to content

re-organize analysis module

Björn Brandenburg requested to merge analysis-reorg into master

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)
Edited by Björn Brandenburg

Merge request reports