Hi Oak. Yes, I think Gerwin has missed that frame caps are a bit of a special case. Per-object finalisation actions happen when the last cap to an object is being removed. You can make as many copies of an endpoint cap as you like, and the endpoint will only be cleared when the last one is deleted. Typically the creating manager/supervisor keeps the original for itself and decides when to perform this action. Some caps have per-cap state as well, e.g. the mapping info stored in a frame cap. As an aside, frame caps are the only caps with per-cap state that I know of, but other architectures might have more. This per-cap state is finalised with the cap. So deleting a mapped copy (or deleting all mapped copies with the Revoke operation) will remove the mapping. The kernel has to do this, in fact, because information about how to remove the mapping only exists in the mapped cap, which is the whole point of forcing you to duplicate the caps per-mapping. Cheers, Thomas. On 23/06/17 05:24, 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, mailto:Gerwin.Klein@data61.csiro.au> 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 mailto:nrattana@uci.edu> 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 Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

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, 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 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 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