1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
Problem: how do we address capabilities in other cspaces?
seL4 does this with guarded page tables. Proposal 2 suggested incorporating
something which is essentially identical to seL4's approach, but I ran into
issues in the implementation: how to deal with the init thread's cspace?
The init thread's guard is set to 64-k, so that capability addresses from
0-(1 << k) resolve predictably, i.e. caddr N refers to slot N. To resolve
through to an Nth-order cspace, we would have had to change that guard, but
that would shift all of the capability addresses over -- a guard of 8 would
make 0x100 address cslot 0. This would invalidate all of the capabilities
addresses init was already using, including all of the capabilities in
bootinfo. It would also mean that addressing adjacent cslots would require
incrementing by 0x100 instead of 1. Lots of headaches in this approach.
Proposal 3:
- little endian (root table address occupies least significant bits)
- no guards (guard is always 64-k, it wasn't very useful anyway)
k = cspace bits (1 << k slots)
cspace A
k=8
+==========+
|%reserved%|
+----------+
| page | 0x01
+----------+
| ... | cspace B
+----------+ k=8
| cnode | 0xEF --> +==========+
+----------+ |%reserved%|
| ... | +----------+
+==========+ | ... | cspace C
+----------+ k=16
| cnode | 0xBE --> +==========+
+----------+ |%reserved%|
| ... | +----------+
+==========+ | ... |
+----------+
| page | 0xDEAD
+----------+
| ... |
+==========+
lookup algorithm:
. given addr
. slot = addr & ((1 << k) - 1) e.g. 0xBEEF becomes 0xEF at this step
. if remaining bits are all 0:
terminate, use this slot
. else if slot is a cspace:
addr >>= k
repeat with that cspace as the root
. else
lookup fails
a capability address is for this configuration is:
0xCCCCBBAA
example addresses:
0x1 page in cspace A
0xEF cspace B (cnode in cspace A)
0xBEEF cspace C (cnode in cspace B)
0xDEADBEEF page in cspace C
--
0xDEAD page in cspace C, relative to cspace C