114 |
/* The maximum number of fpages required to cover a page aligned range |
/* The maximum number of fpages required to cover a page aligned range |
115 |
of memory. This is k if the maximum memory range size to cover is |
of memory. This is k if the maximum memory range size to cover is |
116 |
2^(k + min_page_size_log2), which can be easily proved by |
2^(k + min_page_size_log2), which can be easily proved by |
117 |
induction. The minimum page size in L4 is at least 2^10. */ |
induction. The minimum page size in L4 is at least 2^10. We also |
118 |
|
need to have each fpage aligned to a multiple of its own size. |
119 |
|
This makes the proof by induction a bit more convoluted, but does |
120 |
|
not change the result. */ |
121 |
#define MAX_FPAGES (sizeof (l4_word_t) * 8 - 10) |
#define MAX_FPAGES (sizeof (l4_word_t) * 8 - 10) |
122 |
|
|
123 |
|
|
124 |
|
/* Find the first bit set. The least significant bit is 1. If no bit |
125 |
|
is set, return 0. FIXME: This can be optimized a lot, in an |
126 |
|
archtecture dependent way. Add to libl4, like __l4_msb(). */ |
127 |
|
static inline unsigned int |
128 |
|
wffs (l4_word_t nr) |
129 |
|
{ |
130 |
|
unsigned int bit = 0; |
131 |
|
|
132 |
|
while (bit < sizeof (l4_word_t) * 8) |
133 |
|
{ |
134 |
|
if ((1ULL << bit) & nr) |
135 |
|
{ |
136 |
|
return bit + 1; |
137 |
|
} |
138 |
|
bit++; |
139 |
|
} |
140 |
|
} |
141 |
|
|
142 |
|
|
143 |
/* Determine the fpages required to cover the bytes from START to END |
/* Determine the fpages required to cover the bytes from START to END |
144 |
(exclusive). START must be aligned to the minimal page size |
(exclusive). START must be aligned to the minimal page size |
145 |
supported by the system. Returns the number of fpages required to |
supported by the system. Returns the number of fpages required to |
146 |
cover the range, and returns that many fpages (with maximum |
cover the range, and returns that many fpages (with maximum |
147 |
accessibility) in FPAGES. At most MAX_FPAGES fpages will be |
accessibility) in FPAGES. At most MAX_FPAGES fpages will be |
148 |
returned. */ |
returned. Each fpage will also be aligned to a multiple of its own |
149 |
|
size. */ |
150 |
static unsigned int |
static unsigned int |
151 |
make_fpages (l4_word_t start, l4_word_t end, l4_fpage_t *fpages) |
make_fpages (l4_word_t start, l4_word_t end, l4_fpage_t *fpages) |
152 |
{ |
{ |
164 |
nr_fpages = 0; |
nr_fpages = 0; |
165 |
while (start < end) |
while (start < end) |
166 |
{ |
{ |
167 |
fpages[nr_fpages] = l4_fpage_add_rights (l4_fpage (start, end - start), |
/* Each fpage must be self-aligned. */ |
168 |
l4_fully_accessible); |
unsigned int fpsize_log2 = wffs (start | (end - start)) - 1; |
169 |
|
|
170 |
|
fpages[nr_fpages] |
171 |
|
= l4_fpage_add_rights (l4_fpage_log2 (start, fpsize_log2), |
172 |
|
l4_fully_accessible); |
173 |
start += l4_size (fpages[nr_fpages]); |
start += l4_size (fpages[nr_fpages]); |
174 |
nr_fpages++; |
nr_fpages++; |
175 |
} |
} |
291 |
This can also be used to actually create these threads up |
This can also be used to actually create these threads up |
292 |
front. */ |
front. */ |
293 |
ret = l4_thread_control (physmem_server, physmem_server, l4_myself (), |
ret = l4_thread_control (physmem_server, physmem_server, l4_myself (), |
294 |
l4_nilthread, (void *) 0x2000000); |
l4_nilthread, (void *) -1); |
295 |
if (!ret) |
if (!ret) |
296 |
panic ("Creation of initial physmem thread failed"); |
panic ("Creation of initial physmem thread failed"); |
297 |
|
|
298 |
/* The UTCB area must be controllable in some way, see above. Same |
/* The UTCB area must be controllable in some way, see above. Same |
299 |
for KIP area. */ |
for KIP area. */ |
300 |
ret = l4_space_control (physmem_server, 0, |
ret = l4_space_control (physmem_server, 0, |
301 |
l4_fpage_log2 (0x2400000, l4_kip_area_size_log2 ()), |
l4_fpage_log2 (wortel_start, |
302 |
l4_fpage_log2 (0x2000000, 14), |
l4_kip_area_size_log2 ()), |
303 |
|
l4_fpage_log2 (wortel_start + l4_kip_area_size (), |
304 |
|
l4_utcb_area_size_log2 ()), |
305 |
l4_anythread, &control); |
l4_anythread, &control); |
306 |
if (!ret) |
if (!ret) |
307 |
panic ("Creation of physmem address space failed"); |
panic ("Creation of physmem address space failed"); |
308 |
|
|
309 |
ret = l4_thread_control (physmem_server, physmem_server, l4_nilthread, |
ret = l4_thread_control (physmem_server, physmem_server, l4_nilthread, |
310 |
l4_myself (), (void *) -1); |
l4_myself (), |
311 |
|
(void *) (wortel_start + l4_kip_area_size ())); |
312 |
if (!ret) |
if (!ret) |
313 |
panic ("Activation of initial physmem thread failed"); |
panic ("Activation of initial physmem thread failed"); |
314 |
|
|
475 |
l4_msg_load (&msg); |
l4_msg_load (&msg); |
476 |
l4_reply (from); |
l4_reply (from); |
477 |
} |
} |
478 |
|
else if ((label >> 4) == 0xffe) |
479 |
|
{ |
480 |
|
if (l4_untyped_words (msg_tag) != 2 || l4_typed_words (msg_tag) != 0) |
481 |
|
panic ("Invalid format of page fault message"); |
482 |
|
panic ("Unexpected page fault from 0x%xat address 0x%x (IP 0x%x)", |
483 |
|
from.raw, l4_msg_word (&msg, 0), l4_msg_word (&msg, 1)); |
484 |
|
} |
485 |
else |
else |
486 |
panic ("Invalid message with tag 0x%x", msg_tag.raw); |
panic ("Invalid message with tag 0x%x", msg_tag.raw); |
487 |
} |
} |