64 lines
939 B
Text
64 lines
939 B
Text
#ifdef ARCH_ARM
|
|
arch arm11
|
|
#else
|
|
arch ia32
|
|
#endif
|
|
|
|
objects {
|
|
my_ep = ep /* A synchronous endpoint */
|
|
|
|
/* Two thread control blocks */
|
|
tcb1 = tcb
|
|
tcb2 = tcb
|
|
|
|
/* Four frames of physical memory */
|
|
frame1 = frame (4k)
|
|
frame2 = frame (4k)
|
|
frame3 = frame (4k)
|
|
frame4 = frame (4k)
|
|
|
|
/* Two page tables */
|
|
pt1 = pt
|
|
pt2 = pt
|
|
|
|
/* Two page directories */
|
|
pd1 = pd
|
|
pd2 = pd
|
|
|
|
/* Two capability nodes */
|
|
cnode1 = cnode (2 bits)
|
|
cnode2 = cnode (3 bits)
|
|
}
|
|
caps {
|
|
cnode1 {
|
|
0x1: frame1 (RW) /* read/write */
|
|
0x2: my_ep (R) /* read-only */
|
|
}
|
|
cnode2 {
|
|
0x1: my_ep (W) /* write-only */
|
|
}
|
|
tcb1 {
|
|
vspace: pd1
|
|
ipc_buffer_slot: frame1
|
|
cspace: cnode1
|
|
}
|
|
pd1 {
|
|
0x10: pt1
|
|
}
|
|
pt1 {
|
|
0x8: frame1 (RW)
|
|
0x9: frame2 (R)
|
|
}
|
|
tcb2 {
|
|
vspace: pd2
|
|
ipc_buffer_slot: frame3
|
|
cspace: cnode2
|
|
}
|
|
pd2 {
|
|
0x10: pt2
|
|
}
|
|
pt2 {
|
|
0x10: frame3 (RW)
|
|
0x12: frame4 (R)
|
|
}
|
|
}
|