Hi Jeff,

We really like the *WithMRs functions and there is no plan to get rid of them. Support for the syscall stub generator using them was removed here (https://github.com/seL4/seL4/commit/5271925ba54639b849261e652e73ab56ee243fb2).

Not being able to get error information after doing an invocation is unacceptable as a default. I suppose if you have an application where you *know* you won't need the error information then you might want to re-enable this.

Ideally we come up with some better stub generation that doesn't throw away the errors.

Adrian

On Thu 27-Oct-2016 10:14 AM, Jeff Waugh wrote: Hi all,

Last night I opened two pull requests to begin fixing the CallWithMRs code path on x86_64 and aarch32.

syscall_stub_gen.py couldn't generate x86_64 stubs for the CallWithMRs / non-IPCBuffer path. That didn't surprise me too much, as x86_64 support is relatively new.

Then I discovered that libsel4 *always* [1] uses the IPCBuffer path. Hrm.

Changing that prompted a quick fix to aarch32's apparently unused, long since even built CallWithMRs. (Similar fixes might be needed in some of the other functions.)

The test suite failed with it on aarch32, which I could poke at in more depth, but it worked fine for x86_64.

So… what's the status of the *WithMRs functions? Based on my understanding of the source (particularly the new helper functions) and assembly output, they're destined for the chopping block, right?

Thanks, Jeff

[1] hard coded --buffer parameter to syscall_stub_gen.py in libsel4/Makefile, since late 2015

_______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

To give a bit more detailed explanation. Take the Page_Map invocation, more concretely let's look at seL4_ARM_Page_Map in the case where we do not pass --buffer

LIBSEL4_INLINE long seL4_ARM_Page_Map(seL4_X86_Page service, seL4_CPtr vroot, seL4_Word vaddr, seL4_CapRights rights, seL4_ARM_VMAttributes attr) { seL4_MessageInfo_t tag = seL4_MessageInfo_new(ARMPageMap, 0, 1, 3); seL4_MessageInfo_t output_tag; seL4_Word mr0; seL4_Word mr1; seL4_Word mr2;

/* Setup input capabilities. */ seL4_SetCap(0, vroot);

/* Marshal input parameters. */ mr0 = vaddr; mr1 = rights; mr2 = attr;

/* Perform the call, passing in-register arguments directly. */ output_tag = seL4_CallWithMRs(service, tag, &mr0, &mr1, &mr2, seL4_Null);

return seL4_MessageInfo_get_label(output_tag); }

Now let's suppose we call this, and it returns an error.

seL4_Error error = seL4_X86_Page_Map( [args] ); if (error == seL4_FailedLookup) { /* do something */ }

Now in the case of a failed lookup when mapping a page the kernel gives us some useful information, it tells us how far through traversing the paging structures it got, before it failed to find something. (okay, on ARM the only failure can be because of a missing page table, but on x86_64 it becomes more relevant). So let's go and do that (please note that libsel4 has constants and helpers for all these, I've put in the raw constants to make the example easier)

seL4_Word failed_bits = seL4_GetMR(2); if (failed_bits == 20) { /* need a page table */ } else { /* something crazy just happened */ }

Now here's the problem. We want message register two. But on ARM, the first 4 message registers are done actually in register (not the IPC buffer). When we called seL4_CallWithMRs, it gave returned us message register 2 in the variable we passed to it, but we have then thrown it away, thus forever losing the error information.

As for adding more tests, people are always encouraged to do that :)

Adrian

On Thu 27-Oct-2016 11:49 AM, Jeff Waugh wrote: On Thu, Oct 27, 2016 at 11:03 AM, <Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au> wrote: Not being able to get error information after doing an invocation is unacceptable as a default. I suppose if you have an application where you *know* you won't need the error information then you might want to re-enable this.

Ideally we come up with some better stub generation that doesn't throw away the errors.

OK, clearly I have to read these functions way more closely to grok the difference. :-)

Oddly, I can't find any public code that uses the *WithMRs functions. In order to give them regular exercise, would you like me to add some of them to the syscalls tests? :-)

Thanks, Jeff

On Thu 27-Oct-2016 1:12 PM, Jeff Waugh wrote: On Thu, Oct 27, 2016 at 12:08 PM, <Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au> wrote: Now here's the problem. We want message register two. But on ARM, the first 4 message registers are done actually in register (not the IPC buffer). When we called seL4_CallWithMRs, it gave returned us message register 2 in the variable we passed to it, but we have then thrown it away, thus forever losing the error information.

I can see the more complex generated functions (that use more than the number of available real registers) are comfy using SetMR before and GetMR after *WithMRs calls. I'm assuming a SetMR is safe after the *WithMRs call? Correct me if I've misunderstood something in there, but it seems about right.

Naively, would the following be appropriate to generate:

LIBSEL4_INLINE long seL4_ARM_Page_Map(seL4_ARM_Page service, seL4_ARM_PageDirectory pd, seL4_Word vaddr, seL4_CapRights rights, seL4_ARM_VM Attributes attr) { ...

/* Perform the call, passing in-register arguments directly. */ output_tag = seL4_CallWithMRs(service, tag, &mr0, &mr1, &mr2, seL4_Null);

/* Unmarshal real register results into the IPC buffer. */ seL4_SetMR(0, mr0); seL4_SetMR(1, mr1); seL4_SetMR(2, mr2); // 4th register isn't relevant for this function, but would be elsewhere

return seL4_MessageInfo_get_label(output_tag); }

This is where things start to get complicated. Different errors have a different number of words for their fault. In the worst case this can be 5 words, so all 4 message registers on arm need to be stored. Without some detailed information to the syscall stub generator of exactly which invocations can cause which errors, you're looking at just always stashing all 4 MRs back into the IPC buffer. Could probably optimize this by checking the label before return and storing the MRs only if an error happened.

I actually cannot think of a compelling reason for why that wouldn't work.... Either there is something I've forgotten, or the solution really is that simple.

Adrian