Cycle-based Programming of Distributed Systems: The Synchrony Hypothesis Michael Mendler Faculty of Information Systems and Applied Computer Sciences University of Bamberg, Germany M. Mendler tubs.CITY, Braunschweig, 1.7.2009 1 Overview 1. 2. 3. 4. 5. M. Mendler Synchronous Programming The Synchrony Hypothesis Causal Reaction = Fixed Point ? What‘s in a Step ?: Notions of Causality The Synchrony Hypothesis (Hypo-)Thesis tubs.CITY, Braunschweig, 1.7.2009 2 1. Synchronous Programming M. Mendler tubs.CITY, Braunschweig, 1.7.2009 3 Synchronous Programming Control flow paradigms UMLStatecharts Statemate Stateflow RSML VisualState SyncCharts Modecharts ... Statecharts (Harel) Esterel (Berry, Gonthier) Signal (Benveniste, LeGuernic) Lustre (Caspi, Halbwachs) iCONNECT Syndex ... Argos LabView Simulink Lustre V7 SCADE Data flow paradigms M. Mendler tubs.CITY, Braunschweig, 1.7.2009 4 Example: SCADE – Esterel Tech Data Flow: SCADE Lustre ABSync Detection 1 WaitAandB idle wA arm wB A/arm dA B/arm cnt dB 2T/ disarm Inhib / AB done Reset Timer eot 2 • embedded systems domain (avionics, automotive) • rigorous semantics • verification & testing (certification) • code-generation • hw/sw codesign disarm signal arm signal disarm Control Flow: SCADE Safe State Machines M. Mendler tubs.CITY, Braunschweig, 1.7.2009 5 Orthogonality in Time and Space M. Mendler tubs.CITY, Braunschweig, 1.7.2009 6 Data Flow data flow M. Mendler tubs.CITY, Braunschweig, 1.7.2009 7 Data Flow Q: How do we treat the cyclic DF dependencies ? data flow A: Continuitiy Hypothesis, Kahn stream semantics ! M. Mendler tubs.CITY, Braunschweig, 1.7.2009 8 Orthogonality in Time and Space M. Mendler tubs.CITY, Braunschweig, 1.7.2009 9 State Flow state flow M. Mendler tubs.CITY, Braunschweig, 1.7.2009 10 State Flow Q: How do we treat the cyclic SF dependencies ? state flow A: Synchrony Hypothesis, Fourman response semantics M. Mendler tubs.CITY, Braunschweig, 1.7.2009 11 2. The Synchrony Hypothesis M. Mendler tubs.CITY, Braunschweig, 1.7.2009 12 Synchrony Hypothesis Environment view: Reactions are • atomic • deterministic • bounded System view: Reactions may be • non-atomic • non-deterministic • unbounded M. Mendler “A reactive system is faster than its environment, hence reactions can be considered atomic” tubs.CITY, Braunschweig, 1.7.2009 14 The Synchrony Paradox Environment view: Reactions are • atomic • deterministic • bounded Paradox ? System view: Reactions may be • non-atomic • non-deterministic • unbounded M. Mendler faster R2 R1 faster “A reactive system is faster than its environment, hence reactions can be considered atomic” tubs.CITY, Braunschweig, 1.7.2009 15 Programming Synchronous Reactions • logical transitions • conjunctions = parallelism • negations code choices, priorities and hierarchy parallelism logical transitions choice, priority M. Mendler tubs.CITY, Braunschweig, 1.7.2009 21 Programming Synchronous Reactions • logical transitions • conjunctions = parallelism • negations code choices, priorities and hierarchy M. Mendler tubs.CITY, Braunschweig, 1.7.2009 22 Programming Synchronous Reactions • logical transitions • conjunctions = parallelism • negations code choices, priorities and hierarchy M. Mendler tubs.CITY, Braunschweig, 1.7.2009 23 Synchronous Abstraction In which sense does REACT describe an atomic macro step ? instantaneous reaction input stimulus M. Mendler tubs.CITY, Braunschweig, 1.7.2009 24 Synchronous Abstraction In which sense does REACT describe an atomic macro step ? input stimulus M. Mendler instantaneous reaction Cyclic dependencies ? => Fixed-Points ! tubs.CITY, Braunschweig, 1.7.2009 25 3. Causal Reaction = Fixed-Point ? M. Mendler tubs.CITY, Braunschweig, 1.7.2009 28 Synchronous Reactive Component Reactive component , atomic logical signals, logical transitions positive, negative triggers, actions Response of C action enabled „response function“ M. Mendler tubs.CITY, Braunschweig, 1.7.2009 29 Reaction = Fixed-Point ? Logical Coherence [Berry] "A signal s is present in an instant if and only if an `emit s' statement is executed in this instant." Logical Coherence & Reactiveness ● ● M. Mendler A response S is logically coherent iff S is a fixed-point of AEC, i.e., S = AEC(S). C is logically reactive iff it in every activation state and environment, AEC has a fixed-point. tubs.CITY, Braunschweig, 1.7.2009 30 Causal Response = Unique Fixed Point ? Problem The response function is not monotonic ! M. Mendler tubs.CITY, Braunschweig, 1.7.2009 31 Causal Response = Unique Fixed Point ? Problem The response function covariant contravariant is not monotonic ! • no unique (least) fixed points ! • compositionality and full-abstraction problems ! • different computation methods ! → different notions of steps, instants, reactions ... M. Mendler tubs.CITY, Braunschweig, 1.7.2009 32 Example ≈ For all inputs there is a unique stationary Boolean fixed point. Thus, the system is logically reactive. We can compile & execute Boolean solution atomically ! But what if we are compiling for a component-based and distributed architecture ? M. Mendler tubs.CITY, Braunschweig, 1.7.2009 34 Example Oscillation under up-bounded inertial delay scheduling [Brzozowski & Seger] M. Mendler tubs.CITY, Braunschweig, 1.7.2009 35 Example Oscillation can be avoided if we schedule s1, s3 with higher priority than s2 or implement s1, s3 atomically, as a 2in/2out block. Then, whenever s2 is executed, we maintain the invariant M. Mendler tubs.CITY, Braunschweig, 1.7.2009 36 4. What is in a Step ? Notions of Causality M. Mendler tubs.CITY, Braunschweig, 1.7.2009 38 What is in a Step ? - A Profusion of Options 1 Avoid Negations ƒ only positive triggers [Modecharts´94, Argos´89] 2 Modify Semantics of Negation ƒ give up global consistency [Huizing&al.´88, Modecharts´96] ƒ add consistency as implicit trigger [Maggiolo-Schettini &al.´96, Lüttgen &al.´99] 3 Give up Synchrony Hypothesis (no abstraction) ƒ all signals delayed[Statemate´90,VHDL,RSML´95,PretC´09] ƒ negative triggers delayed [Saraswat TCCP´94, Boussinot & deSimone SL´95, Boussinot FunLoft‘07] M. Mendler tubs.CITY, Braunschweig, 1.7.2009 39 What is in a Step ? - A Profusion of Options 4 Conflict-avoiding Schedules ƒ only accept stratifiable (statically schedulable) programs [Normal Logic Programming] ƒ sequential schedule (endochrony) [Benveniste &al.´00] ƒ NRSA „no reaction to signal absence“ (weak endochrony, concurrent input reading) [Butucaru, Caillaud´06] M. Mendler tubs.CITY, Braunschweig, 1.7.2009 40 What is in a Step ? - A Profusion of Options 5 Self-scheduled Run-time (explicit absence, dual rail) ƒ non-deterministic speculation on absence [Pnueli & Shalev´91; Boussinot‘s „basic semantics“ ‘98] M. Mendler tubs.CITY, Braunschweig, 1.7.2009 42 What is in a Step ? - A Profusion of Options 5 Self-scheduled Run-time (explicit absence, dual rail) ƒ non-deterministic speculation on absence [Pnueli & Shalev´91; Boussinot‘s „basic semantics“ ‘98] „Feel free to assume the absence of a signal as long as it is consistent to do so; if necessary, backtrack!“ - fully-abstract, compositional intuitionistic Kripke semantics [Lüttgen & Mendler´01] - game-theoretic “lazy“ fixed-points [Aguado & Mendler´05] M. Mendler tubs.CITY, Braunschweig, 1.7.2009 43 What is in a Step ? - A Profusion of Options 5 Self-scheduled Run-time (explicit absence, dual rail) ƒ non-deterministic speculation on absence [Pnueli & Shalev´91; Boussinot‘s „basic semantics“ ‘98] ƒ constructiveness = “computed“ absence [Berry´00] M. Mendler tubs.CITY, Braunschweig, 1.7.2009 44 What is in a Step ? - A Profusion of Options 5 Self-scheduled Run-time (explicit absence, dual rail) ƒ non-deterministic speculation on absence [Pnueli & Shalev´91; Boussinot‘s „basic semantics“ ‘98] ƒ constructiveness = “computed“ absence [Berry´00] “Accept the absence of a signal only under computable evidence that it may not occur later“ - game-theoretic “eager“ fixed-points [Aguado & Mendler´05] - delay-insensitivity = non-inertial delay = constructive modal logic [Mendler & Shiple & Berry´07] ƒ SugarCubes [Boussinot ´98] (Esterel v3,v4,v5,v6,v7) ƒ & many other hardware approaches - speed-independence, semi-modularity, distributivity, ... M. Mendler tubs.CITY, Braunschweig, 1.7.2009 45 5. The Synchrony Hypothesis Thesis M. Mendler tubs.CITY, Braunschweig, 1.7.2009 46 Outlook Thesis 1 There are as many notions of constructive causality as there are scheduling/run-time models Thesis 2 Synchronous reaction requires intensional semantics: classical Boolean logic ⇒ constructive logic (e.g., Heyting algebra) least and greatest fixed points ⇒ general game-theoretic fixed points M. Mendler tubs.CITY, Braunschweig, 1.7.2009 47 Thank You ! M. Mendler tubs.CITY, Braunschweig, 1.7.2009 54