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 <[email protected]
> 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, <[email protected]> wrote:
>
>> 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 <[email protected]>
>> wrote:
>> >
>> > 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
>> > [email protected]
>> > 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
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
