• Felipe Cerqueira's avatar
    Major Changes in RTA and Directory Structure · 32126a75
    Felipe Cerqueira authored
    - Removed unnecessary assumption in RTA about task precedence/no intra-task parallelism.
    - Scheduler models and analyses are organized in separate modules/folders.
    - Added RTA for FP and EDF for schedulers with release jitter.
    - The scheduling invariants were split into more fine-grained assumptions:
      (a) scheduler is work-conserving
      (b) scheduler enforces FP/JLDP priority X
    - New helper lemmas about counting, and sorted/uniq lists
    - Inclusion of tactics feed and feed_n (see documentation).
    - Added a Makefile generator
bertogna_fp_comp.v 30.1 KB