Transcript Real-Time FRP - Computer Science

Real-Time FRP
Zhanyong Wan
Yale University
Department of Computer Science
Joint work with:
Walid Taha
Paul Hudak
Sept 4, 2001
ICFP, Florence, Italy
1
Outline
 To be written
Sept 4, 2001
ICFP, Florence, Italy
2
Reactive Programming
 Reactive systems


Continually reacts to stimuli
Environment cannot wait
 Reactive Languages






Signal: programming by constraints
Lustre: synchronous data-flow
Esterel: imperative
Simulink: visual but lacks control structure
Synchronous Kahn networks: extends Lustre w/ recursion
FRP (Functional Reactive Programming):

Sept 4, 2001
synchronous data-flow + (higher-order, typed) functional
programming
ICFP, Florence, Italy
3
Functional Reactive Programming
 Functional Reactive Programming (FRP)








General framework for reactive programming
High-level, declarative
Time is continuous
Embedded in Haskell
Behaviors
Events
Reaction
Combinators
Sept 4, 2001
ICFP, Florence, Italy
4
Behaviors
 Continuous behaviors capture any time-varying
quantity, whether:



input (sonar, temperature, video, etc.),
output (actuator voltage, velocity vector, etc.), or
intermediate values internal to a program.
 Operations on behaviors include:


Generic operations such as arithmetic, integration, and
differentiation.
Domain-specific operations such as edge-detection and
filtering for vision, scaling and rotation for animation and
graphics, etc.
Sept 4, 2001
ICFP, Florence, Italy
5
Events
 Discrete event streams include user input as well as domainspecific sensors, asynchronous messages, interrupts, etc.
 They also include tests for dynamic constraints on behaviors
(temperature too high, level too low, etc.)
 Operations on event streams include:


Mapping, filtering, reduction (?), etc.
Reactive behavior modification (next slide).
Sept 4, 2001
ICFP, Florence, Italy
6
Reactive Control of Continuous Values
One animation example that demonstrates
key aspects of FRP:
growFlower = stretch size flower
where size = 1 + integral bSign
bSign =
0 `until`
(lbp ==> -1 `until` lbp ==> bSign) .|.
(rbp ==> 1 `until` rbp ==> bSign)
Sept 4, 2001
ICFP, Florence, Italy
7
Applications of FRP
 Fran is a DSL for graphics and animation.
 Frob is a DSL for robotics.
 FranTk and Fruit are two DSL’s for graphical user
interfaces.
 FVision is a DSL for vision.
 FRP is the essence of Fran, Frob, FranTk, Fruit,
and FVision:





Fran
Frob
FranTk
Fruit
FVision
Sept 4, 2001
= FRP + graphics engine + library
= FRP + robot controller + library
= FRP + Tk substrate + library
= FRP + Java 2D substrate + library
= FRP + XVision + library
ICFP, Florence, Italy
8
Domain-Specific Languages
FVision
Fruit
FranTk
Frob
Fran
Graphics, Robotics, GUIs, Vision
Specialized languages
Continuous behaviors
and discrete reactivity
FRP
Functional Programming
Sept 4, 2001
Applications
ICFP, Florence, Italy
Functions, types, etc.
(Haskell)
9
Crouching Robots, Hidden Camera
 RoboCup


Two teams of soccer-playing robots, colormarked for ID/orientation
Overhead camera is the only sensor
camera
Team A
ctrlr
Team B
ctrlr
radio
Sept 4, 2001
radio
ICFP, Florence, Italy
10
Yale RoboCup Team
 FRP used in all parts of the system:



FVision for sensing
Frob for robot controlling
E-FRP (on-going work) for the on-board microcontroller
Sept 4, 2001
ICFP, Florence, Italy
11
The Problem
 FRP cannot guarantee bound on space/time




Program can diverge
Program can take unreasonable amount of time to
respond to a stimulus
Program can use huge amount of memory
Program can have hard-to-find space leaks
 Goal: to extend FRP for real-time
applications
Sept 4, 2001
ICFP, Florence, Italy
12
Our Goal
 How do we make FRP run fast?
 How do we make guarantees about both time and
space behavior?
 How does FRP relate to other models of hybrid
automata?
 Can FRP be used for embedded systems?
 And at a more abstract level:
What is an operational semantics for FRP?
Our goal:
Real-Time FRP, a subset of FRP, with
guaranteed bounds on execution
time and space, and deadlock free.
Sept 4, 2001
ICFP, Florence, Italy
13
Real-Time FRP (RT-FRP)
 Reactive language + base language
 Reactive language



Expressive: two forms of recursion
Space bounded
Time bounded
 Base language

Can be instantiated to any resource-bounded
language
Sept 4, 2001
ICFP, Florence, Italy
14
Syntax of Base Language
 Syntax of the sample base language:
(“lifted” terms are just “Maybe” type)
 Syntax of values in the sample base
language:
Sept 4, 2001
ICFP, Florence, Italy
15
Syntax of Reactive Language
 Syntax of signals:
 let-signal exports to the base language
 ext imports from the base language
Note: “Event a” in FRP is isomorphic to “Behavior (Maybe a)”.
In RT-FRP we just combine them and call them “signals”.
Sept 4, 2001
ICFP, Florence, Italy
16
Operational Semantics
 A program is executed in discrete steps, driven by timestamped input values.
Given a time t and input i, a term s evaluates to a value v and is
updated to a new term s’.
 We write this as:
and
or, more compactly as:
where:
Sept 4, 2001
ICFP, Florence, Italy
17
Program Execution
 A proper RT-FRP program never terminates.
Its meaning is the infinite sequence of
values, or “observations” that it yields.
 The sequence:
t0,i0
t1,i1
t2,i2
s0 v1, s1 ; s1  v2, s2 ; s2  v3, s3 ; …
 Meta-comment: Program output depends on
the time-stamped input pairs (tj,ij).
Sept 4, 2001
ICFP, Florence, Italy
18
Some Semantic Rules
Sept 4, 2001
ICFP, Florence, Italy
19
Snapshot
 Recursion form #1: recursive signal
Sept 4, 2001
ICFP, Florence, Italy
20
Swtich
 Delayed switching
 Allows self-reacting signals
let snapshot x  s1 switch on (when (x>100)) in s2 …
Sept 4, 2001
ICFP, Florence, Italy
21
Continuation
 Delayed switching too
 Recursion form #2: tail signals
Sept 4, 2001
ICFP, Florence, Italy
22
Intuition for Continuation
 Hybrid automaton


Continuations are modes
s in “s until <evj => kj>” defines the behavior
within a mode
 Goto statement


Continuations are labels
No need for stack
Sept 4, 2001
ICFP, Florence, Italy
23
For Example
 A simple model of a thermostat:
let snapshot temp 
let continue k1 () = <heating-model>
until when (temp>t) => k2
k2 () = <cooling-model>
until when (temp<t-hys) => k1
in t0 until startev => k1
in ext temp
Sept 4, 2001
ICFP, Florence, Italy
24
From FRP to RT-FRP
 Many FRP constructs can be expressed in
RT-FRP as macros

Lifting

When
Sept 4, 2001
ICFP, Florence, Italy
25
More from FRP to RT-FRP
 How about integral?

the forward-Euler method:
 And etc.
Sept 4, 2001
ICFP, Florence, Italy
26
What Can Go Wrong?
 Recursive signals


Expressive
However, w/ recursion, term can get stuck immediately:
let snapshot x  ext x in …

Or get stuck after updating:
let snapshot f  delay id (ext (\y. f y)) in …
 let snapshot f  delay (\y. f y) (ext (\y. f y)) in …
 Solution:



Use type system to disallow “direct” recursions, thus
preventing “deadlock”
Ensures delay/switch/until appear somewhere in a
recursive signal
Restricts delay to non-functional types
Sept 4, 2001
ICFP, Florence, Italy
27
What Can Go Wrong? (cont’d)
 Tail signals


Adds expressive power
However, w/ tail signals, term size can grow
let continue { k x = f (s until ev => k) } in (s until ev => k)

let continue { k x = f (s until ev => k) } in f (s until ev => k)

let continue { k x = f (s until ev => k) } in f (f (s until ev => k))
…

There are other ways for a term to grow
 Solution


Restrict by syntax and type system
Inspired by tail recursion
Sept 4, 2001
ICFP, Florence, Italy
28
Types
 Syntax of types
 Annotated types:

Local/exportable:
 Contexts
/
 Expose( )/export( )
 Judgments:
“e is a base language term of type g”
“s is a signal carrying values of type g”
Sept 4, 2001
ICFP, Florence, Italy
29
Some Typing Rules
Where b is a base (non-functional) type:
Sept 4, 2001
ICFP, Florence, Italy
30
Some Typing Rules
Where b is a base (non-functional) type:
Sept 4, 2001
ICFP, Florence, Italy
31
More typing rules
 Let-continue:
 until:
Sept 4, 2001
ICFP, Florence, Italy
32
More typing rules
 Let-continue:
 until:
Sept 4, 2001
ICFP, Florence, Italy
33
Key Results
 Type safety / preservation

thus no core dumps!
 Each step takes bounded amount of time

thus no time leaks!
 Term size cannot exceed a bound

thus no space leaks!
 In addition, using a type system, progress is
guaranteed

thus no deadlock!
Sept 4, 2001
ICFP, Florence, Italy
34
Future Work on RT-FRP






Enrich language for practical use.
Compile into lower-level code (C, etc.).
Examine sensor / behavior fusion.
Consider embedded systems.
Better formulation of well-formed recursion.
Test case: compile to PIC micro-controller on
our “soccer-bots”.
Sept 4, 2001
ICFP, Florence, Italy
35