History log of /seL4-l4v-master/seL4/src/model/statedata.c
Revision Date Author Comments
# a00c2c16 17-Sep-2020 Curtis Millar <curtis.millar@data61.csiro.au>

Make kernel log buffer derived from cmake config

This removes the explicit CMake configuration for the kernel log buffer
and replaces it with a #define that is enabled for the required
configurations.

Signed-off-by: Curtis Millar <curtis@curtism.me>


# 88a7d138 13-Jul-2020 Kent McLeod <Kent.Mcleod@data61.csiro.au>

KernelBenchmarksTrackUtilisation: Add more stats

For each thread also track number of times scheduled, number of kernel
entries and amount of cycles spent inside the kernel. Also add
core-wide totals for each.

Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>


# 4eccea54 13-Jul-2020 Kent McLeod <Kent.Mcleod@data61.csiro.au>

KernelBenchmarksTrackUtilisation: Fix for SMP

Create per-node global definitions for utilization variables.
This enables the tracking to more cleanly work on SMP configurations.
As resetting and starting the counters via SysBenchmarkResetLog only
updates the counters of the current thread and idle thread on the
current node it was not possible to accurately record utilization
statistics across multiple nodes. Now each node can have its tracking
independently started, stopped and queried. It is possible to add
additional syscalls in the future for doing this for all nodes in a
single syscall.

Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>


# 79da0792 01-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

Convert license tags to SPDX identifiers

This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.


# 0de7fc11 18-Dec-2019 Kent McLeod <Kent.Mcleod@data61.csiro.au>

Revert "Cache FPU enable state on all platforms"

This reverts commit 186180cf309b365b45c162f7a1f5931f0fc05d7c.


# 186180cf 11-Jul-2019 Curtis Millar <curtis.millar@data61.csiro.au>

Cache FPU enable state on all platforms

This change broadens the caching of the FPU enable/disable bit from arm
to all platforms to ensure that on x86 time is not wasted on the
fastpath disabling or enabling an already disabled/enabled FPU.


# 04e51d40 27-Nov-2019 Curtis Millar <curtis.millar@data61.csiro.au>

Revert the recent changes to Faster FPU switch

These changes need to be reverted until we can properly test the changes
with all of our hardware online (currently we cannot test on x86
hardware).

This reverts commit a0aeec3b304d16909619bc847197df221c73a0c4.
This reverts commit af0fdc82c23f1e7e3f1e568f6987f5afd0d2150a.
This reverts commit a190a14ecaae688a6b40dd0a699b8f49c2c0631e.


# e9b90f9f 11-Jul-2019 Curtis Millar <curtis.millar@data61.csiro.au>

Cache FPU enable state on all platforms

This change broadens the caching of the FPU enable/disable bit from arm
to all platforms to ensure that on x86 time is not wasted on the
fastpath disabling or enabling an already disabled/enabled FPU.


# 106b893e 23-May-2017 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: configurable scheduling context size

This allows users to define custom amounts of refills without
increasing the scheduling context size system wide.

also add libsel4 functions for refill size


# 34c1f920 03-Nov-2016 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: add periodic scheduling

This commit adds periodic scheduling with sporadic servers.


# 71244499 31-Oct-2016 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: tickless scheduler implementation

This changes the budget/remaining fields in scheduling contexts
to contain timer ticks, not number of abstract sel4ticks.

seL4_SchedControl_Configure now takes microseconds, not ticks.

This commit is plat-independant - the platform and arch specific
timer code follows in later commits.


# 952134d1 27-Oct-2016 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: Add a scheduling context object

This is the first part of the seL4 MCS. This commit:

* adds a scheduling context object. Threads without scheduling
context objects cannot be scheduled.
* replaces tcbTimeSlice with the scheduling context object
* adds seL4_SchedControl caps for each core
* adds seL4_SchedControl_Configure which allows users to configure
amount of ticks a scheduling context has, and set a core for the
scheduling context.
* adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
a tcb to be bound to a scheduling context.


# a6157d5d 18-Jul-2019 Sylvain Gauthier <sylvain.gauthier@data61.csiro.au>

[SMP] Abstracted IRQ indexing to handle PPIs

irq_t is now a "virtual" interrupt type that encapsulates the
information of the core in case of a private interrupt. There is a
couple of macros that need to be defined on the interrupt controller
level to translate between virtual and hardware IRQs.


# 69339d42 09-Apr-2019 Jasper Lowell <jasper.lowell@data61.csiro.au>

Boot code: Statically allocate idle thread

The idle thread is not managed at user-level and so it can instead be
statically allocated. This simplifies the boot code and increments
towards being easier to formally verify.


# 1c6c06dc 23-Apr-2019 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

boot: implement intStateIRQNode as an array

It turns out that verifying this is easier than if intStateIRQNode is a
pointer that is statically initialised to point to another array.


# bbbd7a14 23-Apr-2019 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

trivial: tighten assertion on IRQ CNode size


# a6b4cf73 09-Apr-2019 Anna Lyons <Anna.Lyons@data61.csiro.au>

boot: allocate irq cnode statically

The memory used for the irq cnode is never available to the user. As a
result this memory can be allocated statically, simplifying the
bootcode.

- remove allocation of irq cnode
- add static init
- generate irq cnode size from cmake for arm
- add static constants for riscv, x86 as there is no variability at the
moment.


# c6e4cc3e 23-Nov-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

Correct L2 bitmap size calculation and put it in one place

This corrects the calculation of the L2 bitmap size to correctly handle cases where the
requested num priorities is not a clean multiple of the wordBits


# bb5ecb1b 29-May-2017 Anna Lyons <Anna.Lyons@data61.csiro.au>

SELFOUR-880: add seL4_DebugDumpScheduler

- when CONFIG_DEBUG is enabled, track all threads
- when CONFIG_PRINTING is enabled, provide seL4_DebugDumpScheduler which
allows the user to dump the state of the kernel scheduler.


# 0abc7202 04-Apr-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

s/DEBUG/CONFIG_DEBUG_BUILD/

DEBUG definition is not supposed to be used in the kernel, rather CONFIG_DEBUG_BUILD,
which can be toggled separately to user notion of DEBUG


# 0707ae87 23-Feb-2017 amrzar <azarrabi@nicta.com.au>

Move arch independent functions to generic files and HAVE_FPU config


# ae8f2c99 23-Feb-2017 amrzar <azarrabi@nicta.com.au>

x86: move current active FPU owner to node state


# 323e60a7 23-Feb-2017 amrzar <azarrabi@nicta.com.au>

x86: define number of restore since switch as node state


# 0ef7c693 14-Feb-2017 Hesham Almatary <hesham.almatary@data61.csiro.au>

x86: define L1_CACHE_LINE_SIZE_BITS as with ARM


# 48d17e1f 16-Jan-2017 Hesham Almatary <hesham.almatary@data61.csiro.au>

ARM/SMP: Prepare for ARM SMP adding stubs

Currently building ARM/SMP is broken. This commit:
1- Makes it possible to build ARM/SMP with stubs. Run-time SMP for ARM
DOES NOT WORK.
2- Can be a reference for future SMP targets to follow in order to
layout/add the minimal required files and functions needed to support SMP.
3- Builds for Sabre only. In order to support other platforms, ipi
interrupt ID should be defined in machine.h


# 7f767494 15-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

Revert SELFOUR-242

This reverts commits
3aee0ab7b3ae5ff5294192526fb00823b49048b5
6b6b965528d16c1e4c946fb920fb95060f84424f
a1421832acd19ed5ede71640af82b982708207c2


# a1421832 15-Feb-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

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


# 5f7fa2fc 19-Oct-2016 Hesham Almatary <hesham.almatary@data61.csiro.au>

Benchmark: Pack arch-independent benchmark-related files into separate directories


# 3f9eb7c8 06-Oct-2016 amrzar <azarrabi@nicta.com.au>

SELFOUR-632: implement cores non-architecture dependent structres


# 2cbc7123 28-Sep-2016 amrzar <azarrabi@nicta.com.au>

SELFOUR-630:preliminary booting application processors
- update core detection code and Kconfig file
- update kernel stack managment so that BSP does not use boot stack before IPI APs
- move arch dependant data to a single structure
- add cache line size to Kconfig
- add cpu indexing and apic id mapping
- boot APs to halting state
- add guard for kernel stack if there is only one core


# 4044e204 21-Sep-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

Revert "Merge pull request #358 in SEL4/sel4 from ~AZARRABI/sel4:multicore to master"

This reverts commit ce2f666bb811c5e4c779829fcb09d5a189ebcdbb, reversing
changes made to dc183f96b81f2344d7d0d910fc430f924eaae940.


# fbc071b4 12-Sep-2016 amrzar <azarrabi@nicta.com.au>

SELFOUR-630:preliminary booting application processors
- update core detection code and Kconfig file
- update kernel stack managment so that BSP does not use boot stack before IPI APs
- move arch dependant data to a single structure
- add cache line size to Kconfig
- add cpu indexing and apic id mapping
- boot APs to halting state
- add guard for kernel stack if there is only one core


# 16c34811 31-Jul-2016 Hesham Almatary <hesham.almatary@data61.csiro.au>

SELFOUR-518: User-level log buffer

Remove global ksLog and use KS_LOG_PPTR instead

Benchmark - Log buffer: use global page table


# bcf0a235 01-Jun-2016 Hesham Almatary <Hesham.Almatary@nicta.com.au>

SELFOUR-446 Unify code base for trace points and track feature


# 7cbaeb8e 30-May-2016 Hesham Almatary <Hesham.Almatary@nicta.com.au>

SELFOUR-446 Benchmark: Track interrupts and user/vm faults


# fc1feb67 24-May-2016 Hesham Almatary <Hesham.Almatary@nicta.com.au>

SELFOUR-446 Benchmark: Track syscall feature

Benchmark feature that currently:
- Keeps track of system calls info
- Start time
- Duration
- Capability type
- Invocation tag
- Log the number of invocations of each system call*
- Log the number of invocations for each capability type per syscall.
- Has 3 new syscalls (dump, reset, get size).
- This new feature uses the existing log buffer (which is 1MiB for x86
and ARM). Since the number of syscall invocations is not
deterministic, the logged number of invocations is limited by the size
of the buffer. I suggested to enable the users to pass their own
user-level buffer, to enable more flexibility, later.
- ENABLE_BENCHMARKS is now a parent config option of trace points and
system call track features, they can't be used at the same time.


# b9a7f3c9 05-May-2016 Felix Kam <felix.kam@nicta.com.au>

Make lockTLBEntry comply with the decompiler

lockTLBEntry, an assembly function, had tlb_lock_count as a symbol that
needed to be placed sufficiently close to be loaded and stored with
offset-from-pc addressing. When assembled, the symbol would turn up
between functions, as opposed to within a literal pool (it's a variable,
not a constant) or the .bss / data sections. The decompiler doesn't
handle that use case, and likely won't. This change turns
tlb_lock_count into a C global variable (so that it will be placed in
the .bss / data sections), and splits lockTLBEntry into two parts so the
critical section will still fit in a 64-byte aligned region, and
therefore be guaranteed to live within a single page.


# a0e5db7a 14-Dec-2015 Anna Lyons <Anna.Lyons@nicta.com.au>

Add debug functionality to print the kernel entry reason and arguments at any point in the kernel


# 2d61910e 09-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

Rename uint32_t -> word_t in any relevant places


# 62727e30 15-Jun-2015 Stephen Sherratt <stephen.sherratt@nicta.com.au>

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.


# 91b7da86 17-Jul-2014 TrusthworthySystems <gatekeeper@sel4.systems>

Release snapshot