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) < [email protected]> 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 > > -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
