Commit graph

31 commits

Author SHA1 Message Date
Adrian Danis
eccaae51dc s/D61/DATA61/ in license headers for consistency 2017-02-21 16:38:51 +11:00
Adrian Danis
c574f4fc48 Helper for allocating the extra boot info region 2017-02-16 14:34:52 +11:00
Adrian Danis
4f52aca5b1 Remove multiple stack definitions
This commit changes the stack so that it is declared a single time in stack.c,
with the correct attributes and alignment, instead of being declared in stack.h
and relying on the linker to collapse the multiple declarations.
2017-02-06 15:42:37 +11:00
Hesham Almatary
c156c9dddd Merge pull request #607 in SEL4/sel4 from ~HALMATARY/sel4:KernelStacks to master
* commit 'be77963e5bb4c5c28ad3ebd8746c292e7b5876f6':
  Define CONFIG_MAX_NUM_NODES and CONFIG_KERNEL_STACK_BITS in plat/autoconf.h
  Unify kernel stack definition/declaration and share it between architecures/modes
2017-01-18 12:43:34 +11:00
Hesham Almatary
e9922b7456 Unify kernel stack definition/declaration and share it between architecures/modes
Rather than defining a kernel stack in random places for each
architecure for each mode (32/64) and for single/SMP modes, make the
stack definition shareable between all of the above. This is also useful
for the future ARM SMP work.
2017-01-17 15:52:58 +11:00
Hesham Almatary
af02927b69 SMP: move lock.h to architecture-independent include/smp
s/__sync_lock_test_and_set/__atomic_exchange_n in lock.h
2017-01-16 15:21:50 +11:00
Anna Lyons
b827ad37ba SELFOUR-413: refactor libsel4 fault API
This is a *breaking API change*

This commit:

* makes seL4_Fault_tag_t common between the kernel and libsel4
* deprecates the existing functions from sel4/messages.h includes
* introduces a new fault API in sel4/faults.h and
* sel4/sel4_arch/faults.h
* deprecates seL4_GetTag(), as the function did not work without
  the user calling seL4_SetTag() first (seL4_MessageInfo is passed
  in registers and not set in the IPC buffer)
* removes previously deprecated functions (deprecated prior to 3.0.0)
* updates the seL4 manual to reflect the changes
2016-11-25 12:29:07 +11:00
Adrian Danis
cc6853017d Remove unneeded usages of VISIBLE
Using `VISIBLE` where it is not needed limits the ability for the
compiler to optimize, especially when using whole program optimizations
2016-11-24 14:46:01 +11:00
Adrian Danis
7f76749448 Revert SELFOUR-242
This reverts commits
3aee0ab7b3
6b6b965528
a1421832ac
2016-11-16 14:02:11 +11:00
Anna Lyons
a1421832ac SELFOUR-242: invert bitfield scheduler & optimise
This commit does the following:

* invert the bit field scheduler for better cache performance for high priority threads
* peeks into the bitfield scheduler to allow fastpath to be leveraged when IPC occurs from lo --> hi priority threads if correct
2016-11-15 09:45:48 +11:00
amrzar
25bb94372f SELFOUR-635: support for TCB operations
This will update TCB invocations to consider multicore environment, this may include:
- adds the affinity invocation to transfer TCB between different cores and update TCB structure for core ID
- checking the thread/core state before performing TCB operation, e.g. deleting the runnable TCB, etc
2016-10-30 08:59:32 +11:00
amrzar
e63be664c6 SELFOUR-631: implement CLH lock and barrier infrastructure 2016-10-06 11:50:57 +11:00
Anna Lyons
7336303b7f SELFOUR-276: Add MCP field to threads.
Where MCP = Maximum Controlled Priority

This commit adds:

* seL4_TCB_SetMCPriority

and changes the arguments to

* seL4_TCB_Configure

As of this commit, a thread cannot create or set a threads
priority (including itself) above its mcp. Previously the kernel
did this check against a threads priority, which prevented a thread
from setting it's own priority down and then up again.
2016-10-05 11:11:19 +11:00
Adrian Danis
d507b2d39e SELFOUR-421 Introduce explicit device frames and untypeds
Kernel objects cannot be created from device untypeds, with the
exception of frames, which do not get zeroed and cannot be used
as an IPC buffer. Device untypeds additionally cannot be used
in the construction of ASID pools.

This then changes the API to the rootserver (i.e. bootinfo) to
send device untypeds instead of device frames. On ARM these
device untypeds are the same as the previously exported device
frame regions. On x86 PCI scanning is removed and all physical
memory addresses (that are not important for kernel integrity)
are released to the user.

In order to have bits in the frame and untyped caps on ARM the
number of software ASIDs had to be reduced from 2^18 to 2^17,
and the maximum untyped size reduced from 2^31 to 2^30
2016-09-23 14:15:08 +10:00
Anna Lyons
ef00e98689 SELFOUR-615: arm entry point stubs 2016-08-24 10:42:36 +10:00
Adrian Danis
e0f8111faa move benchmark code from arch hooks 2016-08-24 10:42:36 +10:00
Adrian Danis
5466105cb9 call arch entry hook from C entry hook 2016-08-24 10:42:36 +10:00
Adrian Danis
4c57e6e577 define arch entry hooks instead 2016-08-24 10:42:36 +10:00
Hesham Almatary
16c3481109 SELFOUR-518: User-level log buffer
Remove global ksLog and use KS_LOG_PPTR instead

Benchmark - Log buffer: use global page table
2016-08-15 15:06:38 +10:00
Anna Lyons
289bf92bf0 SELFOUR-114: remove bootinfo.h duplication 2016-03-01 17:25:22 +11:00
Adrian Danis
e61a1056cc SELFOUR-56: Remove diminish rights from IPC
Diminish rights were to prevent a user from sending a writeable
cap over a read only endpoint. It turns out this 'security' can
be worked around without difficulty (by putting caps in a cnode
and sending the cnode) making the current diminish rights
implementation functionally useless.

Removing diminish rights has the benefit of simplifying all the
IPC paths.
2016-02-23 13:58:48 +11:00
Adrian Danis
68887cd836 x86: Populate the freemem list from the multiboot mem list
If the multiboot memory list exists, then it may contain more
than just the single contiguous memory region listed in 'mem_upper'
Therefore we use it to populate a more complete free memory list,
if it exists
2016-01-12 10:59:08 +11:00
Adrian Danis
0ecff9f393 unsigned int -> word_t 2015-12-10 10:45:21 +11:00
Adrian Danis
2d61910e0f Rename uint32_t -> word_t in any relevant places 2015-12-10 10:45:20 +11:00
Yanyan Shen
9f2d521979 Make cspace address walking 32/64-bit agnostic 2015-12-10 10:45:19 +11:00
Anna Lyons
a99a10408d SELFOUR-279: rename Wait -> Recv, add wrappers for seL4_Poll and seL4_Wait for notification objects.
This commit deprecates seL4_ReplyWait, removes seL4_NBwait completely,
and changes the return type of seL4_Wait to void (seL4_Wait should be
used for notification objects, and seL4_Recv should be used where
seL4_Wait was used previously for endpoints).
2015-11-20 15:28:18 +11:00
Adrian Danis
8743737dae Use CONST instead of PURE in thread functions
As these functions do not read any global state they fit
within the subset of PURE that can be declared as CONST
2015-10-23 15:02:53 +11:00
Stephen Sherratt
62727e30a2 Using bitfields to track for which priorities there exist non-empty ready queues.
Background
seL4 organizes threads into ready queues, of which there is one for each
domain, for each priority level. The ready queue for a given
domain/priority combination can be found by indexing the array
`ksReadyQueues` with "domain*num_priorities + priority".

Current scheduler implementation
To find the non-empty ready queue with the maximum priority for the current domain,
seL4 iterates through `ksReadyQueues`, starting with the element
corresponding to the current domain and maximum possible priority, and
decrementing the priority until a non-empty queue is found. This is
problematic in cases where the only ready threads have low priorities,
as iterating through many elements of an array effectively flushes the
cache.

Changes in this patch
This patch replaces the iteration with a lookup into a table of
bitfields per domain. Using bitfields allows the kernel to determine the
highest priority level with a non-empty ready queue for the current
domain by counting the leading zeroes in bitfields. This removes the
negative cache effects of iterating through an array.

Implementation details
For each domain, a multilevel table of bitfields is maintained which
stores the priority levels within that domain for which there exist
ready threads. On a 32-bit architecture, the top level of the table is a 32-bit bitfield where if
the ith bit is set, there is at least 1 priority level in
[i*32..i*32+31] with a non-empty ready queue. The positions of bits in
this bitfield are used as indices into the second level table, which is
an array of 32-bit bitfields. The ith bit of the jth bitfield in this
array set to 1, indicates that priority level j*32+i has a non-empty
ready queue.
2015-10-21 18:52:44 +11:00
Anna Lyons
d9802d179f Add seL4_NBWait: non blocking wait for notifications and endpoints. 2015-10-21 13:43:39 +11:00
Adrian Danis
97042a0f07 Introduce 'Notification Binding': a new feature which allows a tcb to be bound to a single asynchronous endpoint. 2015-10-09 15:19:58 +11:00
TrusthworthySystems
91b7da8625 Release snapshot 2014-07-18 05:03:59 +10:00