Commit graph

2763 commits

Author SHA1 Message Date
Anna Lyons
f88d58aa8d Fix scheduling behaviour on seL4_SchedContext_YieldTo
When yieldingTo a same prio thread, the same prio thread should run
first, not the current thread. Due to changes to possibleSwitchTo in
master scheduler this code became outdated and the current thread would
be rescheduled immediately.

The desired behaviour is that the thread being yieldedTo should be at
the head of the scheduler queue for its priority, and the current thread
should be just after it.
2018-12-03 13:33:13 +11:00
Anna Lyons
c31272511f Preserve the value of scConsumed when seL4_Yield is called
We use the chargeBudget logic in the kernel on seL4_Yield to free up
the budget available in the head refill, however this
updates scConsumed. Given this is a simulated charge (the thread is
yielding the budget, not actually using it), this is incorrect.
2018-12-03 13:33:13 +11:00
Anna Lyons
e36f727272 remove incorrect line from refill_split_check 2018-12-03 13:33:13 +11:00
Gerwin Klein
74daf5fc35 Allow only unbound SC/TCB in SetSchedParams call
This removes some special-casing from the proof.
2018-12-03 13:33:13 +11:00
Gerwin Klein
4267811622 minor: sync comment with code 2018-12-03 13:33:13 +11:00
Gerwin Klein
e75d364b50 Swap TCB cap install order in invokeTCB_ThreadControl
Installing the endpoint caps before the CSpace/VSpace roots is easier for
verification, because deleting endpoint caps is always well-behaved, but
CNode cap deletion can be complex.
2018-12-03 13:33:13 +11:00
Anna Lyons
927c9b60b9 smp: always migrateTCB on schedcontrol_configure
we have no guarantees as to where the FPU context is
2018-12-03 13:33:13 +11:00
Anna Lyons
ef47fa6e3c smp: remove excess code in schedContext_donate
- always migrate the TCB (the FPU context could be anywhere)
- don't need to call migrateTCB or rescheduleRequired, this is handled
by calling paths.
2018-12-03 13:33:13 +11:00
Anna Lyons
8eb9ccd270 smp: remove excess remote call stall in unbindTCB
This isn't required as all code paths into this function have already
stalled the tcb
2018-12-03 13:33:13 +11:00
Anna Lyons
c4e2b23aba smp: remove excess code in bindTCB
- we know the tcb does not have an SC at this point
- it may need to migrate if the FPU context is still on the other core.
2018-12-03 13:33:13 +11:00
Anna Lyons
ab9f2a7e2c smp: use tcbAffinity everywhere rather than scCore
Using scCore is inefficient as we don't need to reach into another
object for this value when the tcbAffinity == scCore
2018-12-03 13:33:13 +11:00
Anna Lyons
ed6f9c6fde x86-smp: remove check on Arch_migrateTCB
This check is not required and aligns the code back with master.
2018-12-03 13:33:13 +11:00
Anna Lyons
56ec98db93 Fix build error on SMP 2018-12-03 13:33:13 +11:00
Anna Lyons
fde93303ad Update version file for MCS kernel 2018-12-03 13:33:13 +11:00
Anna Lyons
1a8716dd97 SchedControlConfigure: charge correct core
Previously this code would incorrectly call chargeBudget twice, where it
was intended to be charging a specific core.
2018-12-03 13:32:58 +11:00
Anna Lyons
a81ddbdf31 remove reply_clear
no longer used
2018-12-03 13:32:58 +11:00
Anna Lyons
9382133315 Use cancelIPC instead of reply_clear
reply_clear only does half the job
2018-12-03 13:32:58 +11:00
Anna Lyons
1be61dc33c reply_pop: do not call donate if SC is not NULL
This handles the specific case where a thread has donated its SC
over a Call but then is bound to another SC before the reply is
executed. In this edge-case, the donated SC remains with the callee.
2018-12-03 13:32:58 +11:00
Anna Lyons
2280c2063a remove superfluous setThreadState in completeYieldTo
- this was causing headaches for verification and was redundant after
the specific yieldTo state was removed.
2018-12-03 13:32:58 +11:00
Anna Lyons
bd9771a493 SELFOUR-1352: avoid overridding scYieldFrom
This change causes any previous yeildTo to complete before updating
scYieldFrom.
2018-12-03 13:32:58 +11:00
Anna Lyons
62e6a2c243 style 2018-12-03 13:32:58 +11:00
Anna Lyons
61ab6fd9aa Pass slot through to functions that dereference it 2018-12-03 13:32:58 +11:00
Anna Lyons
6f9010ebc5 Define CONFIG_KERNEL_WCET_SCALE 2018-12-03 13:32:58 +11:00
Anna Lyons
4972a41c7c Unbind reply in seL4_SchedContext_Unbind 2018-12-03 13:32:58 +11:00
Anna Lyons
a3102e993f Fix donation bug on smp new-rt kernel
Set the sc field to NULL after manipulating scheduling queues - on smp
we use the sc to obtain the core id. However, also NULL it before
rescheduleRequired or a thread without an SC could end up in the
scheduler.
2018-12-03 13:32:58 +11:00
Anna Lyons
486ab32ccf Implement RT timer driver for KZM
- use gpt, so we can have overflow and compare interrupts at the same
time (epit only allows compare)
- set the gpt to use the ipg_highfreq timer, as the standard ipg is too
low and breaks the timer calculations
2018-12-03 13:32:58 +11:00
Anna Lyons
f380924e4e Refactor replies to solve revoke problems.
Before this change, we set the replyObject in the thread state on recv
with no back pointer such that stray pointers would be left in the
thread state when a reply object was completed.

The new semantics are clearer and fix this problem by doing the
following:

- tcb->tcbReply is removed and the thread state field is always used,
this was unneccessary duplication previously
- the thread state value is set to the reply object only when the thread
is in BlockedOnReply or BlockedOnRecv
- the reply contains a back pointer, replyTCB, which points to that
thread
- if a thread has its reply removed, it must be set to
ThreadState_Inactive.
- deletion is easy in the blockedOnRecv case, we just unlink the reply
and the tcb.
- deletion is complicated for blockedOnReply. If we are deleing a tcb, we remove the actual
reply object and the call chain is broken. If we are deleting a reply,
we maintain the call chain by moving the tcb to the next reply.
- we refactor the reply object interface to solve the above.
    * reply_clear: removes the reply from any connections (tcb, sc)
    * reply_unlink: just unlinks the tcb and reply, and sets the thread
    state to inactive
    * reply_remove: removes the reply from the call chain
    * reply_remove_tcb: removes the exact reply that a tcb is bound to,
    as we are removing that tcb. Breaks the call chain.
2018-12-03 13:32:58 +11:00
Anna Lyons
fda6b1ee64 Use call_stack_new instead of setting the pointer
The proofs are free and we're touching those words anyway, and we know
the value.
2018-12-03 13:32:58 +11:00
Anna Lyons
5ff0338b89 Set thread state to blockedOnReply in reply_push 2018-12-03 13:32:58 +11:00
Anna Lyons
a9096aa4e8 Fix scheduler after invert fastpath merge
Set sc to NULL before calling reschedule required and check
ksSchedulerAction.

Due to changes in the scheduler (invert-fastpath and friends) reschedule
required would put a thread without an SC into the scheduler, which is
fail.
2018-12-03 13:32:58 +11:00
Anna Lyons
968871e7a6 remove ThreadState_YieldTo due to duplication
We can check the tcbYieldTo field rather than adding another thread
state
2018-12-03 13:32:58 +11:00
Anna Lyons
2773a03500 Fixes for aarch64 fastpath
- pass reply cptr to handle_syscall
- remove unused function
2018-12-03 13:32:58 +11:00
Anna Lyons
d941918414 Fixes for ARM SMP 2018-12-03 13:32:58 +11:00
Anna Lyons
2f6a75b733 Fix seL4_BenchmarkFinalizeLog
It did not compile on this branch
2018-12-03 13:32:58 +11:00
Anna Lyons
a2dea2828e Update seL4_FaultType to 4
With timeout faults + arm_hyp the number of faults won't fit in 3 bits.
2018-12-03 13:32:58 +11:00
Anna Lyons
7b15809d88 Fix aarch32 low frequency usToTicks
Prior to this commit we attempted to use reciprocal division to
divide by 1000, which is required on platforms where calculations must
be performed in KHz for precision. This overflowed too quickly.

Use div64 specifically for usToTicks, and move getMaxUsToTicks to the
arch level.
2018-12-03 13:32:58 +11:00
Anna Lyons
23cb84976c Move div64 to mode specific include
Such that they can be used on all architectures.
2018-12-03 13:32:58 +11:00
Anna Lyons
8f05e28ac9 aarch64: fix RT build for aarch64
- update seL4_NotificationBits
- add Timeout to types.bf
- update system call stubs
- add RT register definitions
- update getMaxUsToTicks and getMaxTicksToUs
2018-12-03 13:32:58 +11:00
Anna Lyons
c3de88f8da Fix broken syscall_sysenter stubs 2018-12-03 13:32:58 +11:00
Adrian Danis
7c4ac07380 Update cmake build information for new-rt branch
This updates the cmake build information for new-rt branch specific changes
2018-12-03 13:32:58 +11:00
Anna Lyons
e6424fa45e Check budget is sufficient in preemptionPoint()
When we enter the kernel we know we have at least getKernelWcetUs
budget. Preemption points need to maintain this invariant and check
again.
2018-12-03 13:32:58 +11:00
Anna Lyons
dfe6904154 Increase WCET us for tk1
The TK1 is running at 700Mhz so this needs to be slower
2018-12-03 13:32:58 +11:00
Adrian Danis
8fb9b9afb9 Migrate if the TCBs affinity should change, not the contexts
If we modify a scheduling context, and it has a bound TCB, then we need to migrate the TCB
if its affinity should change based on the new affinity of this scheduling context
2018-12-03 13:32:58 +11:00
Anna Lyons
21730c53fb Correctly migrate threads on context donation
As we're changing schedulability we must tell remote cores to reschedule, and also
reschedule local core if we are migrating into the current core.
2018-12-03 13:32:58 +11:00
Anna Lyons
94be100a31 Remove reundant remoteTCBStall
Remote thread will be stalled if needed during migration, but there is no
reason for us to explicitly stall
2018-12-03 13:32:58 +11:00
Anna Lyons
3087da4ec1 Use higher level migrateTCB
This was introduced in prior commits and automates migration and setting
the thread affinity
2018-12-03 13:32:58 +11:00
Anna Lyons
ab895d6d5f Remove redundant SMP_COND_STATEMENT
Code is already in an `#ifdef ENABLE_SMP_SUPPORT`
2018-12-03 13:32:58 +11:00
Anna Lyons
11de1142f8 Use helper definition ENABLE_SMP_SUPPORT 2018-12-03 13:32:58 +11:00
Adrian Danis
93290dd8d6 Fix incorrect WCET spelling 2018-12-03 13:32:58 +11:00
Adrian Danis
b1e01755bc Scale kernel WCET estimate by configurable amount
This configuration option allows for building images destined for simulators,
which may not simulate as fast as hardware, to still be used
2018-12-03 13:32:58 +11:00