Transcript PowerPoint Presentation - Evaluation Strategies for

Hume: a Domain-Specific Language for
Programming with Bounded Resource
Kevin Hammond,
Pedro Vasconcelos, Sun Meng, Roy Dyckhoff,
Leonid Timochouk
University of St Andrews, Scotland
Greg Michaelson, Andy Wallace,
Robert Pointon, Graeme McHale, Chunxiu Liu
Heriot-Watt University, Scotland
Jocelyn Sérot, Norman Scaife
LASMEA, Clermont-Ferrand, France
Martin Hofmann, Hans-Wolfgang Loidl
Ludwig-Maximilians Universität, München, Germany
Christian Ferdinand, Reinhold Heckmann
AbsInt GmbH, Saarbrücken, Germany
http://www.hume-lang.org
Scotland
Highlands
Speyside
St Andrews, 1411
Glasgow, 1452
Lowlands
Kevin Hammond, University of St Andrews
Edinburgh, C18th
Slide 2
Hume
Higher-order Uniform Meta-Environment
David Hume
Scottish Enlightenment Philosopher
and Sceptic
1711-1776
Funded by
€1.3M grant under EU Framework VI
EmBounded: IST-2004-510255, 2005-2008
Qui ckTime™ and a
TIFF (LZW) decompr essor
are needed to see this pi cture.
£200K grants from the UK’s EPSRC
Cost modelling for resource-bounded systems, 2002-2005
MetaHume: EP/C001346/0, 2005-2008
Travel grants from the British Council, CNRS etc.
Hume Research Objectives
• Real-Time, Hard Space Functional Programming
• Virtual Testbed for Space/Time Cost Modelling
• Generative, Domain-Specific Language Design
Kevin Hammond, University of St Andrews
Slide 5
Overview
1. Hume Language Design and Examples
2. Stack and Heap Usage for Primitive Recursive Programs
1. Cost Model
2. Inference Algorithm (Type-and-Effect System)
3. Results of the Analysis
4. Conclusions and Further Work
Kevin Hammond, University of St Andrews
Slide 6
Hume Design Domain (1)
Quic kT ime™ and a YUV420 codec decompress or are needed to s ee this pi cture.
Kevin Hammond, University of St Andrews
Slide 7
Hume Design Domain (2)
Kevin Hammond, University of St Andrews
Slide 8
The Embedded Systems
Domain
• Some Facts
–
–
–
–
98% of all processors are used in embedded systems
by 2005, there will be 280 processors in the average home
by 2010 the number of processors produced each year will double
75% of all processors are 8-bit or 16-bit designs
• And there are some sexy applications
– CPUs found in mobile phones, DVD players, set-top boxes, ....
– and in mundane devices: washing machines, cookers, refrigerators,cars ...
Kevin Hammond, University of St Andrews
Slide 9
State of the Art...
• Embedded Systems Engineering
–
–
–
–
big trend to high level software design (UML etc.)
80% of all embedded software is now written in C/C++
75% of embedded software is delivered late
bugs can cost $14,000 each to fix!
• A Major Problem with C/C++ is Poor Memory Management
– explicit allocation, deallocation
– pointer following
– etc. etc.
• No Accurate Method for Determining Memory Usage
– profiling, guesswork(!!), approximation
Kevin Hammond, University of St Andrews
Slide 10
A New Direction?
Kevin Hammond, University of St Andrews
Slide 11
Hume Design Objectives
• Targets embedded/critical applications
Reliability,
Expressibility,
Controllability,
Predictability,
Costability
– Hard real-time target
– Formally bounded time and space
– I/O managed through low-level “ports”/“streams”
» Memory-mapped, timed, interrupts or devices
– Asynchronous concurrency model (multicore?)
– Simple, easily costed, exception handling mechanisms
– Transparent design and implementation: correctness by construction
– uses Haskell FFI to allow external calls in C/assembler etc.
• High level of expressiveness/productivity
–
–
–
–
–
Rule-based system: concise & clear using functional notation
Runtime errors reduced by strong polymorphic types
Structured reuse through higher order functions
Thread management simplified by implicit concurrency/parallelism
Elimination of memory errors through automatic memory management
Kevin Hammond, University of St Andrews
Slide 12
FSA-derived Notation
• Based on generalised Mealy machines (see Michaelson et al. 2003)
• Boxes encapsulate a set of rules each mapping inputs to outputs
• Multiple inputs/outputs are grouped into tuples
box b ...
match
(patt11, ..., patt1k) -> (expr11, ..., expr1m)
|
...
|
(pattn1, ..., pattnk) -> (expr11, ..., exprnm)
;
•
•
•
•
Sets of boxes are wired into static process networks (automata)
Boxes repeat indefinitely once a result is produced (tail recursion)
Boxes are asynchronous (ignored inputs/outputs)
Wires are single-buffered
Kevin Hammond, University of St Andrews
Slide 13
Hume Language Structure
inport1
• Boxes structure processes
box1
– Static process network
– Asynchronous communication
– Stateless
• Functions structure computations
– Purely functional notation
– Pattern-matching relates inputs/outputs
through functional expressions
box2
box3
outport1
Kevin Hammond, University of St Andrews
outport2
Slide 14
Hume Language Structure
Declaration & Metaprogramming Layer
Coordination Layer
Expression Layer
Kevin Hammond, University of St Andrews
Slide 15
Expression Layer
• Purely functional, strict, higher-order, polymorphic, stateless
• Matches are total
• Timeouts/space overflows are managed through exceptions
varid expr1 … exprn
-- function/constructor application
(expr1, …, exprn)
-- tuples
< expr1, …, exprn >
-- vectors (sized)
[ expr1, …, exprn ]
-- lists (bounded)
let decls in expr
-- local value declarations
expr within cexpr
-- timeout/space restriction
if expr then expr else expr -- conditional expression
case expr of matches
-- case expression
expr :: type
-- type cast
expr as type
-- type coercion (cost implication)
Kevin Hammond, University of St Andrews
Slide 16
Example: Parity Checker
type Bit = word 1;
type Parity = boolean;
comm1
parity true = (“true”,true);
parity false = (“false”,false);
b
box even_parity2
in (b::Bit, p::Parity)
out (show::string, p'::Parity)
match
(0,true)
| (1,true)
| (0,false)
| (1,false)
->
->
->
->
parity
parity
parity
parity
true
false
false
true;
p (true,…)
even_parity2
p’
comm2
wire even_parity2 (comm1, even_parity2.p' initially true)
(comm2, even_parity2.p);
Kevin Hammond, University of St Andrews
Slide 17
Hume Language Levels
Full Hume
PR-Hume
HO-Hume
FSM-Hume
HW-Hume
Kevin Hammond, University of St Andrews
Full Hume
recursive functions
recursive data structures
PR-Hume
primitive-recursive functions
primitive-recursive data structures
HO-Hume
higher-order non-recursive functions
non-recursive data structures
FSM-Hume
1st-order non-recursive functions
non-recursive data structures
HW-Hume
no functions
non-recursive data structures
Slide 18
Metaprogramming Example:
Fair Merge
template merge
in (in1 :: int 32, in2 :: int 32)
out (o :: int 32)
fair
(x,*)
| (*,y)
sysin1
in1
sysin2
in2
sysin3
m{1}
o
-> x
-> y;
instantiate merge as m * 2;
in1
in2
m{2}
o
sysout
wire M(b,inp1,inp2,outp) = b (in1, in2) (outp);
wire M(m{1}, sysin1, sysin2, m{2}.in1);
wire M(m{2}, m{1}.o, sysin3, sysout);
Kevin Hammond, University of St Andrews
Slide 19
Exception Handling
• Handled at box level
– one exception handler per box
– no nested exceptions
• Low Cost Implementation
box ::=
“box”
boxid
“in”
ins
“out”
outs
[ “handles” exnids ]
( “match” | “fair” )
[ “handle” handlers ]
matches
– implemented as branch
– handlers must have trivially bounded cost
expr ::=
“raise”
handlers ::=
handler1 "|" ... "|" handlern
handler ::=
exnid patt "->" cexpr
Kevin Hammond, University of St Andrews
expr | ...
Slide 20
Exception Handling Example
f n = ...;
box overflow
in (c :: char)
out (v :: string 29)
handles TimeOut, HeapOverflow
match
n ->
c
overflow
v
f n within 100us within 10KB heap
handle TimeOut x -> ”Timed Out: " ++ show x
|
HeapOverflow x -> ”Heap Overflow: " ++ show x;
Kevin Hammond, University of St Andrews
Slide 21
Research Problems
• Construct layered cost models for Hume levels
– Source-based
– Expose and solve costs for PR programs
• Stage Costs through Hume levels
– allow use of software defined at higher levels
– automatic (formal) translation from high to low level
– may increase code size and costs
• Resource-aware abstract machine
– expose resource usage
– allow compiler optimisations
Kevin Hammond, University of St Andrews
Slide 22
Predicting the Cost
?
Kevin Hammond, University of St Andrews
Slide 23
A Type-and-Effect
Space Cost Model
• Relates language structure to <heap, max stack> usage
– operational semantics expressed using sequent style
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Both heap and stack
can be cleared after
a single box step
Stack; Heap
• Tuned to prototype Hume abstract machine interpreter
– allows accuracy to be measured
– can be exploited by compiler
Derived from
theoretical
work on cost
analysis for parallel
programs
Kevin Hammond, University of St Andrews
Slide 24
Sized Types
• Types are annotated with sizes
– magnitude of natural
– length of a list
10 :: Nat10
[6,1,2] :: [Nat6 ]3
• Sizes can be weakened to any greater size
– defined as a subtyping relation
– so 10 :: Nat11 but not 10 :: Nat9
–  means unknown size, greater than any other size, so 10 :: Nat
–  means undefined size, less than any other size
• Will be used to determine recursion bounds
Kevin Hammond, University of St Andrews
Slide 25
Latent Costs
• Define costs for functions
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
• Allow costs to be captured for higher-order functions
Kevin Hammond, University of St Andrews
Slide 26
Types and Effects for
Stack/Heap Usage
• Size/Cost Expressions
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
• Types and Effects
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Kevin Hammond, University of St Andrews
Slide 27
Cost Rules: Basic Expressions
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Kevin Hammond, University of St Andrews
Slide 28
Cost Rules: Conditionals/Cases
are needed to see this picture.
TIFF (LZW) decompressor
QuickTime™ and a
Kevin Hammond, University of St Andrews
Slide 29
Cost Rules:
Function Applications
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Kevin Hammond, University of St Andrews
Slide 30
Cost Rules: Function Decls
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Kevin Hammond, University of St Andrews
Slide 31
Cost Inference
• Restrict cost annotations in types to be variables
• Separately collect constraints on variables
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
• So, standard unification can be used on types
• Constraints must be solved to determine closed costs
Kevin Hammond, University of St Andrews
Slide 32
Cost Inference
• Restrict cost annotations in types to be variables
• Separately collect constraints on variables
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
• So, standard unification can be used on types
• Constraints must be solved to determine closed costs
Kevin Hammond, University of St Andrews
Slide 33
Solving Recurrences
• For recursive programs, the effect system generates
recurrence relations on constraints
• These are solved to give closed forms
– use e.g. Mathematica, called during cost analysis
– use an “oracle” of known recurrences
– write a new recurrence solver
• Constraints are monotonically increasing
Kevin Hammond, University of St Andrews
Slide 34
Example: Length
• For the recursive length function
length [] = 0;
length (x:xs) = 1 + length xs;
{stack,heap}
• The type inferred is:
length ::
[t7]^x21-{x19,x20}->nat^x27,
{x19 >=7+6*x21, x20 >=2+4*x21,x27>=x21}
Kevin Hammond, University of St Andrews
Slide 35
Example: Take
• For the recursive take function
take n [] = [];
take n (x : xs) =
if n > 0 then (x : take (n-1) xs) else [];
• The type inferred is:
take ::
nat^x53-{x51,x52}->[t118]^x56
-{x54,x55}->[t118]^x62,
{x51>=0,x52>=0,x54>=10+9*min(x53,x56),
x55>=7+13*min(x53,x56),x62>=min(x53,x56)}
Kevin Hammond, University of St Andrews
Slide 36
Example: Twice/Map
• For the Higher-Order twice and map2 functions
twice f x = f (f x);
map2 f [] = [];
map2 f (x:[]) = [f x];
map2 f (x:(y:[])) = [f x,f y];
add1 x = 1+x;
h x = map2 (twice add1) x;
• The types inferred are:
twice ::
map1 ::
add1 ::
h ::
(t21-{x14,x15}->t21)-{x2,x3}->t21-{x4,x5}->t21,
{x2>=0,x3>=0,x4>=6+max(1+x14,1),x5>=x15+x15}
(t54-{x62,x63}->t73)-{x45,x46}->[t54]^x64
-{x47,x48}->[t73]^x65,
{x45>=0,x46>=0,x47>=6+max(1+max(1+x62,1),2),
x48>=max(8+x63,3),x65>=1}
int-{x23,x24}->int, {x23>=7,x24>=4}
[int]^x112-{x75,x76}->[int]^x113,
{x75>=30,x76>=25,x113>=1}
Kevin Hammond, University of St Andrews
Slide 37
Results
!
Kevin Hammond, University of St Andrews
Slide 38
Results
function
length:
length:
length:
length:
heap (est)
10
100
1000
10000
reverse: 10
reverse: 100
reverse: 1000
twice/map2: 1
twice/map2: 2
lift
181(181)
1711(1711)
17011(17011)
170011(170011)
381(381)
26862(26862)
2518512(2518512)
25(25)
38(38)
129(144)
Kevin Hammond, University of St Andrews
stack(est)
heap(GHC -O2)
72(72)
612(612)
6012(6012)
60012(60012)
1632
2357
15630
141626
88(98)
810(813)
8008(8013)
2080
35395
3051874
30(30)
30(30)
89(89)
1564
1592
-Slide 39
Results (Pump)
• Cost model applied to mine drainage example
2.6KB
v. 2.4KB
– implemented in prototype Hume abstract machine compiler
– compared with measured dynamic runtime costs
box
pump
environ
water
logger
others
wires
totals
heap est heap actual
47
49
54
119
115
96
480
Kevin Hammond, University of St Andrews
38
47
54
105
106
84
434
9%
stack est stack actual
17
29
24
39
70
179
17
29
24
31
70
171
Slide 40
The Reality
!!
Kevin Hammond, University of St Andrews
Slide 41
RTLinux Memory Usage (Pump)
Module
hume_module
rtl_sched
rtl_fifo
rtl_posixio
rtl_time
rtl
text
30146
data
52
Size
61904
43200
10016
7232
10064
27216
bss
30048
Kevin Hammond, University of St Andrews
Used by
0 (unused)
0 [hume_module]
0 [hume_module]
0 [rtl_fifo]
0 [hume_module rtl_sched rtl_posixio]
0 [hume_module rtl_sched rtl_fifo
rtl_posixio rtl_time]
dec
60246
hex
eb56
filename
hume_module.o
Slide 42
Vehicle Sim. Statistics
Thu Aug 21 19:06:06 BST 2003
Box Statistics:
control: MAXRT = 53120ns, TOT = 1960041024ns, MAXHP = 57, MAXSP = 36
env:
MAXRT = 9101600ns, TOT = 1580087776ns, MAXHP = 49099, MAXSP = 129
vehicle: MAXRT = 2973120ns, TOT = 2269933760ns, MAXHP = 49164, MAXSP = 133
Box heap usage: 98440 (99414 est)
Box stack usage: 298 (319 est)
Stream/MIDI Statistics:
output1: MAXRT = 22688ns, TOT = 3188562720ns, MAXHP = 71, MAXSP = 1
...
Kevin Hammond, University of St Andrews
Slide 43
Vehicle Sim. Statistics (2)
Wire Statistics:
control.0:
env.0: MAX
vehicle.0:
vehicle.1:
vehicle.2:
vehicle.3:
MAX DELAY = 24544ns, MAXHP =
DELAY = 67072ns, MAXHP = 11
MAX DELAY = 33056ns, MAXHP =
MAX DELAY = 32448ns, MAXHP =
MAX DELAY = 9118688ns, MAXHP
MAX DELAY = 9135968ns, MAXHP
47
47
2
= 11
= 2
Total heap usage: 197022 (199078 est)
Total stack usage: 597 (640 est)
Sat Aug 23 06:46:19 BST 2003
Kevin Hammond, University of St Andrews
Slide 44
Related Work (Analysis)
• Regions (Tofte)
– explicit labelled memory areas, automatic deallocation
• Cyclone (Morrissett)
– C syntax, region inference
• Sized Types (Hughes & Pareto)
– properties of reactive systems, progress, not inference, not cost
• Camelot/GRAIL (Sannella, Gilmore, Hofmann et al.)
– stack/heap inference from JVM bytecode, parametric costs, tail recursion
• Worst-Case Execution Time Analysis (Wellings et al)
– Java/Ada, probabilistic cache/execution costs
Kevin Hammond, University of St Andrews
Slide 45
Conclusions
• Cost Analysis for
Primitive Recursive, Higher-Order, Polymorphic Functions
– strict, purely functional notation
– generates cost equations plus recurrences
» recurrences solved by reference to an oracle or external solver
– soundness results under construction
• Good Practical Results Obtained in a number of cases
– no loss of accuracy for non-recursive definitions
– exact worst-case solutions obtained for many definitions
– size-aliasing can cause problems for composing polymorphic definitions
Kevin Hammond, University of St Andrews
Slide 46
Further Work/Work in Progress
• Modelling
– soundness proofs
» under construction
• extends Hughes/Pareto MML to inference, different cost domain
• many technical problems solved, some remaining
–
–
–
–
resolve size aliasing problem
extend to general data structures
investigate Presburger arithmetic
application to other language paradigms: non-strict, object-oriented, C/C++
• Real-Time Models
– Predictive real-time models need better hardware (especially cache) models
– alternative real-time scheduling algorithms should be tried
• 1.3MEuro Framework VI Project (FET-OPEN)
– with Jocelyn Sérot (LASMEA, France), Martin Hofmann (Ludwig-Maximilians Univerität,
Germany) and AbsInt GmbH (Saarbrücken, Germany)
Kevin Hammond, University of St Andrews
Slide 47
Recent Papers
Inferring Costs for Recursive, Polymorphic and Higher-Order Functional Programs
Pedro Vasconcelos and Kevin Hammond
To appear in Proc. 2003 Intl. Workshop on Implementation of Functional Languages (IFL ‘03), Edinburgh,
Springer-Verlag LNCS, 2004. Winner of the Peter Landin Prize for best paper
Hume: A Domain-Specific Language for Real-Time Embedded Systems
Kevin Hammond and Greg Michaelson
Proc. 2003 Conf. on Generative Programming and Component Engineering (GPCE 2003), Erfurt, Germany,
Springer-Verlag LNCS, Sept. 2003. Proposed for ACM TOSEM Fast Track Submission
FSM-Hume: Programming Resource-Limited Systems using Bounded Automata
Greg Michaelson, Kevin Hammond and Jocelyn Sérot
Proc. 2004 ACM Symp. on Applied Computing (SAC ‘04), Nicosia, Cyprus, March 2004
The Design of Hume
Kevin Hammond
Invited chapter in Domain-Specific Program Generation,
Springer-Verlag LNCS State-of-the-art Survey, C. Lengauer (ed.), 2004
Predictable Space Behaviour in FSM-Hume”,
Kevin Hammond and Greg Michaelson,
Proc. 2002 Intl. Workshop on Implementation of Functional Languages (IFL ‘02), Madrid, Spain, Sept. 2002,
Springer-Verlag LNCS 2670, ISBN 3-540-40190-3,, 2003, pp. 1-16
Kevin Hammond, University of St Andrews
Slide 48
http://www.hume-lang.org
Kevin Hammond, University of St Andrews
Slide 49
Hume
Higher-order Uniform Meta-Environment
David Hume
Scottish Enlightenment Philosopher
and Sceptic
1711-1776