Library transfer.transfer_schedulability

• Transfer Schedulability for Ideal Uniprocessors
  • System Model
  • Well-Formedness of the Schedules
• Definition of "Schedulability Transfer"
• Auxiliary Lemmas to be Submitted to Prosa
• Setup for the Generic Argument
  • The Remaining Job-Cost Bound
    • Basic Facts About the Remaining Job-Cost Bound
    • Relation to the Remaining Online Cost
  • The Set of Critical Jobs
    • Basic Facts About the Set of Critical Jobs
  • Definition of Slackless Intervals
• The Schedulability Transfer Criterion
• Existence of a Contiguously Slackless Interval
  • Supporting Lemmas
  • Intervals of Non-Positive Slack
    • Facts about Intervals with Non-Positive Slack
  • Main Argument: Slackless Interval Existence
• All Critical Jobs Complete in a Contiguously Slackless Interval
• Main Results
  • Sufficiency Theorem w.r.t. Online Job Costs
  • Necessity Theorem w.r.t. Online Job Costs
  • Sufficiency Theorem w.r.t. Reference Job Costs

Library transfer.paper_model

• Connecting the General Result to the Model in the Paper
• Elements of the EMSOFT System Model
  • Precedence and Delay
    • Job Parameters
    • Definition of Job Readiness
  • System Evolutions
  • Scheduler Interface
• Instantiation of the EMSOFT System Model
  • The Set of Jobs
  • Ideal Uniprocessor Assumption
  • System Evolutions
  • The Schedulers
  • Clairvoyant Results
  • Nonclairvoyant Result
• Results w.r.t. Finish Times
  • Non-Starvation Assumption
  • Definition of Finish Times
  • Clairvoyant Sufficiency Result for Finish Times
  • Nonclairvoyant Sufficiency Result for Finish Times
  • Clairvoyant Necessity Result for Finish Times
    • Online Finish Times, Revisited
    • Clairvoyant Necessity Theorem