• 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
Name
Last commit
Last update
analysis Loading commit data...
doc Loading commit data...
implementation Loading commit data...
model Loading commit data...
util Loading commit data...
.gitignore Loading commit data...
Makefile Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
create_makefile.sh Loading commit data...