Logical Synchrony Plus Functional Processes Entail Observable Determinacy
Sanjiva Prasad · 2024
Determinacy is a desirable but difficult-to-achieve behavioural property in scalable distributed systems. Deterministic Models of Computation range from the asynchronous Kahn Process Networks to synchronous reactive languages such as Lustre, where logical clocks enforce the synchrony hypothesis. These models have well-founded data-flow s emantics w here computations are viewed as the least fixed point solutions of simultaneous equations defined by continuous functions on streams of discrete values. However, scalable and efficient implementations of the Kahn model are challenging to construct, while the synchrony hypothesis in Lustre makes distributed implementations difficult. Moreover, determinacy is a consequence of specific assumptions built into the computational model. The notion of Logical Synchrony, proposed by Lall et al., and explored further by Kenwright et al., suggests that synchronisation issues may be decoupled from computation, leading to a distributed model where computations at independent nodes are related by invariant logical delays. We provide a semantic notion of behaviour for functional processes running on such Logical Synchrony Networks (extension graphs), and an appropriate and robust notion of logical observational equivalence (wavefront equivalence) retaining semantic aspects of KPNs, specifically determinacy. Further, we propose extending the versatile notion of the synchronous observer, exploited in the Lustre toolset, to a network of located synchronous observers with the same invariant logical delays as the distributed system. Thus we will be able to use the same logically synchronous model of computation for checking or monitoring a class of (safety) properties of programs, specifying axioms and assumptions on behaviour, constraining models and specifying test cases, etc.