Commit graph

31 commits

Author SHA1 Message Date
Anna Lyons
a38e62f2f9 mcs: timeout exceptions
- Add seL4_TCB_SetTimeoutEndpoint
- implement timeout exceptions
2019-08-22 11:22:38 +10:00
Anna Lyons
554f812da3 mcs: scheduling context donation over ipc
After this commit, threads blocked on an endpoint can recieve a
scheduling context from the thread that wakes the blocked thread.
2019-08-22 11:22:37 +10:00
Anna Lyons
7124449936 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.
2019-08-22 11:22:34 +10:00
Anna Lyons
9dcb470631 arm: remove plat/machine/timer.h
plat/machine/timer.h is unused on arm, so remove it and fix up the
includes.
2019-06-17 10:44:36 +10:00
Oliver Scott
ea365a8553 capdl-dump: tcbDebug list, multicore-support, add tcb command
-Use debuglist for runqueues and filter idle and root thread.
-Refactor sendEPQueue.
-Add multicore support.
-Added TCB_COMMAND, kernel now does translation
depending on how it's configured.
2019-03-20 12:55:30 +11:00
Anna Lyons
d0930f67de style: consistently attach return type
Add attach-return-type to astyle
2019-03-19 14:05:36 +11:00
Anna Lyons
7b019e3def serial: remove putConsoleChar
putConsoleChar was needless indirection around putDebugChar. Remove
this.
2019-03-14 14:31:12 +11:00
Anna Lyons
cddc4e6ef5 Inline resetTimer for all platforms
- for arm generic timer platforms, we remove resetTimer ->
resetGenericTimer indirection and simply include generic_timer.h
- this reduces boiler plate for platforms that share timer drivers, as
  they simply include the one header
- there is far more timer code in the RT kernel, which motivates this
change
2017-11-28 10:21:46 +11:00
Anna Lyons
2f7d3bb9b0 Move definition of initTimer to be arm specific
initTimer does not exist on x86
2017-11-28 10:21:46 +11:00
Anna Lyons
40c61e5c18 Fix licenses (the rest) 2017-06-22 15:29:12 +10:00
Kofi Doku Atuah
3f90fad605 SELFOUR-836: Hardware debug API functions should take tcb_t and not arch_tcb_t
Touches files all throughout x86 (32 and 64) and ARM.
2017-04-03 14:14:00 +10:00
Bamboo
4d54476621 [STYLE_FIX] 2017-02-27 06:26:58 +00:00
amrzar
0707ae874b Move arch independent functions to generic files and HAVE_FPU config 2017-02-27 12:52:18 +11:00
Adrian Danis
eccaae51dc s/D61/DATA61/ in license headers for consistency 2017-02-21 16:38:51 +11:00
Thomas Sewell
97bac2345f Remove many MODIFIES annotations.
These are redundant for any function which the C-to-Isabelle parser
actually analyses, which is now the vast majority of functions.
2016-12-12 17:30:51 +11:00
Anna Lyons
ed95f84a43 SELFOUR-413: changes for verification
Avoid using ptrs to arrays at all

Another macrofull change brought to your by verification. This should
avoid nasty proofs about const pointers.
2016-11-25 12:30:29 +11:00
Adrian Danis
b90238d089 Replace #pragma once with include guards 2016-10-21 12:05:02 +11:00
Bamboo
77c4954a00 [STYLE_FIX] 2016-10-10 03:11:19 +00:00
Kofi Doku Atuah
bebfcf6d27 SELFOUR-499: X86, ARM: Add userspace invocations for hardware debugging
This commit implements the body of SELFOUR-499. The API exposes the x86 DR0-7
and ARM coprocessor 14 features to userspace by virtualizing them as context-
switched registers in the TCB. Implemented as TCB invocations. This feature is
only built when CONFIG_HARDWARE_DEBUG_API is selected.

* Add low-level support routines for setting, unsetting, getting, enabling
  and disabling breakpoints.
* Add support for single-stepping as well.
  ^ Single-stepping is not supported on ARMv6 since the hardware
    doesn't have support.
  ^ ARM implements single-stepping as instruction breakpoints
    configured to fault on every instruction -- this is achieved through
    the "mismatch" mode, which is only supported from ARMv7 onwards.
* Also support explicit software break requests, a la "BKPT" and "INT $3".

* New invocations:
  * seL4_TCB_SetBreakpoint().
  * seL4_TCB_GetBreakpoint().
  * seL4_TCB_UnsetBreakpoint().
  * seL4_TCB_ConfigureSingleStepping().
* New constants:
  ^ Event types:
    ^ seL4_InstructionBreakpoint.
    ^ seL4_DataBreakpoint.
    ^ seL4_SoftwareBreakRequest.
  ^ Access types:
    ^ seL4_BreakOnRead.
    ^ seL4_BreakOnWrite.
    ^ seL4_BreakOnReadWrite.
  ^ Exports:
    ^ seL4_NumHWBreakpoints.
    ^ seL4_NumExclusiveBreakpoints.
    ^ seL4_NumExclusiveWatchpoints.
    ^ seL4_NumDualFunctionMonitors.
    ^ seL4_FirstBreakpoint.
    ^ seL4_FirstWatchpoint.
    ^ seL4_FirstDualFunctionMonitor.

See documentation in the seL4 API manual.
2016-10-10 13:53:21 +11:00
Anna Lyons
ada2fc5f14 SELFOUR-624: fix ia32 debug build
- separate putDebugChar and putConsoleChar
- this only has effect on x86 where 2 serial ports are initialised by
  the kernel
- for arm, putConsoleChar just calls putDebugChar
2016-08-24 11:10:12 +10:00
Anna Lyons
49510f9df4 SELFOUR-624: remove redundancy in io.[c|h]
And clean up a bit while we are there
2016-08-23 08:00:47 +10:00
Anna Lyons
ce2c058f3d SELFOUR-607: inline remaining irq path functions 2016-08-09 16:18:34 +10:00
Rafal Kolanski
e105053581 Update prototype of maskInterrupt to match implementations.
The prototype will ultimately be removed, but the mismatch is presently
breaking verification.
2016-08-05 16:42:04 +10:00
Anna Lyons
c5b6a6a58a Refactor duplicated code in hardware.h
One copy to rule them all.
2016-06-07 12:01:14 +10:00
Anna Lyons
c9684b964f trivial: consolidate timer function declarations
This moves all timer function declarations to a single
header instead of duplication them for each platform
2016-06-07 11:50:11 +10:00
Adrian Danis
541289a326 Further separate 'release' and 'verification' builds
Originally building the kernel was largely considered to be done in
one of two ways
1. Release build with no assertions, no debug symbols and no printing.
   This was generally considered to be a 'verified' build
2. Debug build with assertions, debug symbols and printing

Since then various options were added, such as the 'code injection'
option, which we wanted on builds that did not have assertions or
other options that affected performance. As such it did not depend
upon a debug build and had large warning signs saying that enabling
this in a release build would not give you a verified or trusted
kernel.

Most recently the ability to print from the kernel in release mode
was added. For the same reason that tying the ability to print with
the performance reduction of various debugging was not always desireable.

This change attempts to unify the current state and have a single top
level option to enable a 'verification friendly' build. All other
options (assertions, printing, code injection) then depend upon
this configuration not being set.
2016-05-17 10:51:55 +10:00
Adrian Danis
0ecff9f393 unsigned int -> word_t 2015-12-10 10:45:21 +11:00
Anna Lyons
88d73db06c refactor tcb_t to remove duplication between x86 and arm header files 2015-11-09 17:18:43 +11:00
Anna Lyons
07a7f4c42e generate warnings for incorrect format strings for kprintf, bring stdint.h
inline for x86 and arm and fix some format strings as a consequence
2015-09-30 12:31:39 +10:00
Anna Lyons
ec78890001 xIntroduce RELEASE_PRINTF, which allows a renamed printf (release_printf) to be used in a release build of the kernel - userful for debugging tests that only fail on a release build of the kernel 2015-08-03 10:26:41 +10:00
TrusthworthySystems
91b7da8625 Release snapshot 2014-07-18 05:03:59 +10:00