 06 Sep, 2016 1 commit


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 nonunique 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).

 05 Aug, 2016 1 commit


Felipe Cerqueira authored

 08 Jun, 2016 1 commit


Felipe Cerqueira authored

 06 Jun, 2016 1 commit


Felipe Cerqueira authored
 Add definitions related to APA scheduling  Prove correctness of reductionbased RTA for APA scheduling (FP and EDF)  Add implementation of a weak APA scheduler  Update definition of taskset to assume uniqueness  Modify names and comments to improve readability  Remove strong assumptions about priority order in FP scheduling  Add tests with FP RTA for every model  Add tests for RTA with parallel jobs

 05 May, 2016 2 commits


Felipe Cerqueira authored

Felipe Cerqueira authored

 04 May, 2016 1 commit


Felipe Cerqueira authored

 31 Mar, 2016 2 commits


Felipe Cerqueira authored

Felipe Cerqueira authored

 01 Mar, 2016 1 commit


Felipe Cerqueira authored

 23 Feb, 2016 2 commits


Felipe Cerqueira authored

Felipe Cerqueira authored
We use simpler, more pessimistic interference bounds to prove that Bertogna and Cirinei's RTA works for parallel jobs.

 16 Feb, 2016 1 commit


Felipe Cerqueira authored

 14 Feb, 2016 1 commit


Felipe Cerqueira authored

 12 Feb, 2016 1 commit


Felipe Cerqueira authored

 06 Feb, 2016 1 commit


Felipe Cerqueira authored

 01 Feb, 2016 1 commit


Felipe Cerqueira authored
 Removed unnecessary assumption in RTA about task precedence/no intratask parallelism.  Scheduler models and analyses are organized in separate modules/folders.  Added RTA for FP and EDF for schedulers with release jitter.  The scheduling invariants were split into more finegrained assumptions: (a) scheduler is workconserving (b) scheduler enforces FP/JLDP priority X  New helper lemmas about counting, and sorted/uniq lists  Inclusion of tactics feed and feed_n (see documentation).  Added a Makefile generator
