38 |
} |
} |
39 |
|
|
40 |
|
|
41 |
/* Start kernel by simply jumping to the entry point. */ |
/* Start kernel. */ |
42 |
void |
void |
43 |
start_kernel (l4_word_t ip) |
start_kernel (l4_word_t ip) |
44 |
{ |
{ |
45 |
|
/* Flush the data cache, so that the kernel code instructions can be |
46 |
|
found. Actually, ia32 does this automatically for backwards |
47 |
|
compatibility, but other architectures may not. If you are |
48 |
|
porting this file, make sure that the instruction fetcher gets to |
49 |
|
see the loaded kernel code. */ |
50 |
|
asm volatile ("wbinvd"); |
51 |
|
|
52 |
|
/* Jump to the entry point. */ |
53 |
(*(void (*) (void)) ip) (); |
(*(void (*) (void)) ip) (); |
54 |
} |
} |
55 |
|
|