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.
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