- Feb 17, 2022
-
-
- Feb 16, 2022
-
-
From changelog of Coq version 8.15: Changed: [apply with] does not rename arguments unless using compatibility flag Apply With Renaming (#13837, fixes #13759, by Gaëtan Gilbert). So, this commit replaces all occurrences of [apply L with (NAME0 := V)] to [apply L with (NAME := V)]
-
- Sep 08, 2021
-
-
Note that many files have changed; however, this is due to the fact that some of the lemmas in nat.v have been renamed or removed.
-
- Dec 19, 2019
-
-
Björn Brandenburg authored
Move everything into the new namespace starting with 'prosa' rather than the bland 'rt'.
-
- Nov 15, 2019
-
-
Björn Brandenburg authored
-
Björn Brandenburg authored
-
Björn Brandenburg authored
-
- Jun 05, 2019
-
-
Sergey Bozhko authored
-
- Jan 10, 2017
-
-
Felipe Cerqueira authored
-
- Nov 25, 2016
-
-
Felipe Cerqueira authored
- Added definitions and implementation of jitter-aware RTA for uniprocessor scheduling. - The Prosa directory was restructured to better accomodate the different types of arrival sequences and schedules.
-
- Oct 18, 2016
-
-
Felipe Cerqueira authored
- Add generic definition of job suspension based on the cumulative service - Define the dynamic suspension model (based on task suspension bounds) - Add suspension semantics for uniprocessor schedules - Formalize reduction from suspension-aware schedule to suspension-oblivious schedule by inflating costs (works with JLDP policies and non-unique priorities) - Formalize suspension-oblivious FP RTA using the reduction - Add implementation of a concrete suspension-aware scheduler - Test suspension-oblivious FP RTA with an actual task set - Add simpler definition for JLFP policies - Generalize busy interval lemmas from FP to JLFP scheduling
-
- Sep 06, 2016
-
-
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).
-
- Aug 05, 2016
-
-
Felipe Cerqueira authored
-
- Jun 06, 2016
-
-
Felipe Cerqueira authored
- Add definitions related to APA scheduling - Prove correctness of reduction-based 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
-
- May 05, 2016
-
-
Felipe Cerqueira authored
-
Felipe Cerqueira authored
-
- May 04, 2016
-
-
Felipe Cerqueira authored
-
- Mar 31, 2016
-
-
Felipe Cerqueira authored
-
- Mar 01, 2016
-
-
Felipe Cerqueira authored
-
- Feb 23, 2016
-
-
Felipe Cerqueira authored
-
- Feb 16, 2016
-
-
Felipe Cerqueira authored
-
- Feb 01, 2016
-
-
Felipe Cerqueira authored
- Removed unnecessary assumption in RTA about task precedence/no intra-task 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 fine-grained assumptions: (a) scheduler is work-conserving (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
-