1. 21 Dec, 2019 1 commit
  2. 19 Dec, 2019 3 commits
  3. 15 Nov, 2019 1 commit
  4. 30 Aug, 2019 1 commit
  5. 20 Aug, 2019 1 commit
    • Sergey Bozhko's avatar
      tighten response-time recurrence for EDF · d6cdcfe1
      Sergey Bozhko authored
      When we were writing the paper on Abstract RTA, we noticed that the response-time recurrence for EDF does not match the known bound.
      This merge request tightens the analysis in Prosa to match the known bound.
  6. 24 Jul, 2019 1 commit
  7. 05 Jun, 2019 2 commits
    • Sergey Bozhko's avatar
      Change definition of completion · 0c922d98
      Sergey Bozhko authored
    • Björn Brandenburg's avatar
      port existing proofs to ssreflect 1.9.0 · 09703078
      Björn Brandenburg authored
      From the mathcomp 1.9.0 release notes:
      > removed Coq prelude hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm, to
      > improve robustness of by ...; scripts may need to invoke addn0,
      > addnS, muln0 or mulnS explicitly where these hints were used
      > accidentally.
      => This patch makes these required fixes in Prosa.
      While at it, turn on CI for coq:dev and Coq 8.9 with two versions of ssreflect.
  8. 26 May, 2019 1 commit
  9. 19 May, 2019 1 commit
  10. 13 May, 2019 6 commits
  11. 12 May, 2019 1 commit
  12. 05 Apr, 2019 10 commits
  13. 19 Sep, 2018 1 commit
  14. 17 Jul, 2018 1 commit
    • Felipe Cerqueira's avatar
      Formalization of Weakly Sustainable Policy · 258edf49
      Felipe Cerqueira authored
      1) Formalize the notion of weakly sustainable policy, along with
      its contrapositive, and prove the equivalence between the two.
      2) Establish weak sustainability of self-suspending tasks w.r.t.
      execution times and variable suspension times, based on the
      transformation we had formalized.
  15. 05 Jan, 2018 1 commit
  16. 14 Dec, 2017 2 commits
  17. 07 Dec, 2017 2 commits
    • Felipe Cerqueira's avatar
      Major Commit: Suspension-aware Scheduling · 3f39fe20
      Felipe Cerqueira authored
      1) Definition of a generic model for job suspensions based on
         received service (e.g., job j_1 should suspend for 4ms as
         soon as service reaches 5ms).
      2) Definition of the dynamic suspension model (i.e., cumulative
         suspension of job j_1 <= X).
      3) Analysis of suspension-aware scheduling by inflation of job
         costs (via schedule reduction). In the literature, this is
         called suspension-oblivious analysis.
      4) Analysis of suspension-aware scheduling by adjusting job
         jitter (via schedule reduction).
      5) Proof of (weak) sustainability of job costs under suspension-aware
         scheduling. We show that if we increase the costs of all jobs while
         reducing their suspension times in a certain way, the response times
         of all jobs do not decrease.
         This has an important implication regarding worst-case schedules: if
         some schedulability analysis already accounts for the fact that job
         suspension times can vary from 0 to the task suspension bound, then
         it's perfectly safe to assume that jobs execute for their WCET.
      6) Proof of sustainability of the cost of a single job under
         suspension-aware scheduling. That is, we show that increasing the
         cost of a single job does not reduce its own response time.
         (Note that this is a very basic result that applies to many
         work-conserving, JLFP schedulers. We don't claim anything about
         the response time of other jobs.)
    • Felipe Cerqueira's avatar
      Make Prosa compatible with Coq 8.7.0 and Mathcomp 1.6.4 · b6c93d38
      Felipe Cerqueira authored
      - Remove Require declarations from Modules.
      - Small fixes due to changes in the type checker.
      - Generate _CoqProject with Makefile and remove spurious warnings from ssreflect.
  18. 10 Jan, 2017 1 commit
  19. 25 Nov, 2016 3 commits