1. 10 Jan, 2017 5 commits
  2. 25 Nov, 2016 7 commits
  3. 26 Oct, 2016 2 commits
  4. 19 Oct, 2016 1 commit
  5. 18 Oct, 2016 6 commits
  6. 06 Oct, 2016 3 commits
  7. 06 Sep, 2016 5 commits
    • Felipe Cerqueira's avatar
      Major commit: Uniprocessor RTA · ac6f0d4e
      Felipe Cerqueira authored
      This commit contains several updates related to uniprocessor scheduling.
      
      - Basic definitions of uniprocessor scheduling (see model/uni)
      - Definitions of worload and service for generic sets of jobs (see service.v and workload.v in model/uni)
      - Definitions and lemmas about busy intervals (see model/uni/basic/busy_interval.v)
      - Definition of an arrival bound for sporadic tasks (see model/arrival_bounds.v)
      - Definitions and correctness proofs of the RTA for FP scheduling
        (also works with non-unique priorities and arbitrary deadlines, but gives pessimistic bounds)
      - Implementation of the FP RTA to check for contradictory assumptions
      
      In addition, we have also defined partitioned scheduling and proven how it relates
      with uniprocessor (see model/partitioned).
      ac6f0d4e
    • Felipe Cerqueira's avatar
      Add lemmas about iter_fixpoint · 5d02df7f
      Felipe Cerqueira authored
      5d02df7f
    • Felipe Cerqueira's avatar
      Add more lemmas about \max · d3d75a3b
      Felipe Cerqueira authored
      d3d75a3b
    • Felipe Cerqueira's avatar
      Add new lemmas for counting and sorting · 6461aa51
      Felipe Cerqueira authored
      6461aa51
    • Felipe Cerqueira's avatar
      Add more notation for map/filter · 74126db1
      Felipe Cerqueira authored
      74126db1
  8. 05 Aug, 2016 2 commits
  9. 03 Aug, 2016 1 commit
  10. 17 Jul, 2016 1 commit
  11. 15 Jul, 2016 1 commit
  12. 14 Jul, 2016 1 commit
  13. 13 Jul, 2016 1 commit
  14. 12 Jul, 2016 1 commit
  15. 08 Jun, 2016 3 commits