seL4/include
Jack Suann cea45cd1bd x86: Handling pending interrupts in kernel mode
This commit allows x86 to completely handle a pending interrupt without switching
out to user mode. To handle an interrupt on x86 the APIC *must* generate an exception,
prior to you being able to acknowledge it. Previously we only allow exceptions (i.e.
interrupts) to be generated outside of kernel mode when we are in user mode.

This change allows us to 'poll' for an interrupt and transition the APIC whilst in kernel
mode by enabling and taking interrupts at carefully defined points. A pending interrupt
will be stored by the exception handler, allowing us to then handle the interrupt and
acknowledge the hardware APIC. Handling is done by waiting until after we have 'left' the
kernel and are about to switch to user mode and then 'entering' the kernel again by jumping
to the interrupt entry point.

Handling interrupts entirely in kernel mode provides two advantages
 * It will allow, in the future, the ability to handle kernel interrupts in situations
   where we need to handle the interrupt before actually performing the hardware switch
   back to user mode. This case happens where the user thread is using vt-x and so
   pending interrupts do not generate an interrupt exception, but rather cause an exception
   to be generated telling the system that there is a pending interrupt
 * Where there are multiple pending interrupts it is more efficient to avoid additional
   switches in and out of the user thread

Whilst this change does not enable pre-emption points to handle the interrupt before
returning out of `handleSyscall` it should be easily implementable with what is provided.
2017-02-01 12:44:14 +11:00
..
32/mode SELFOUR-413: refactor libsel4 fault API 2016-11-25 12:29:07 +11:00
64/mode SELFOUR-413: refactor libsel4 fault API 2016-11-25 12:29:07 +11:00
api SELFOUR-567: use seL4_CapRights_t from libsel4 2016-11-25 12:29:07 +11:00
arch x86: Handling pending interrupts in kernel mode 2017-02-01 12:44:14 +11:00
benchmark Benchmark: Define benchmark_util_t in a separate file to avoid circular dependency 2017-01-11 14:19:34 +11:00
fastpath x64: Rearrange cnode_cap structure to improve fastpath speed 2017-01-10 16:57:57 +11:00
kernel Merge pull request #607 in SEL4/sel4 from ~HALMATARY/sel4:KernelStacks to master 2017-01-18 12:43:34 +11:00
machine Remove many MODIFIES annotations. 2016-12-12 17:30:51 +11:00
model SMP: Abstract architecture/platform independent parts of smp.h and ipi.h 2017-01-13 15:35:41 +11:00
object x64: Allow full 48bits of virtual address space to be used 2017-01-27 12:21:07 +11:00
plat x86: Handling pending interrupts in kernel mode 2017-02-01 12:44:14 +11:00
smp [STYLE_FIX] 2017-01-16 22:32:08 +00:00
api.h
assert.h Always have compile_assert enabled 2015-11-11 11:09:24 +11:00
basic_types.h Rename uint32_t -> word_t in any relevant places 2015-12-10 10:45:20 +11:00
bootinfo.h SELFOUR-114: remove bootinfo.h duplication 2016-03-01 17:25:22 +11:00
compound_types.h unsigned int -> word_t 2015-12-10 10:45:21 +11:00
config.h SELFOUR-444: Preemptible zeroing for retype. 2016-11-01 17:05:36 +11:00
machine.h SELFOUR-607: inline remaining irq path functions 2016-08-09 16:18:34 +10:00
Makefile SELFOUR-413: refactor libsel4 fault API 2016-11-25 12:29:07 +11:00
object.h SELFOUR-317: rename async endpoint to notification object, and other 2015-11-09 17:18:43 +11:00
stdarg.h
stdint.h conversion: fixed unnecessary word_t change 2015-12-10 10:45:22 +11:00
string.h Correct separation of printing and debug builds 2016-05-17 15:10:08 +10:00
types.h ia32: added the option to disable prefetchers 2015-04-15 14:38:55 +10:00
util.h Mark halt as no-inline and no-return. 2016-12-12 17:30:50 +11:00