Introduction to Embedded Systems Edward A. Lee & Sanjit A. Seshia UC Berkeley Copyright © 2008-12, Edward A. Lee & Sanjit Seshia, All rights reserved Chapter 6: Synchronous/Reactive ModelsLee & Seshia, UC Berkeley: 2 Concurrent Composition: Alternatives to Threads Threads yield incomprehensible behaviors. Composition of State Machines: • Side-by-side composition • Cascade composition • Feedback composition We will begin with synchronous composition, an abstraction that has been very effectively used in hardware design and is gaining popularity in software design.Lee & Seshia, UC Berkeley: 3 Recall: Actor Model for State Machines Expose inputs and outputs, enabling composition:Lee & Seshia, UC Berkeley: 4 Recall: Actor Model of Continuous-Time Systems A system is a function that accepts an input signal and yields an output signal. The domain and range of the system function are sets of signals, which themselves are functions. Parameters may affect the definition of the function S.Lee & Seshia, UC Berkeley: 5 Recall: Composition of Actors Angular velocity appears on both sides. The semantics (meaning) of the model is the solution to this equation. We will now generalize this notion of composition.Lee & Seshia, UC Berkeley: 6 Side-by-Side Composition Synchronous composition: the machines react simultaneously and instantaneously.Lee & Seshia, UC Berkeley: 7 Cascade Composition Synchronous composition: the machines react simultaneously and instantaneously, despite the apparent causal relationship!Lee & Seshia, UC Berkeley: 8 Synchronous Composition: Reactions are Simultaneous and Instantaneous Consider a cascade composition as follows:Lee & Seshia, UC Berkeley: 9 Synchronous Composition: Reactions are Simultaneous and Instantaneous In this model, you must not think of machine A as reacting before machine B. If it did, the unreachable states would not be unreachable. SC= SA SBunreachableLee & Seshia, UC Berkeley: 10 Feedback Composition Turns out everything can be viewed as feedback composition…Lee & Seshia, UC Berkeley: 11 Example: Feedback Composition Angular velocity appears on both sides. The semantics (meaning) of the model is the solution to this equation.Lee & Seshia, UC Berkeley: 12 Observation: Any Composition is a Feedback Composition s ∈ S N The behavior of the system is a “fixed point.”Lee & Seshia, UC Berkeley: 13 Fixed Point Semantics s ∈ S N Consider an interconnection of actors Abstract actors Abstract signals Reorganize We seek an s ∈ S N that satisfies F(s) = s. Such an s is called a fixed point. We would like the fixed point to exist and be unique. And we would like a constructive procedure to find it. It is the behavior of the system.Lee & Seshia, UC Berkeley: 14 Data Types x y s As with any connection, we require compatible data types:Vy VxThen the signal on the feedback loop is a functions: N ⇥ Vy⇤ {absent}Then we seek s such thatF(s)=swhere F is the actor function, which for determinate systemshas formF : (N ⇥ Vx⇤ {absent}) ⇥ (N ⇥ Vy⇤ {absent})Lee & Seshia, UC Berkeley: 15 Firing Functions x y s With synchronous composition of determinate state machines,we can break this down by reaction. At the n-th reaction, thereis a (state-dependent) functionf (n): Vx⇥ {absent}  Vy⇥ {absent}such thats(n)=(f (n))(s(n))This too is a fixed point.Lee & Seshia, UC Berkeley: 16 Well-Formed Feedback x y s At the n-th reaction, we seek s(n)  Vy⇥ {absent} such thats(n)=(f (n))(s(n))There are two potential problems:1. It does not exist.2. It is not unique.In either case, we call the system ill formed. Otherwise, it iswell formed.Note that if a state is not reachable, then it is irrelevant todetermining whether the machine is well formed.Lee & Seshia, UC Berkeley: 17 Well-Formed Example In state s1, we get the unique s(n)=absent.In state s2, we get the unique s(n)=present.Therefore, s alternates between absent and present.Lee & Seshia, UC Berkeley: 18 Composite MachineLee & Seshia, UC Berkeley: 19 Ill-Formed Example 1 (Existence) In state s1, we get the unique s(n)=absent.In state s2, there is no fixed point.Since state s2 is reachable, this composition is ill formed.Lee & Seshia, UC Berkeley: 20 Ill-Formed Example 2 (Uniqueness) In s1, both s(n)=absent and s(n)=present are fixed points.In state s2, we get the unique s(n)=present.Since state s1 is reachable, this composition is ill formed.Lee & Seshia, UC Berkeley: 21 Constructive Semantics: Single Signal 1. Start with s(n) unknown.2. Determine as much as you can about ( f (n))(s(n)).3. If s(n) becomes known (whether it is present, and if it isnot pure, what its value is), then we have a unique fixedpoint.A state machine for which this procedure works is said to beconstructive.Lee & Seshia, UC Berkeley: 22 Non-Constructive Well-Formed State Machine In state s1, if the input is unknown, we cannot immediately tellwhat the output will be. We have to try all the possible valuesfor the input to determine that in fact s(n)=absent for all n.For non-constructive machines, we are forced to do exhaus-tive search. This is only possible if the data types are finite, andis only practical if the data types are small.Lee & Seshia, UC Berkeley: 23 Must / May Analysis For the above constructive machine, in state s1, we can im-mediately determine that the machine may not produce an out-put. Therefore, we can immediately conclude that the output isabsent, even though the input is unknown.In state s2, we can immediately determine that the machinemust produce an output, so we can immediately conclude thatthe output is present.Lee & Seshia, UC Berkeley: 24 Constructive Semantics: Multiple Signals 1. Start with s1(n), ··· , sN(n) unknown.2. Determine as much as you can about ( f (n))(s1(n), ··· , sN(n)).3. Using new information about s1(n), ··· , sN(n), repeat step(2) until no information is obtained.4. If s1(n), ··· , sN(n) all become known, then we have aunique fixed point and a constructive machine.A state machine for which this procedure works is said to beconstructive.Lee & Seshia, UC Berkeley: 25 Constructive Semantics: Multiple Actors Procedure is the same.Lee & Seshia, UC Berkeley: 26 Constructive Semantics: Arbitrary Structure Procedure is the same. A state machine language with constructive semantics will reject all compositions that in any iteration fail to make all signals known. Such a language rejects some well-formed compositions.Lee & Seshia, UC Berkeley: