Camkes dataports on seL4 (seL4SharedData connector) are implemented as a shared memory mapping between the two components both pages are mapped to the same underlying frame of physical memory. The access rights are implemented via mapping attributes supported by the architecture. Your reads and writes through your dataport pointers are acting on this shared memory directly. The fault is generated by a hardware exception that seL4 handles by creating a fault and sending it to a registered fault handler (sendFaultIPC is the function in the kernel). There is a setting (that is enabled by default) that causes each Camkes component to set up a fault handler for all of its threads. If any of these threads cause a fault, such as by writing to read only memory, the fault handler will receive a message from the kernel.
These mapping attributes are set when the kernel creates the page mapping for each component using the relevant Map invocation [1]. The result of building a Camkes system for seL4 is a system spec that contains all of the seL4 kernel objects and capabilities described by the system. Within this spec, dataports are described as a capability to physical memory where each capability has the specified access rights. When the system initialiser (capdl-loader-app in our case) is started by seL4 as the root task, it constructs the system following the spec and starts each Camkes component. By this point, the seL4 invocations for setting up the shared data page mappings have been performed. You can look through the generated spec in the build directory by finding the file with the .cdl extension. If you search for the name of the dataport you can find the capabilities and objects to validate that the rights are as you would expect. Hope this answers your questions. @Matthew: Write only mappings are still coerced by the capdl-loader to read write mappings before calling the mapping invocation. [1] https://docs.sel4.systems/ApiDoc.html#map-4 _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
