Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5
  • v0.4
  • v0.3
  • v0.2
  • v0.1
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.04Dec20Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep2925221716151110987643128Aug26252418171211654331Jul30292827252422211716151413121110987611Jun15May8765430Apr22212023Mar658Aug131Jul3029fix dependency of basic readiness model on analysis factsfix dependency of preemption model on analysis factsremove unneeded 'Require' statement in behavior specremove unneeded `Require Import` statements in rt.utilCI: re-enable parallel builds in proof-state generationdisambiguate Require commands in rt.restructuringdisambiguate Require commands in rt.util and rt.classic.utiluse Gitlab DAG feature and re-organize CI orderproofloc.py: "Next Obligation" also starts a proofCI: build docs with interspersed proof stateadd script for interspersing proof state in source filesdon't pick up annotated copies in create_makefile.shadd script for recording proof stateEDF instantiationsFP instantiationsAdd concise imports of preemption modelsAdd add instances of rtc_thresholdAdd add instances of task_preemptableAdd add instances of job_preemptableAdd notion of schedule with limited preemptionsAdd proof that priority inversion is boundedAdd notion of preemptions for priority-aware schedulerAdd notion of preemption timeRestructure preemption parameters of jobAdd instantiation for ideal uni-processorAdd EDF priorityRestructure model.taskAdd notion of sequential jobs -aware policyAdd notion of busy intervalAdd lemmas about service of jobsAdd destruction tactic for ideal uni-processorAdd notion of idleness for ideal uni-processorRename and move preemption.util fileAdd notion of non-preemptive scheduleAdd lemmas about incremental serviceAdd lemma about arrivals in empty intervalMove workload lemma to basic filesAdd file to util.allAdd lemma to util.sumAdd lemmas to util.list