I haven’t worked with CAmkES for some time, so it’s possible I’m going to inject nothing but nonsense into this conversation, but Amit’s question stirred a memory of mine. I read Amit’s question as, “why does reading from a dataport with W permission trigger a fault?”
Whether you expect a read to write-only memory to trigger a fault or not depends on how you think of hardware. At one point, CAmkES was passing the user’s requested permissions directly to the kernel.¹ This meant if you asked for a write-only dataport, CAmkES asked the kernel for write-only memory. The platforms we ran on at the time (ARMv6 and 32-bit x86?) had no concept of write-only mappings, and the kernel’s logic silently downgraded this to a kernel-only mapping. When we realised this, we worked around it by coercing a write-only mapping into read/write during code generation. This seemed more consistent with the user’s expectation. I notice requesting a write-only mapping from seL4 now triggers a debug message (c.f. maskVMRights) so maybe it was in response to this. As to why reading a write-only dataport now triggers a fault, I do not know. Maybe write-only dataports now really are write-only in some clever way? If I’ve misconstrued the question, please consider this a scenic detour and we will return to our regularly scheduled program. ¹ It’s possible this was actually in the CapDL loader not CAmkES dataports and I’m misremembering the scenario. > On Jun 30, 2019, at 17:47, Lee, Damon (Data61, Kensington NSW) > <[email protected]> wrote: > > Hi Amit, > > I'd like to apologise first for errors in the tutorials. The first hint for > Task 8 of this tutorial should say: "use attributes <component>.<interface > name>_access" instead. > > As for the fault handler, I assume that you didn't get a fault where we > intended it to (writing to 'd_typed'). > > The checks aren't really done by CAmkES or seL4 but rather, by the hardware. > Depending on the permissions given to the shared memory dataports, pages are > mapped in with different permissions. So writing to a read-only page will > trigger a page fault and the kernel will defer it to the fault handlers of > your components. > > And as you've found out, the default handlers are found in > 'component.template.c' of the CAmkES repository. > > I hope this answers your question. > > PS: Reference solutions for the tutorials can be accessed by running the init > script with the --solution flag. E.g. `./init --tutorial hello-camkes-2 > --solution` would get you the solutions for the 'hello-camkes-2' tutorial. > > Sincerely, > Damon > From: Devel <[email protected]> on behalf of Amit Goyal > <[email protected]> > Sent: Monday, 1 July 2019 9:16 AM > To: [email protected] > Subject: [seL4] Understanding Camkes Dataport Interface Access Rights > > Hi All, > > I was looking at hello-camkes-2 tutorial. I understand the concept of > dataports and the access rights given on dataport interfaces. I changed > the configuration in hello-camkes-2.camkes.template file by adding > echo.d = "R"; client.d = "W";. I did some changes in the > client.c.template file to read on the dataport interface d by trying to > access its contents through str/n/d pointers. Although, it only has > write access on "d" in the new configuration. This leads to the fault > handler being called when I simulate the build. I was just curious to > find out where are such checks being done at the backend in camkes/seL4. > I could find the code of fault handler in component.template.c but I > could not find anywhere the code which checks that the client only has > write access on dataport d and thus calling the fault handler. Can > someone point me towards that piece of code or explain what is exactly > happening at the backend in camkes/seL4? > > -- > Thanks and Regards, > Amit Goyal > > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel > <https://sel4.systems/lists/listinfo/devel> > _______________________________________________ > Devel mailing list > [email protected] <mailto:[email protected]> > https://sel4.systems/lists/listinfo/devel > <https://sel4.systems/lists/listinfo/devel>
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
