Commit graph

57 commits

Author SHA1 Message Date
Joel Beeren
d7cf973002 Refactor sanitiseRegister to take a bool rather than a (tcb_t *).
This involves adding a function to determine if a tcb has a vcpu, and
makes verification a lot easier for arm-hyp.
2017-04-27 15:50:22 +10:00
Adrian Danis
0abc720277 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
2017-04-06 10:43:24 +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
Adrian Danis
ccd9020b6a Pass tcb_t to sanitiseRegister instead of arch_tcb_t 2017-03-06 13:42:33 +11:00
Kent McLeod
aa656604db Modify FinalizeLog syscall
There is no way to know how many entries the syscall log contains
otherwise.  One option was iterating through until finding a 0
terminator, however this requires the log to be zeroed before each
trial.  This changes the FinalizeLog syscall to return the number of
entries.
2017-02-24 15:55:34 +11:00
Adrian Danis
eccaae51dc s/D61/DATA61/ in license headers for consistency 2017-02-21 16:38:51 +11:00
Jack Suann
50995b4c5f Replace Arch_handleInterrupt with Arch_finaliseInterrupt 2017-02-16 12:51:14 +11:00
Jack Suann
9f67d21c3d x86: Handle pending interrupt before scheduling thread in handleSyscall
In handleSyscall the current thread may be preempted to handle a pending interrupt.
With kernel mode interrupts in x86 this handling was delayed until we were about
to switch back to user mode. This change unifies the handling with ARM, where the
interrupt is handled prior to calling the thread scheduler.
2017-02-15 14:31:55 +11:00
Adrian Danis
f709e49481 arm: SELFOUR-781: Only allow threads with VCPU to run outside user mode
Previously any thread could be set to run in any mode (except HYP mode).
Whilst this causes no security issues for the kernel, different execution
modes in ARM have different banked registers. These registers are not
currently saved and restored allowing for threads to manipulate registers
that will be seen (or potentially are being actively used) by other threads.

Saving and restoring these banked registers for all threads is a performance
cost (even if only done for the actual mode the thread runs in) for no real
benefit, as there is no clear reason to run a thread in other modes if you
do not have a vcpu. Therefore this commit restricts being in modes other than
user to threads that have a vcpu. When multiple VCPUs are properly supported
the switching of VCPUs will then save/restore these banked registers.
2017-01-30 09:47:51 +11:00
Kofi Doku Atuah
6eb2ea50f1 Add userError messages 2016-11-30 09:31:33 +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
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
Anna Lyons
33a771d3cb Split fault types into arch/generic
Prior to this commit faults were separate
per architecture. This commit extracts the common
fault types and introduces arch specific faults,
reducing code duplication across architectures.
2016-11-25 12:29:07 +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
Anna Lyons
f0cb354755 Merge pull request #410 in SEL4/sel4 from ~ALYONS/sel4:cache to master
* commit '44ed6adb616590a0f6ae8b0ad8c442afed625457':
  add seL4_BenchmarkFlushCaches() for arm and ia32
2016-10-28 04:21:25 +00:00
Anna Lyons
44ed6adb61 add seL4_BenchmarkFlushCaches() for arm and ia32
Available when CONFIG_ENABLE_BENCHMARKS is set, flushes caches for
running cold-cache benchmarks
2016-10-28 15:09:03 +11:00
Hesham Almatary
5f7fa2fcc8 Benchmark: Pack arch-independent benchmark-related files into separate directories 2016-10-20 11:42:04 +11:00
amrzar
3f9eb7c873 SELFOUR-632: implement cores non-architecture dependent structres 2016-10-10 16:33:48 +11:00
Hesham Almatary
9c507cffd1 SELFOUR-603 - Benchmark: Add null syscall 2016-09-28 11:05:25 +10:00
Adrian Danis
5fbcda43c5 SELFOUR-538: Avoid out of bounds read in debug mode 2016-09-22 12:16:07 +10:00
Hesham Almatary
8808ba7fa0 Benchmark: Implement per-thread reset syscall 2016-09-12 13:54:12 +10:00
Anna Lyons
ef00e98689 SELFOUR-615: arm entry point stubs 2016-08-24 10:42:36 +10:00
Adrian Danis
4c57e6e577 define arch entry hooks instead 2016-08-24 10:42:36 +10:00
Adrian Danis
a217102b4e Consolidate benchmark entry/exit
Move the benchmark pre/post ambles into the now existing entry/exit
hook functions
2016-08-24 10:42:36 +10:00
Adrian Danis
3c05b79a6e Provide generic C entry/exit hook routines
It can be deseriable to run code before/after user mode, but
not have to write it in assembly. This commit adds such stubs
that get called as the first/last C code when coming in
and out of the kernel
2016-08-24 10:42:36 +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
Hesham Almatary
c3826e0efe SELFOUR-518: Benchmark - User-level log buffer, delete dump and size system calls
Given that the log buffer is now
(79291252a8) in user-level, the kernel doesn't have
to dump and send the size for users. Users have to take care of this.
2016-08-19 12:57:03 +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
ce2c058f3d SELFOUR-607: inline remaining irq path functions 2016-08-09 16:18:34 +10:00
Anna Lyons
8d8cdba302 trivial: fix bbone build 2016-08-05 17:08:21 +10:00
Hesham Almatary
c6247d36a3 SELFOUR-526: Refactor benchmark/debug syscall kernel entry 2016-07-28 10:29:42 +10:00
Hesham Almatary
d97603bd84 SELFOUR-566: Decouble seL4_DebugNameThread from CONFIG_PRINTING 2016-07-15 12:30:17 +10:00
Hesham Almatary
09358f9b6a SELFOUR-448 Benchmark: Track thread's CPU utilisation time 2016-06-24 12:43:09 +10:00
Anna Lyons
fb98d91ec9 trivial: fix warning when benchmarks enabled 2016-06-15 15:41:02 +10:00
Hesham Almatary
0b1456d739 Benchmark: include scheduler time 2016-06-08 11:55:46 +10:00
Hesham Almatary
95909cd8bc Default MAX_NUM_TRACE_POINTS to 0 for compatibility
Some libraries and apps assume MAX_NUM_TRACE_POINTS = 0
if benchmarks are disabled.
2016-06-02 12:29:16 +10:00
Hesham Almatary
bcf0a235b1 SELFOUR-446 Unify code base for trace points and track feature 2016-06-02 10:49:25 +10:00
Hesham Almatary
7cbaeb8ed0 SELFOUR-446 Benchmark: Track interrupts and user/vm faults 2016-05-31 08:54:57 +10:00
Hesham Almatary
fc1feb670e 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.
2016-05-25 13:47:49 +10:00
Adrian Danis
1287590e97 Correct separation of printing and debug builds
Fixes some build issues with 541289a326
as well as further allowing debugging (via the capdl interface) to
happen when printing is turned off.
2016-05-17 15:10:08 +10:00
Adrian Danis
bbb841325a Merge pull request #18 in SEL4/sel4 from ~MFERNANDEZ/sel4:b9822ce6-bd06-46ac-bb43-010e3478ba1f to master
* commit '59ec7c9a738266ef8cc4f119cebbf6bf6b8d2a62':
  Fix: Make settings actually take effect on spurious interrupt reporting.
2016-01-11 03:26:52 +00:00
Anna Lyons
d93699c9a3 SELFOUR-114: remove duplication of seL4_MessageInfo_t, adjust naming to avoid cparser mangling 2016-01-11 11:16:08 +11:00
Matthew Fernandez
59ec7c9a73 Fix: Make settings actually take effect on spurious interrupt reporting.
The `IRQ_REPORTING` configuration variable is documented to affect whether
undelivered and spurious interrupts are reported, but it previously only
affected whether undelivered IRQs were reported. Spurious interrupts were
always reported leading to needless UART spam when you were not debugging an
interrupt issue.
2015-12-16 12:31:59 +11:00
Anna Lyons
a0e5db7a2a Add debug functionality to print the kernel entry reason and arguments at any point in the kernel 2015-12-15 12:01:18 +11:00
Adrian Danis
171824f7b7 Change additional int->word_t due to interraction with the C parser to ease verification 2015-12-10 10:45:22 +11:00
Adrian Danis
2d61910e0f Rename uint32_t -> word_t in any relevant places 2015-12-10 10:45:20 +11:00
Adrian Danis
fee26a8816 Change casting from int->long to be compatible with both 32 and 64 bit compilations 2015-12-10 10:45:18 +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
Anna Lyons
54603123e6 SELFOUR-317: rename async endpoint to notification object, and other
fallout.
2015-11-09 17:18:43 +11:00
Anna Lyons
d9802d179f Add seL4_NBWait: non blocking wait for notifications and endpoints. 2015-10-21 13:43:39 +11:00