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.014Apr13725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410Remove leq_addkRemove subn_abbaadd lemmas about [service_of_jobs]introduce the notion of "total service of jobs"rename `np_uni_schedule` to `pmc_uni_schedule`add alternate interpretation of numeric prioritiesmake naming consistent and fix commentsfix the `job_preemption_points` name clashCI: fix opam-triggered recompilationdemonstrate arrival-model conversion with an exampleenable periodic->RBF auto conversionenable automatic arrival-model conversionreorganize arrival model conversionsadd sporadic task -> arrival curve interpretationestablish an arrival bound for sporadic tasksadd auxiliary lemmas on `{task_}arrivals_between`establish that `arrivals_between` is sortedadd lemma on `div_ceil` on integer multiplesclean up facts.sporadic.arrival_timesrestructure sporadic task factssporadic task analysis: remove unneeded TaskMaxInterArrivalsporadic tasks analysis: remove unnecessary offset parameterCI: drop Coq < 8.14 and mathcomp < 1.13revise ideal uniprocessor schedule factsimport and comment tweaks in results & analysisstreamline some imports in the results modulemake the limited-preemptive job model a local instancemake the non-preemptive job model a local instancedisambiguate `fully_preemptive_job_model`disambiguate preemption model and RTC threshold instancesMake the floating preemptive model hypothesis more explicitMake the limited_preemptive mode hypothesis more explicitMake the fully nonpreemptive model hypothesis more explicitMake the fully preemptive model hypothesis more explicitRemove suspension readiness Global InstanceRemove sequential readiness Global InstanceRemove jitter readiness Global InstanceMake the basic readiness hypothesis more explicitRemove multiprocessor Global InstanceRemove var. speed processor model Global Instance