Thank you, Thomas. That makes sense.
I run into a problem in the implementation though. I try to create a copy of a copy of a frame cap and revoke it later. But the revocation does not seem to work as I expect.
My code is as follows:
vka_object_t frame_obj;
error = vka_alloc_frame(&vka, FRAME_BITS, &frame_obj);
assert(error == seL4_NoError);
cspacepath_t copy_rw_path, copy_copy_rw_path, page_path;
vka_cspace_make_path(&vka, frame_obj.cptr, &page_path);
// create a copy
error = vka_cspace_alloc_path(&vka, ©_rw_path);
assert (error == seL4_NoError);
error = vka_cnode_copy(©_rw_path, &page_path, seL4_AllRights);
assert(error == seL4_NoError);
// create a copy of copy
error = vka_cspace_alloc_path(&vka, ©_copy_rw_path);
assert (error == seL4_NoError);
error = vka_cnode_copy(©_copy_rw_path, ©_rw_path, seL4_AllRights);
assert(error == seL4_NoError);
vka_object_t objects[3];
int num = 3;
char* mapping = (char*)(0x11000000);
error = sel4utils_map_page(&vka, simple_get_pd(&simple), copy_copy_rw_path.capPtr, (void*)mapping, seL4_AllRights, 1, objects, &num);
assert(error == 0);
*mapping = 'a';
if(vka_cnode_revoke(©_rw_path)) printf("REVOKE failed\n");
*mapping = 'b'; // This should fail
However, if I revoke the original cap instead (using vka_cnode_revoke(&page_path)), then it seems to properly revoke the mapping and a copy.
Anything I'm missing here? or does seL4 only support 1-level of cap delegation?
Thanks,
Oak