This project is mirrored from https://github.com/seL4/seL4.git. Pull mirroring updated .
  1. 07 May, 2021 1 commit
  2. 05 May, 2021 1 commit
  3. 04 May, 2021 6 commits
  4. 30 Apr, 2021 5 commits
    • Curtis Millar's avatar
      mcs: Clear ksConsumed when charging to revoked SC · bbd3f5ab
      Curtis Millar authored
      
      
      When a revoke operation clears the current SC, that SC can't continue
      operation past the subsequent preemption point. Presumably, that SC had
      sufficient budget for each iteration up to the last and could have been
      charged for the last iteration.
      
      Simply setting the consumed time to 0 at the point where the SC would
      have been charged is equivalent to charging the time to that SC priori
      to its being cleared, including any accounting for overrun.
      Signed-off-by: default avatarCurtis Millar <curtis.millar@data61.csiro.au>
      bbd3f5ab
    • Kent McLeod's avatar
      mcs: call updateTimestamp in preemptionPoint · 9663e1e6
      Kent McLeod authored
      
      
      Call updateTimestamp unconditionally whenever ksWorkUnitsCompleted
      exceeds the preemption level. This is necessary such that future calls
      to checkBudget and chargeBudget occur with the correct time consumed.
      Signed-off-by: default avatarKent McLeod <kent@kry10.com>
      9663e1e6
    • Kent McLeod's avatar
      mcs: Update ksDomainTime in updateTimestamp · fa4f1bae
      Kent McLeod authored
      
      
      When ksDomainTime reaches 0 the current domain expires and the next
      domain is switched to. This change performs the domain time accounting
      in one place, in updateTimestamp, and avoids situations where ksConsumed
      is reset without also updating ksDomainTime such as in chargeBudget.
      
      Calling rescheduleRequired in the domain expires ensures that a new
      thread will be chosen in the scheduler after the domain has been
      advanced.  Any remaining ksConsumed will be charged to the outgoing
      scheduling context when it is switched away from.
      Signed-off-by: default avatarKent McLeod <kent@kry10.com>
      fa4f1bae
    • Curtis Millar's avatar
      mcs: Defer charging budget in preempted invocation · 8373f0a0
      Curtis Millar authored
      
      
      Rather than charge consumed time to the current thread at the point
      where it is exhausted in a long-running syscall, we only check whether
      checkBudget would fail and raise an exception if it would. We then
      always charge after handleInvocation rather than avoid-double charging.
      
      This is done as it is easier to add the exhaustion case in the abstract
      spec in this manner (without also adding changes to the current SC).
      Signed-off-by: default avatarCurtis Millar <curtis@curtism.me>
      8373f0a0
    • Curtis Millar's avatar
      mcs: Don't assume active SC at preemption · 0647a84c
      Curtis Millar authored
      
      
      At a preemption point the current SC may have been revoked and cleared
      and would thus no longer be configured. In this case, it woudl be
      invalid to perform a checkBudget and so we just treat it as a preemption
      and don't charge any budget.
      Signed-off-by: default avatarCurtis Millar <curtis.millar@data61.csiro.au>
      0647a84c
  5. 29 Apr, 2021 6 commits
  6. 28 Apr, 2021 1 commit
  7. 21 Apr, 2021 1 commit
  8. 20 Apr, 2021 1 commit
    • Ben Leslie's avatar
      Fix MCS / ARM64 VCPU interrupt interaction · c64867eb
      Ben Leslie authored
      See: https://github.com/seL4/seL4/issues/346
      
       for details.
      
      VPPIEvent and VGICMaintenance handling is updated to first
      check that the current thread has budget. If it does not
      have budget the interrupts are ignored. As interrupts are
      level-triggered this effectively just delays the interrupts.
      
      The check for budget is based on determining if the current
      thread is enqueued. This occurs if (and only if) the current
      thread has had a budget check that is expired.
      Signed-off-by: default avatarBen Leslie <benno@brkawy.com>
      c64867eb
  9. 14 Apr, 2021 3 commits
    • Curtis Millar's avatar
      mcs: Add explicit checks to not unblock current SC · 5fd9619f
      Curtis Millar authored
      
      
      The current version of the proofs does not track whether the current SC
      is bound to the current thread or any thread at all in the proof state.
      As a short-term workaround, we add explicit checks in the kernel to
      guarantee that we don't treat the current SC as having been unblocked
      rather than relying on static knowledge that this doesn't occur.
      
      The proofs should be updated in the future with all of the checks
      introduced in this PR removed.
      Signed-off-by: default avatarCurtis Millar <curtis.millar@data61.csiro.au>
      5fd9619f
    • Curtis Millar's avatar
      mcs: Add sporadic flag to SchedControl_Configure · afbea157
      Curtis Millar authored
      This adds a flags parameter to SchedControl_Configure to enable
      configuration of a sporadic SC.
      
      This also allows flags to be added in the future as needed without
      breaking the API.
      
      This allows the user to configure an SC either to be constrained as a
      sporadic task where accumulated time is only delayed to when a task has
      become runnable (implementing the sporadic server algorithm) or
      whenever the task becomes the current executing task (implementing the
      sliding-window constraint as in constant-bandwidth servers).
      
      This can be used to prevent non-realtime tasks from exceeding bandwidth
      under any circumstances, even in an over-committed configuration, whilst
      also allowing work-conserving tasks to be configured in the same system.
      
      To implement sporadic servers, we need to ensure that the suspension of
      a task cannot be used as a mechanism to amplify budget of a task by
      granting that task access to effectively multiple periods worth of
      replenishments within a...
      afbea157
    • Kent McLeod's avatar
      mcs,sporadic: Remove calls to refill_unblock_check · 9f0381c2
      Kent McLeod authored
      
      
      refill_unblock_check is called in switchSchedContext whenever an SC is
      switched to. Any other calls would have no effect:
      - If the SC was already running then it would have had
        refill_unblock_check already called on it,
      - If the SC was not already running, then it would have
        refill_unblock_check called when it was next switched to which would
        override the previous call.
      Signed-off-by: default avatarKent McLeod <kent@kry10.com>
      9f0381c2
  10. 12 Apr, 2021 1 commit
    • Ben Leslie's avatar
      Fix MCS refill_order assertion on SMP · 5b2a9250
      Ben Leslie authored
      The `refill_order` assertion is only applicable when the scheduling
      context is not round-robin.
      
      Assertions are changed such that `refill_order` is only asserted
      when the the scheduling context is *not* a round-robin scheduling
      context.
      
      When performing `maybe_add_empty_tail` the `rTime` attribute
      is updated to the existing time. This smplifies as compared
      to existing code. Another option could be to set to zero, however
      this brreaks invariants relied on for verification.
      
      See: https://github.com/seL4/seL4/issues/262
      
      Signed-off-by: default avatarBen Leslie <benno@brkawy.com>
      5b2a9250
  11. 08 Apr, 2021 2 commits
  12. 07 Apr, 2021 3 commits
  13. 06 Apr, 2021 5 commits
  14. 01 Apr, 2021 4 commits