[seL4] Re: Blocking and unblocking under the MCS kernel

Hi Kent, thanks for your response! Am 02.06.21 um 07:00 schrieb Kent Mcleod:

On Wed, Jun 2, 2021 at 6:10 AM Robert Kaiser wrote:

...

Hi all,

I'm working on the SOS example of the AOS course, trying to adapt code that used to work under the non-MCS kernel to the now used MCS kernel.

So far, this mostly works. However, I'm having problems in resuming a thread that is blocked in an IPC Call operation.

In simple cases where the server can reply immediately, the thread is successfully unblocked, simply by replying to the reply object as with the reply capability in the non-MCS kernel. However, if the server does not respond immediately, (i.e. it leaves the calling thread in blocked state, serves some other requests and/or notifications in the meantime, then comes back to reply), replying to the reply object silently fails to unblock the thread for some reason.

In the non-MCS kernel, it was necessary in these cases to save the reply capability in a cspace. Therefore I tried to similarly copy/move the reply object to a thread-specific cspace slot, but that doesn't help.

I'm sure I'm missing something very basic here. Can anybody point me to the right direction?

Hi, In MCS reply objects are no longer part of thread TCBs. Instead they are separate objects that can be created from kernel untyped. This means that a receiving thread needs a different reply object for each concurrent blocking thread it wants to hold. If the receiving thread uses a reply object that has a thread already blocked on it to receive a message from a new thread, the old thread's IPC operation is cancelled and it moves to inactive. So if you kept a separate reply object for each client thread and didn't share the reply objects between threads, the client threads should stop silently failing.

I thought I had implemented it like that (i.e. using individual, client-specific reply objects), but did it wrongly. My server waits for requests from several potential clients with an sel4_Recv() call, to which I have to pass an endpoint cap, a pointer to store the badge to and a reply object CPtr. I can tell the origin (i.e. client) of the received message/notification from the badge, but only *after* that call returns. However, in order to pass the right client-specific reply CPtr up front, I would have needed that information *before* making the sel4_Recv() call. So, what I did was trying to copy the reply object to the right client-specific slot after the sel4_Recv() call. But this failed because either I did it wrongly or because reply objects as such can not be copied. (*Can* they be copied?) My current (working) solution is to keep track of the client's states. If the current client thread is found to be blocked on its reply object, I pass a system-global CPtr to sel4_Recv() instead of the thread-specific one. This works, but it feels somewhat "unelegant". Is this acceptable practice or is there a better solution? Best Robert

...

Best,

Robert

-- Robert Kaiser

Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim

Computer Engineering RheinMain University of Applied Sciences

robert.kaiser@hs-rm.de http://www.cs.hs-rm.de/~kaiser

tel:(+49)611-9495-1292 fax:(+49)611-9495-1210

Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

-- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser@hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postanschrift/Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany