Hi Martin,

I think my question was slightly different.

It can be better explained by giving the example of attaching a function for a region_map. This function takes in a dataspace capability as an argument. I understand that when a client does a rm_client.attach(ds_cap, vaddr, size ...) It is transformed (by the client stub code) to a seL4 IPC message which goes over a badged-endpoint to the rm_service in the core.

The rm_service finds out which rm to manipulate by knowing which badged endpoint the message was delivered to(I think). However, it also got another badged endpoint cap as an argument (the one for dataspace). seL4 will not reveal the badge for this endpoint as the IPC message did not arrive over this endpoint. But the core still needs to find the dataspace corresponding to this dataspace-cap. So my question is, how can the server know the badge of an endpoint that it had issued in the past.

I think the answer lies in [1] decode_seL4_message() and new_seL4_message() functions. Here I see that when Msfbuf_base has a cap as an argument(dataspace cap in the case of rm.attach()), it is added in the IPC msg buffer in two places:

The seL4 cap is sent as an extra cap in the IPC message
Another place is an IPC message argument. Looks like it is a value of the RPC object.

I think the 2nd one is the missing piece in my design. I relied solely on the server to recognize the server-side object using just the badged endpoint seL4 cap. This does not work as seL4 will not reveal the badge of any of the endpoints caps, which came as extra caps in a message.

Thanks,

Sid

[1] <GENODE>/repos/base-sel4/src/lib/base/ipc.cc's

On Fri, Apr 22, 2022 at 2:37 AM Martin Stein <martin.stein@genode-labs.com> wrote:

[CAUTION: Non-UBC Email]

Hi Sid,

I'm not an expert regarding the topic you're in. However, if I'm not
mistaking, the badges you're talking about sound like what is
accomplished by the so-called ID space in Genode [1][3][4].

Some examples on how ID spaces are used are the Trustzone VMM block
driver [2] that manages its device objects with IDs, the VFS file
systems [5] and GPU buffers [6]. Maybe, looking into that code provides
you with some answers.

Let me know if so!

Cheers,
Martin

[1] <GENODE>/repos/base/include/base/id_space.h
[2] <GENODE>/repos/os/src/server/tz_vmm/include/block_driver.h
[3] https://genode.org/documentation/genode-foundations-21-05.pdf 8.8.4.
ID space
[4] grep -r "ID space" <GENODE>/doc/
[5] <GENODE>/repos/os/src/lib/vfs/fs_file_system.h
[6] <GENODE>/repos/os/src/drivers/gpu/intel/main.cc

On 20.04.22 00:42, Sid Agrawal wrote:
> Hi Genode,
> I am building userspace on seL4 directly and have run into a design
> issue. I am implementing server and client using badged endpoints. I
> think Genode would have run into the same issue, and I would like to
> understand better how Genode solves it. It is not directly a Genode
> question, but I would benefit from your experience. Below I have laid
> out the scenario, the issue, and some questions.
>
>
> _Scenario_
>
> I have a userspace server that implements the functionality for an
> object(say type obj_T1). The server hands out badged-endpoints to
> clients to interact with this object. The badge is the virtual address
> of the object's struct in the server’s virtual address space. A client
> can interact with the object by sending messages on this badged
> endpoint. The client never learns the badge value. The kernel extracts
> the badged value when the server receives a message on this endpoint. By
> using the badge value, the server knowswhich object the client is trying
> to manipulate.
>
>
> The same PD, which implements the 1st server, also implements another
> server(in a separate thread, but same address space) for another object
> type (say type obj_T2). The server follows the same paradigm of handing
> out badged endpoints and using the badges values to keep track of the
> object.
>
>
> _Issue_
>
> I have a scenario where the client wants to invoke the functionality of
> obj_T1. This functionality needs access to obj_T2 as well. The client
> has badged EP caps to both objects. The client can invoke the badged EP
> handed out by server-1 for obj_T1 and givethe badged EP of obj_T2 as an
> extraCap in the IPC message(or vice versa). Since the server has noway
> to look up the badge of the second cap, it cannot look up the underlying
> object for obj_T2.
>
> So my questions are:
>
> 1.
>
> Is there a way for a PD to look up the badge value of badged EP? I
> think the answer is no, but I thought I would still ask.
>
> 2.
>
> Is my idea of using the badge to keep track of the underlying object
> on the right track? Is there a better way of going about doing it?
>
> 3.
>
> As a potential solution, I can extend my server to add a new
> function, say GETID, which returns the badge value of a given
> object(i.e., EP). Since I know that the server always badges the EP
> with the virtual address of the struct, it is a trivial call to
> implement. But I somehow feel like this is not a neat idea, not
> quite sure why.
>
>
> Thanks for the help, everyone!
>
> Thanks,
> Sid
> Graduate Student @ UBC
> sid-agrawal.ca <http://sid-agrawal.ca>
>
> _______________________________________________
> Genode users mailing list
> users@lists.genode.org
> https://lists.genode.org/listinfo/users
>

_______________________________________________
Genode users mailing list
users@lists.genode.org
https://lists.genode.org/listinfo/users