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.01Aug28Jul25211914116130Jun27May26161296519Apr1413725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan19generalize some parts of the EDF aRTA instantiationgeneralize priority inversion definitionadd lemma about [service_of_jobs_at]add auxiliary lemmas about ideal scheduleadd computed fixpoints for FP-FP RTAadd utilities for finding fixpoints of functionsadd lemmas on misc. properties of total RBF variantsadd a lemma on the monotonicity of sums of monotonic functionsfix comments for hypothesisclean up proofsremove sequential tasks assumption from EDF RTAmake assumption weakergeneralize lemma for bound on busy windowadd more lemmas to [basic_rt_facts]add lemmas about [workload_of_jobs]simplify GEL definitionexclude the blocking bound from the EDF search spaceadjust FP NPS PI-blocking bound proof to narrowed definitionnarrow priority-inversion bound to jobs with non-zero costadd utility lemmas on `\max_( r <- xs)` (bigmax)add fact about non-pathological arrival curvesaRTA clean-upfix various deprecation warningsremove unnecessary `unfold prefix`classic: fix deprecated mathcomp symbolsrename `prefix` -> `prefix_of`CI: bump mathcomp versionadd concrete job constructorupdate license, silence opam warningCI: account for proof irrelevance when checking validation outputadd --without-refinements option to ./create_makefile.shopam: constrain min. supported versionadd refinements needed for POETCI: add CoqEAL dependencyCI: factor out common codeCI: simplify the setup to use a single stageremove redundant clause from `busy_intervals_are_bounded_by`improve readability of analysis.abstract.definitionsimprove the bound on arrival blocking under EDFRename [ideal_schedule] into [ideal.schedule]