Scrapping Your Inefficient Engine
0 likes282 views
The document describes an approach to implementing embedded domain specific languages (EDSLs) using dependent types for precise language implementation and partial evaluation for efficient language implementation. It presents an EDSL for implementing a reliable network transport protocol as an example. Partial evaluation of the EDSL interpreter specialized for concrete EDSL programs results in significantly more efficient executable code compared to the general interpreter. Guidelines are provided for EDSL developers to fully exploit partial evaluation.
![Network Protocol EDSL Interpreter
The interpreter for ARQ is parameterised over the actual
network data, and keeps track of time to check for
timeouts.
params (s:Socket, host:String, port:Int) {
interpBy : Time -> (prog:ARQ st st t) [static] ->
IO (Maybe t);
...
interpBy t END
= checkTime t (sendPacket s host port (CTL S_BYE));
...
}
checkTime : Time -> (IO t) -> IO (Maybe t);
ICFP 2010, September 29th 2010 p.9/20](https://image.slidesharecdn.com/icfp10-100929165445-phpapp02/85/Scrapping-Your-Inefficient-Engine-9-320.jpg)
![[JavaOne 2011] Models for Concurrent Programming](https://cdn.slidesharecdn.com/ss_thumbnails/24881-modelsforconcurrentprogramming-111019034625-phpapp02-thumbnail.jpg?width=560&fit=bounds)
More Related Content
What's hot (10)
Viewers also liked (13)
Similar to Scrapping Your Inefficient Engine (20)
Scrapping Your Inefficient Engine
- 1. Scrapping Your Inef鍖cient Engine Using Partial Evaluation to Improve Domain Speci鍖c Language Implementation Edwin Brady and Kevin Hammond eb@cs.st-andrews.ac.uk University of St Andrews ICFP 2010, September 29th 2010 ICFP 2010, September 29th 2010 p.1/20
- 2. Introduction We will describe an approach to Embedded Domain Speci鍖c Language (EDSL) development, combining two technologies: Dependent Types for precise language implementation Partial Evaluation for ef鍖cient language implementation We will use I DRIS, an experimental language with full dependent types. (http://www.idris-lang.org/; cabal install idris) ICFP 2010, September 29th 2010 p.2/20
- 3. Some Idris Features I DRIS has several features to help support EDSL implementation. . . Full-Spectrum Dependent Types Compile-time evaluation Ef鍖cient executable code, via C Uni鍖cation (type/argument inference) Plugin decision procedures Overloadable do-notation, idiom brackets Simple foreign function interface . . . and I try to be responsive to feature requests! ICFP 2010, September 29th 2010 p.3/20
- 4. A Recipe for EDSLs Our motivation is a desire to reason about extra-functional properties of resource-aware programs. The recipe is: 1. Design an EDSL which guarantees the resource constraints, represented as a dependent type 2. Implement the interpreter for that EDSL 3. Specialise the interpreter for concrete EDSL programs, using a partial evaluator To illustrate this, we present a simple implementation of a reliable (ARQ) network transport protocol. ICFP 2010, September 29th 2010 p.4/20
- 5. Session State ICFP 2010, September 29th 2010 p.5/20
- 6. Transmission State ICFP 2010, September 29th 2010 p.6/20
- 7. Network Protocol EDSL data ARQ : State -> State -> Set -> Set where START : ARQ CLOSED OPENING () | START_RECV_ACK : (if_ok : ARQ (OPEN (Ready First)) st t) - (on_timeout : ARQ OPENING st t) -> ARQ OPENING st t | END : ARQ (OPEN (Ready n)) CLOSING () | END_RETRY : ARQ CLOSING CLOSING () | END_RECV_ACK : (if_ok: ARQ CLOSED st t) -> (on_timeout: ARQ CLOSING st t) -> ARQ CLOSING st t ... ICFP 2010, September 29th 2010 p.7/20
- 8. Network Protocol EDSL data ARQ : State -> State -> Set -> Set where ... | WITHIN : Time -> (action : ARQ st st t) -> (on_timeout : ARQ st st t) -> ARQ st st t | IF : Bool -> (if_true : ARQ st st t) -> (if_false : ARQ st st t) -> ARQ st st t | RETURN : t -> ARQ st st t | BIND : ARQ st st t -> (k : t -> ARQ st st t) -> ARQ st st t; ICFP 2010, September 29th 2010 p.8/20
- 9. Network Protocol EDSL Interpreter The interpreter for ARQ is parameterised over the actual network data, and keeps track of time to check for timeouts. params (s:Socket, host:String, port:Int) { interpBy : Time -> (prog:ARQ st st t) [static] -> IO (Maybe t); ... interpBy t END = checkTime t (sendPacket s host port (CTL S_BYE)); ... } checkTime : Time -> (IO t) -> IO (Maybe t); ICFP 2010, September 29th 2010 p.9/20
- 10. Sending Packets An example program, which opens a connection, sends a batch of packets, then closes it, within i microseconds: sendNumber : Time -> Nat -> ARQ CLOSED CLOSED (); sendNumber i tot = WITHIN i (do { open_connection 500000; session 500000 O tot First; close_connection 500000; (TRACE "Timed out"); The types ensure that the protocol is followed; any protocol violation is a type error. ICFP 2010, September 29th 2010 p.10/20
- 11. Sending Packets The following function sends tot packets, with no payload, with timeout i per packet. session : Time -> Nat -> Nat -> (sq:Seq) -> ARQ (OPEN (Ready sq)) CLOSING (); session i n tot sq = IF (n == tot) END (do { TRACE ("Sending " ++ showNat n); send sq i; session i (S n) tot (Next sq); }); This program is recursive and not obviously terminating. ICFP 2010, September 29th 2010 p.11/20
- 12. Sending Packets (Specialised) Partial evaluation of the ARQ interpreter with this program yields: sessionS : Socket -> String -> Int -> Time -> Time -> Nat -> Nat -> Seq -> IO (Maybe ()); sessionS s h p t i n tot sq = do { checkTime t (if (n == tot) then checkTime t (sendPacket s h p (CTL S_BYE)) else do { putStr ("Sending " ++ showNat n); checkTime t (sendS s h p t sq i); checkTime t (sessionS s h p t (S n) i tot (Next sq))); } ICFP 2010, September 29th 2010 p.12/20
- 13. Partial Evaluation In order to achieve this result, we: Changed the evaluator to allow caching of intermediate results Cache intermediate results for functions with declared static arguments This speci鍖cally prevents in鍖nite unfolding of recursive calls Host languages job details in the paper Followed some clearly de鍖ned guidelines when implementing the interpreter EDSL developers job details in the paper ICFP 2010, September 29th 2010 p.13/20
- 14. Results Run time, in seconds of user time, for a variety of DSL programs: Program Spec Gen Java C fact1 0.017 8.598 0.081 0.007 fact2 1.650 877.2 1.937 0.653 sumlist 3.181 1148.0 4.413 0.346 copy 0.589 1.974 1.770 0.564 copy_dynamic 0.507 1.763 1.673 0.512 copy_store 1.705 7.650 3.324 1.159 sort_file 5.205 7.510 2.610 1.728 ARQ 0.751 0.990 ICFP 2010, September 29th 2010 p.14/20
- 15. Results Run time, in seconds of user time, for a variety of DSL programs: Program Spec Gen Java C fact1 0.017 8.598 0.081 0.007 fact2 1.650 877.2 1.937 0.653 sumlist 3.181 1148.0 4.413 0.346 copy 0.589 1.974 1.770 0.564 copy_dynamic 0.507 1.763 1.673 0.512 copy_store 1.705 7.650 3.324 1.159 sort_file 5.205 7.510 2.610 1.728 ARQ 0.751 0.990 ICFP 2010, September 29th 2010 p.15/20
- 16. Results Run time, in seconds of user time, for a variety of DSL programs: Program Spec Gen Java C fact1 0.017 8.598 0.081 0.007 fact2 1.650 877.2 1.937 0.653 sumlist 3.181 1148.0 4.413 0.346 copy 0.589 1.974 1.770 0.564 copy_dynamic 0.507 1.763 1.673 0.512 copy_store 1.705 7.650 3.324 1.159 sort_file 5.205 7.510 2.610 1.728 ARQ 0.751 0.990 ICFP 2010, September 29th 2010 p.16/20
- 17. Conclusions I DRISs type system occupies a sweet spot where partial evaluation is particularly effective. Tagless interpreters Existing evaluator; only minor changes required Comparable performance to hand written C/Java . . . . . . but veri鍖ed resource usage, via EDSLs This is not unique to I DRIS! Techniques equally applicable to Agda, Coq, Guru, Trellys, Haskell (with GADTs). . . ICFP 2010, September 29th 2010 p.17/20
- 18. . . . and 鍖nally I have been packaging and documenting I DRIS. Please give it a go! cabal install idris http://www.idris-lang.org/ http://www.idris-lang.org/tutorial/ Thank you for your attention. ICFP 2010, September 29th 2010 p.18/20
- 19. Partial Evaluation Guidelines An EDSL developer can fully exploit partial evaluation by following these guidelines: 1. Index the EDSL representation by its type 2. The interpreter must only pattern match on the EDSL program to be translated 3. Auxiliary functions which match on dynamic data must not be passed EDSL code 4. Ensure that all of program construction, generation and transformation can be evaluated statically Note: this rules out higher order functions, for the moment! ICFP 2010, September 29th 2010 p.19/20
- 20. Network Protocol EDSL data ARQ : State -> State -> Set -> Set where ... | SEND : Packet -> ARQ (OPEN (Ready n)) (OPEN (Waiting n)) () | RESEND : Packet -> ARQ (OPEN (Waiting n)) (OPEN (Waiting n)) () | RECV_ACK : (if_ok : ARQ (OPEN (Ready (Next n))) st t (on_timeout : ARQ (OPEN (Waiting n)) st t) -> ARQ (OPEN (Waiting n)) st t ... ICFP 2010, September 29th 2010 p.20/20