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.019Jan18171615141210864312Dec24Nov23221096213Oct1222Sep12Jul7530Jun29272321161312928Apr252019141110654130Mar29272423171615131042128Feb272221201428Jan2011Nov109828Sep207129Aug25181084128Jul25211914116130Jun27May26161296519Apr1413725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov191815add [arrives_in] to SBF defAdd I/IW instantiation for restricted supplyprove existence of abstract busy intervaladd notion of speculative executiongeneralize proof and improve structurerestructure I/IW instantiation filesadd proofs about jitter propagationadd definition of propagated arrival curvesdefine task-level release jitter parametergeneralize a few "bigcat" lemmasprove supply related properties of ideal uni-procintroduce more notions of serviceintroduce more notions of workloadimprove proof scriptremove trailing spacesprove that service inversion is boundedadd a few lemmas about service and schedulabilityimprove terminology about priority inversionprove a few facts about service inversionadd a few auxiliary lemmasadd notion of service inversionremove [priority_inversion_is_bounded_by_constant]improve comment about [priority_inversion]use fully qualified namesimprove SBF definition structureadd sequential restricted-supply aRTACI: use locally hosted Docker imagesremove Makefile.coq.patch hackremove esy $HOME hackremove CoqDocJS and Alectryon hackwork around Coq bug #18434remove `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 subproofs