Thanks for the reply, Gerwin. I really appreciate it. I have further questions below.
On Sun, Aug 4, 2019 at 8:51 PM Klein, Gerwin (Data61, Kensington NSW) < Gerwin.Klein@data61.csiro.au> wrote:
Hi Norrathep,
I have been reading Andrew Boyton's thesis about CapDL and realized that
CapDL does not support a shared memory page. Is it still a limitation in CapDL/Camkes? Or has it somehow been addressed?
This limitation has been lifted recently on the verification side, there can now be more than one cap to a frame in capDL.
I believe this has already made it into the public master branch, but I haven’t checked. If I remember correctly, the rest of the capDL tool chain has had this ability for quite some time, the result would just not pass wellformedness verification.
So does it have any implication if it fails wellformedness verification? i.e., would I still be able to extend the Camkes proof to prove functional correctness of the component's code? Btw, how can I access generated Isabelle theorems from Camkes. I'm using Camkes from the public master branch. I think I could access generated glue code and capdl C specification (e.g., for hello-camkes-1 example, it's in hello-camkes-1_build/capdl_spec.c) but I couldnt find any generated RPC stub and system initialization theorems.
Does this limitation include the case where a page is mapped/shared with
different access rights? e.g., a page is mapped writable to one process and the same page is mapped only readable to another process?
The different caps to the same frame can have different access rights, i.e. your scenario should be possible.
Cheers, Gerwin