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.023Aug21201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep2925221716151110987643128Aug26252418171211654331Jul30292827252422211716151413121110987611Jun15May8765430Apr22212023Mar658Aug131Jul3029note equivalence of assumptions in case of basic readinessprove ready jobs are incompletemake definition of completed_jobs_dont_execute uniformprove jobs must arrive to be readydefine [backlogged] in terms of job readinessnote that ideal processor model provides unit serviceadd [n + k <= m => n <= m] helper lemmatighten response-time recurrence for EDFChange name of a matched variableadd EDF optimality argumentadd prefix_map transformation and two supporting lemmasadd utility function search_arg for searching across schedulesadd theory of schedules with swapsadd two notions of "all deadlines met" independent of tasksnote two simple facts about job deadlinesintroduce a utility lemma on points outside of intervalsadd subn_abba helper lemmaadd ltn_leq_trans utility lemmastart classification of processor modelsdefine preemptive work-conserving and priority-based schedulesRemove superfluous variableport definitions for arrival curvesenable proof-length checking during CIadd scripts/proofloc.py, a utility for checking proof lengthport notions of job/task deadlines and schedulability to restructuringsimplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to modelclean up the new schedule definitionsautomatically build HTML docs as part of CIsplit out 'make validate' into individual jobsimplify CI setup by using official mathcomp Docker imagesChange definition of completionport existing proofs to ssreflect 1.9.0Copied model/schedule/uni/basic/platform_tdma.v to restructuring/model/schedule/tdma.vcopied everything from model/policy_tdma.vapplied naming convention to behaviormove readme to restructuring rootfix indentation in completion.vAdd sporadic task modeladd task_cost containing definitions related to the WCET modelmove job_cost to job.v