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) <Damon.Lee@data61.csiro.au> 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 <devel-bounces@sel4.systems> on behalf of Amit Goyal <amitgoyal@cse.iitb.ac.in>
Sent: Monday, 1 July 2019 9:16 AM
To: devel@sel4.systems
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
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel