XMOS in safety critical systems: IEC 61508 and spatial and t

[aclassifier]

IEC 61508-3 © IEC:2010. "Annex F (informative). Techniques for achieving non-interference between software elements on a single computer" states that:

Techniques for achieving and demonstrating spatial independence include the following:
 
a) Use of hardware memory protection between different elements, including elements of differing systematic capability.
 
b) Use of an operating system which permits each element to execute in its own process with its own virtual memory space, supported by hardware memory protection.
 
c) Use of rigorous design, source code and possibly object code analysis to demonstrate that no explicit or implicit memory references are made from between software elements which can result in data belonging to another element being overwritten (for the case where hardware memory protection is not available).
 
Even if the heading is "single computer" this post is about how to argue when also multi-core:
 
The XMOS processors, without HW memory protection (like many smaller microcontrollers, but then, are the XMOS processors "small"?), but with xC, a restrictive view on pointers, analysis tools and a known scheduler in HW (even if the two latter are closer to "temporal independence", see below) would be rather easy to argue for, in a 61508 safety case?
 
Could the below paragraph (text suggested by me) describe the XMOS situation, made generic to also include other processors:
 
Concurrent or parallel language and compiler support may safeguard against parallel usage violations to such a degree that it may be shown that hardware memory protection may not be needed.
 
I remember the occam/transputer discussion about this in the nineties. The XMOS case, how close is it to that case? (occam didn't have any pointers).
 
There also is a rather lengthy discussion of temporal independence in Annex F (not pasted here). I wonder about the below paragraph (text also suggested by me) might close in on the situation (and also include the XMOS case):
 
Cores that guarantee a specified response time (by for example analyzing the best and worst case timing paths including through a known non-chip scheduler) might yield deterministic hard timing.