Skip to content

GitLab

P
PROSA - Formally Proven Schedulability Analysis

add EDF optimality argument 

This patch adds the classic EDF optimality argument: by swapping
allocations, any schedule in which no job misses a deadline can be
transformed into an EDF schedule in which also no job misses a deadline.
6 jobs for master in 3 minutes and 44 seconds (queued for 3 seconds)
9e805d0b 9e805d0b6b748eadf893697b37f4a5b8fa94feb1
1 related merge request: !13 Master
Status Job ID Name Coverage
  Build
passed #39092
1.8.0-coq-8.8

00:02:04

passed #39094
1.9.0-coq-8.9

00:02:08

failed #39093
allowed to fail
1.9.0-coq-dev

00:00:14

 
  Process
passed #39096
doc

00:00:23

passed #39097
proof-length

00:00:16

passed #39095
validate

00:01:33

 
Name Stage Failure
failed
1.9.0-coq-dev Build There is an unknown failure, please try again 
COQC util/powerset.v
COQC util/seqset.v
File "./util/seqset.v", line 19, characters 42-52:
Error: The reference mkPredType was not found in the current environment.

make[1]: *** [Makefile:659: util/seqset.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile:321: all] Error 2
ERROR: Job failed: exit code 1