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.03Jan12Dec24Nov23221096213Oct1222Sep12Jul7530Jun29272321161312928Apr252019141110654130Mar29272423171615131042128Feb272221201428Jan2011Nov109828Sep207129Aug25181084128Jul25211914116130Jun27May26161296519Apr1413725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep23remove `coqdoc` hack from Makefile patchdefine restricted supply processor modelenforce strict subproofsfix "nonuniform inheritance" deprecation warningadd weaker definition of SBFconvert ε to notation to avoid having to unfold itsilence some warnings and change global behavior of obligation tacticbump mathcomp version to 1.18add guideline about strict subproofssimplify one proofimport ssreflect only onceremove [sequential_tasks] assumption in one proofCI: bump Coq version to 8.18introduce restricted-supply abstract RTAgeneralize [task_IBF -> job_IBF] proofrelate [scheduled_jobs_at] with [scheduled_at] on uniprocessorsuse `=` instead of `<->` [in analysis.facts.model.scheduled]remove [ideal.processor] proc. modelmake indentation more consistentsilence warningtighten bound on maximum ELF busy-interval lengthclean up [analysis.facts.busy_interval.carry_in]remove ideal uni-proc assumption from priority_inversion_bounded.vremove ideal uni-proc assumption from hep_job_scheduled.vmove `busy_interval.ideal.inequalities` -> `abstract.ideal`move `busy_interval.ideal.priority_inversion` -> `facts.model.ideal`remove `ideal.carry_in` (generalize last remaining lemma)remove ideal uni-proc assumption from ideal/busy_interval.vadd two corollaries about `is_idle` and `scheduled_at`introduce conditional interferencemove definition of [served_at] and add new lemmaadd more lemmas about [task_scheduled_at]collect trivial remarks on [same_task]relate [another_hep_job] to [same_task]lemmas about priority inversion at start of busy intervalmisc. cleanups in priority_inversion_bounded.vpull out lemma `no_priority_inversion_after_preemption_point`add two utility lemmas to `util.nat`add three auxiliary lemmas about preemption timesadd the notion of a Supply Bound Function (SBF)