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.08Sep30Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep2925221716151110987643128Aug2625241817121165misc. code and comments polishcleanup: coqdoc fixes and unnecessary ideal uniprocessor assumptionMakefile: allow alectryon to work in parallelCI: remove old proof-state scriptsCI: use custom Docker image for proof-state collectionCI: don't run expensive jobs in wip- branchesCI: use alectryon for proof-state displayadd alectryon wrapper script and `make alectryon` targetadd sequential and work-bearing readiness modelsFixed warningsAdd setoid rewriteestablish preemption model compliance of np_uni_scheduleadd proof of equivalence of EDF definitionsadd definitions of super- and sub-additivityCompile with Coq 8.13 and mathcomp 1.12define completion sequencesadd `bigcat` over sequencesadd lemmas to sumcomment on ssrlia tacticrefactor and comment summation utility lemmasoptimize names for run-to-completion threshold functionsMinor documentation changes about tactics.generalize definition of busy intervalAdd [arrives_in] to [sequential_tasks] definitionadd standard conversions from arrival curves to RBFsproof state recorder: add more out-of-sync checksproof state recorder: don't trip over vernacular commandsproof state recorder: handle multiple closing '}'proof state recorder: fix double prompt detectionproof state recorder: add --pause optionproof state recorder: check expected interaction numberfix minor warningdefine a shifted job costs function and prove its validitymake the proof-state collector slightly more robustProved optimality of work-conserving EDF schedulesAdd Request Bound FunctionsTwo small lemmasCoq 8.10 no longer supported since #104add notion of offset, job index and proof of periodic arrival timesimprove the EDF optimality proof by reasoning about prefixes