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
On Thu, Jun 22, 2017 at 12:24 PM, Norrathep Rattanavipanon wrote: Hi Gerwin, Thank you for your response. But I'm a little bit confused here. Maybe I
misunderstood something or I didnt phrase the question correctly.
From my understanding (please correct me if I'm wrong), each frame cap can
only be mapped once.
This means, you cannot have multiple mappings created by the same frame
cap. Then what did you mean by:
"the kernel will unmap the page if the cap that you are deleting is the
last cap to it. If there is still a copy of the frame cap around, it will
not automatically unmap."
? Oak On Thu, Jun 22, 2017 at 12:43 AM, Hi Oak, the kernel will unmap the page if the cap that you are deleting is the
last cap to it. If there is still a copy of the frame cap around, it will
not automatically unmap. This is a general principle for cap deletion: deleting the last cap to an
object triggers object “finalisation”, i.e. cleanup and resetting it to an
inert state so that it can later be removed from memory without impacting
the rest of the system. If there are still other caps to the same object in
the system, only the cap is removed. Cheers,
Gerwin On 22.06.2017, at 13:50, Norrathep Rattanavipanon Hello, I was wondering when we call seL4_cnode_delete on a (mapped) frame cap,
does the kernel also handle unmapping the frame (in addition to
withdrawing authority) as well?
Or the user-space has to ensure that the frame is unmapped first before
calling delete? I tried my code without unmapping that frame when deleting the cap and
it seems to work fine.
So I guess the kernel handles that? Oak --
Norrathep (Oak) Rattanavipanon
M.S. in Computer Science
University of California - Irvine
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel --
Norrathep (Oak) Rattanavipanon
M.S. in Computer Science
University of California - Irvine --
Norrathep (Oak) Rattanavipanon
M.S. in Computer Science
University of California - Irvine