Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • PG_bin_EDF
  • POET
  • aSBF
  • aSBF_PG
  • aSBF_PG_bin
  • aSBF_PG_bin_per_dmin
  • arrival-curves
  • assumptionless-example
  • certa-examples
  • certificates_update
  • completed-jobs-arent-served
  • concrete_tasks
  • ecrts20
  • fix_task_interference
  • generalize-jobready
  • generalize-proof
  • lightning_POET
  • master default
  • maximal-arrival-sequence
  • merge_temp
  • v0.4
  • v0.3
  • v0.2
  • camera-ready-ecrts-2016
  • paper-submission-ecrts-2016
  • v0.1
26 results
Created with Raphaël 2.2.017Apr151215Feb14139876225Jan24232219181716151412108654312Dec24Nov23221096213Oct1222Sep25Jul24127530Jun2928272321161312928Apr252019141110654130Mar29272423171615131042128Feb271428Jan2011Nov109828Sep207131Aug2925181084128Jul2521191814116130Jun27May2618161210976543229Apr191413728Mar2524181716114325Feb1817161514931Jan1328Dec2715729Nov252423543214Oct1211765430Sep29282724232221improve 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 warningsmastermasterupdate 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 workload[to squash]generalize-jobr…generalize-jobready[to squash][to squash][to squash][to squash][to squash][to squash][to squash]remove proof-term from JobReady type-classprove restricted supply FP-FP RTAprove that task intra-supply IBF is a valid boundremove unnecessary dependency on Task in aRTAsmall refactor of arrivals lemmasa lot of changescompleted-jobs-…completed-jobs-arent-servedinteresting changes