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
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to