Hi,

In the seL4 FAQ section it states:

"Multicore is presently supported on x64 and Arm v7 (32-bit) and v8 (64-bit). 
Verification of the multicore kernel is in progress (but presently as an 
unfunded background activity)."

Considering only seL4
-----------------------------
My interpretation of this is that given a single seL4 application running on a 
device, it is not possible to currently guarantee the protections seL4 provides 
if the application invokes multiple threads across more than 1 core. Is this 
correct?


Considering CAmkES
----------------------------
I would also like to know how CAmkES affects this. For example, looking at the 
vm_multi app for the exynos5422 in the camkes-arm-vm repository, what would the 
effect be of assigning unique CPU affinities to each of the VM components? Do 
the guarantees still hold in this situation?

Thanks,

Ben Turner
Senior Engineer
Roke Manor Research Ltd
Tel:    +44 (0)1794 833721
[email protected]<mailto:[email protected]>

________________________________________
Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part 
of the Chemring Group. 
Registered in England & Wales. Registered No: 00267550
http://www.roke.co.uk
_______________________________________
The information contained in this e-mail and any attachments is proprietary to 
Roke Manor Research Limited and 
must not be passed to any third party without permission. This communication is 
for information only and shall 
not create or change any contractual relationship.
________________________________________
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to