Proving determinacy

Technical questions regarding the XTC tools and programming with XMOS.
User avatar
Respected Member
Posts: 479
Joined: Wed Apr 25, 2012 8:52 pm

Proving determinacy

Post by aclassifier »

In [1] they show that "executions in the PharOS real-time system are deterministic in the sense that the sequence of local states for every process is independent of the order in which processes are scheduled” and “fortunately, it is possible to design concurrent real-time systems such that their behavior does not depend on the order of scheduling, as long as all components have access to a common time base”

Would such a proof at all be necessary for the XMOS architecture? As I read this I would think that CSP processes have this by default since such processes don’t rely on shared data not shared over the shared event called a channel (and when needed, below interface).

[1] continues with "the core idea is to associate every instruction that some process wishes to execute with a temporal window of execution and to ensure that a message sent from one process to another can be received only if the execution window of the receiving instruction is strictly later than that of the sending instruction."

I have a feeling that there's much unnecessary (as seen from some other angle) proving out there? [Maybe all proofs render unnecessary from some other angle?]

Has the XCORE architecture been proven (with say CSPm/FDR), or has this been considered not necessary? Or are parts of it proven? Or none?

[1] - Proving Determinacy of the PharOS Real-Time Operating System by Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, and Stephan Merz © Springer 2016 at ... haros.html

Øyvind Teig
Trondheim (Norway)