Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa protected
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5 protected
  • v0.4 protected
  • v0.3 protected
  • v0.2 protected
  • v0.1 protected
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.018Apr17151215Feb141397625Jan2423221918171615141210864312Dec24Nov23221096213Oct1222Sep12Jul7530Jun29272321161312928Apr252019141110654130Mar29272423171615131042128Feb272221201428Jan2011Nov109828Sep207129Aug25181084128Jul25211914116130Jun27May26161296519Apr1413725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19prove a lemma about intra-interference splitrelax assumption in bounded busy interval lemmaprove alt. version of intermediate point lemmaprove that FIFO has no service inversionprove abstract search space ⊆ RS FIFO search spacefix a typo in commentprove RTAs for RS-FP-EDF and RS-NP-EDFprove busy-interval length bound for RS-EDFprove simple busy-interval length bound for JLFPimprove structure to avoid duplication laterprove that job causing service inversion is uniqueprove a few util lemmasprove abstract search space ⊆ RS EDF search spaceadd lemma about service inversion boundmove a few files to improve folder structureimprove comments about service lemmasadd a lemma about total RBF boundde-duplicate EDF hep-workload bound definitionadd corollary about only one job causing pimove busy interval definitionbound max non-preemptive low-pr segment under EDFgeneralize proof of busy interval from no-carry-ingeneralize workload-bounded predicateprove that ideal sched is unit-supply proc modeluse `Instance` syntax to define RTC threshold instancesmake `eq_sum_seq` rewritableremove superfluous util.list lemmaremove work-conservation dependency from the priority inversion fileCI: complain and fail if there are warningsupdate to Coq 8.19 and MathComp 2.2.0generalize task-cost inequality lemmaadd some lemmas about RBFsadd some guidelines on "!" in context declarationsadd some lemmas about workloadprove restricted supply FP-FP RTAprove that task intra-supply IBF is a valid boundremove unnecessary dependency on Task in aRTAsmall refactor of arrivals lemmasprove that busy intervals are bounded for RS-FPadd the notion of monotone SBF