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