1. 01 Jul, 2022 6 commits
  2. 30 Jun, 2022 5 commits
  3. 27 May, 2022 2 commits
  4. 26 May, 2022 1 commit
  5. 16 May, 2022 1 commit
    • Kimaya Bedarkar's avatar
      add lemma relating task cost and task rbf · 84b04ff3
      Kimaya Bedarkar authored and Björn Brandenburg's avatar Björn Brandenburg committed
      Currently, we have lemmas stating that `task_rbf` at `\vareosilon` is greater than equal to task cost, and `task_rbf` is monotone. I combined these two lemmas to state that `tsk_rbf` at any point greater than `0` is greater than task cost. I find that this fact is regularly required in proofs and, therefore, would be good to have in the facts folder.
      84b04ff3
  6. 12 May, 2022 1 commit
  7. 09 May, 2022 1 commit
    • Marco Maida's avatar
      introduce "greedy" concrete arrival sequence · e122dbb1
      Marco Maida authored and Björn Brandenburg's avatar Björn Brandenburg committed
      This commit defines and adds facts about a concrete arrival sequence in
      which tasks release jobs "as quickly as possible" as allowed by their
      respective arrival-curve constraints. This maximal arrival sequence is
      used in POET to generate assumption-less certificates.
      e122dbb1
  8. 06 May, 2022 1 commit
    • Kimaya Bedarkar's avatar
      modify definitions of priority policy compliance · 41a542a8
      Kimaya Bedarkar authored and Björn Brandenburg's avatar Björn Brandenburg committed
      The current definitions of `respects_JLFP_policy_at_preemption_time`
      and `respects_FP_policy_at_preemption_time` use the predicate
      `hep_job_at`. This predicate does not make sense for `JLFP`
      and `FP` policies. To avoid this, these definitions should
      instead use the definition `respects_JLDP_policy_at_preemption_point`.
      Doing this requires coercions from `JLFP` to `JLDP` and from
      `FP` to `JLFP`. This patch also introduces these coercions.
      41a542a8
  9. 05 May, 2022 1 commit
  10. 19 Apr, 2022 19 commits
  11. 14 Apr, 2022 2 commits