• 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).
Makefile 16.2 KB