Thanks Damon and Matthew for the quick response.
Further, I have following doubts if someone could clarify:
a) As far as I read the camkes code, I understand there is a collapse
function which merges the shared page in the two components and gives
required capabilities to both the components on that page. If, it is
same page, we can make it read only or write only at the hardware level
as suggested. How would the other thread, write or read from that page
for the communication to happen.
b) However, if we consider we have one page each for the dataport in
both components. Then, when one component writes on a dataport then that
should also be written on the dataport of the other component. Can you
point me towards that piece of code.
c) I would like to see the piece of code which converts my read/writes
of str/n/d in the client.c.template source file to the page level read
and write in camkes/seL4. As far as I understand, these are just
pointers. Some code must be there to convert them to page level
pointers.
d) I am curious to see the seL4/Camkes code which creates the page
level mapping (as suggested by Matthew).
e) In the entire conversation, I believe that the kernel stands for
seL4 kernel and not the host system (Ubuntu in my case) kernel. Please
correct me, if am wrong.
--
Thanks and Regards,
Amit Goyal
On 2019-07-01 09:53, Matthew Fernandez wrote:
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)
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
._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 on behalf of Amit Goyal
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
