ReactiveML, a Reactive Extension to ML∗
Contents
1. H present e then e1 else e2 T H F do e until e1 unit H F do e when e1 unit Figure 6 The Type System of active cells 0 4 42 60 83 OCAML 0 74 s 0 75 s 0 76 s 0 77 s 0 77 s LOFT 0 02 s 0 11 s 0 93 s 1 57 s 2 09 s REACTIVEML 0 05 s 0 08 s 0 89 s 1 46 s 1 94 s Figure 7 Average of execution time of one instant for a 500x500 Fredkin s cellular automata written in C The main application written in REACTIVEML is a simula tor of a complex network routing protocol for mobile ad hoc networks 3 19 done in collaboration with F Benbadis from the Network team at LIP6 Paris Mobile ad hoc networks are highly dynamic networks characterized by the absence of physical infrastructure In such networks every node is able to move nodes evolve concurrently and synchro nize continuously with their neighbors Due to mobility con nections in the network can change dynamically and nodes can be added or removed at any time All these character istics concurrency with many communications and the need of complex data structure combined to the routing protocol specifications make the use of standard simulation tools e g NS OPNET inadequate and network protocols appear to be very hard to program efficiently in conventional programming languages This experiment showed that the reactive model as introduced by Boussinot strongly matters for programming those2. The details of the proofs are given in an extended version of the paper 20 5 It is available at www spi lip6 fr mandel rml 6 STATIC TYPING We provide a type system as a conservative extension of the Milner type system of ML 21 In doing so we have to deal with signals and in particular values which can be transmitted on signals The type language is E s Vai Qn T T n Tla rt 77 7r x T process 7 7 event T x int bool Types are separated in regular types T and type schemes o A type T may be a basic type T a type variable a a function type T T2 a product type 71 X T2 or a pro cess type process or the type of a signal 71 72 event In the type of a signal 71 is the type of the emitted value and 72 is the type of the read value obtained after collecting all the emitted values during an instant A typing environment H has the following form H a 1 013 5 2k oF The instantiation and generalization is defined like the following T Ir1 ai Tn An lt Vai1 QK T Gen r H Vai n T where a1 ax FV r FV H Expressions are typed in an initial typing environment TC such that TC true bool fst Ya 6 a x B gt a Expressions are typed by asserting the judgment HF e 7 which states that the expression e has type 7 in the typing environment H The predicate is defined in figure 6 The typing rules for ML expressions are n
3. and the other queue is used for instructions that can wait for more than one instant e g do when Thus if the execution of some code is stopped on the test of a signal then the code to be executed is recorded in the appropriate waiting queue Otherwise its continuations are put in the set of actions to be executed in the current instant C Therefore the execution of an instant consists in the execution of all the ready actions of C The end of the instant is decided when C is empty Instructions which are in the short term waiting queues can be treated to prepare the next instant With this scheduling strategy a fast access to signals for presence information and waiting queues is crucial in order to obtain an efficient execution of programs Almost all im plementations of the reactive approach use dedicated hash tables during the execution for representing the signal envi ronment In our implementation signals are represented as regular values which are automatically garbage collected by OCAML when possible Moreover the presence information and associated waiting queues is done in constant time The efficient representation of signals together with the absence of busy waiting during the execution are central in order to be able to program real size problems Several applications have been written in REACTIVEML ranging from simple graphical systems to complex simula tion problems In particular we have rewritten classical cel l
4. be ei e2 The associativity and commutativity of the gathering func tion expresses the fact that the order of emissions during an instant is not specified It is a strong constraint But even if it is not satisfied a program can be deterministic For ex ample if there is no multi emissions the gathering function does not have to be associative and commutative LEMMA 2 For every expression e let S such that S 5 3E N b NH e e then there exists a unique smallest signal environment MS such that JE N b N F e ZB e ns The proof of this lemma is based on the following lemma which states that if an expression can react in two differ ent environments then it can react in the intersection of these environments This lemma is based on the absence of instantaneous reaction to the absence of a signal Indeed contrary to ESTEREL the absence of a signal can not gener ate the emission of other signals For example in ESTEREL the following program emits s2 if s1 is absent but in RE ACTIVEML the emission of s2 is delayed to the next instant such that the absence can emit signals during the instant present si then else emit s2 LEMMA 3 Let S S2 S3 and e such that Ny F e Ta 1 e and No F e 22 e2 and S3 SI N SJ then there 2 exists E3 N3 b3 and e3 such that N3 F e a e3 and 3 b3 gt b A b2 and E3 E E n E2 and N3 C Ni N N2 5 OPERATIONAL SEMANTICS The previous semantics is n
5. In this model time is defined logically as the sequence of reactions of the system to input events The main consequence of this model is to conciliate paral lelism allowing for a modular description of the system and determinism Moreover techniques were proposed for this parallelism to be statically compiled i e parallel pro grams are translated into purely sequential imperative code tLaboratoire d Informatique de Paris 6 Universit Pierre et Marie Curie 8 rue du Capitaine Scott 75015 Paris France email Louis Mandel Marc Pouzet lip6 fr This work is supported by the French ACI S curit Alidecs Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page To copy otherwise to republish to post on servers or to redistribute to lists requires prior specific permission and or a fee Copyright 200X ACM X XXXXX XX X XX XX 5 00 in terms of transition systems 5 14 Synchronous languages are restricted to the domain of real time systems and their semantics has been specifically tuned for this purpose In particular they forbid important features like recursion or dynamically allocated data in or der to ensure an execution in bounded time and memory In the 90 s Boussinot observed that
6. if the signal is present then the body must be activated at the end of instant If the signal is absent the body is not activated because it has not been activated during the instant 5 3 Execution of a Program The reaction of an instant is defined by the relation ei Si gt e Si If we note J the inputs of the reaction and O the outputs the signal environment have the following properties All the signals that are not in J are initially absent S I The outputs are a subset of the signal environment at the end of the reaction O E The default values and the gathering functions are kept for an instant to the other 5 G Shi and S C S The execution of an instant is made of two steps The reduction of e until a fix point is reached Then there is the end of instant s reaction Hg 1 1 ei Si S Si H ei eoi i ei Si gt e Si Where e S lt lt e S if e S e S and e S 4 The relation is the reflexive and transitive closure of let z v in e S Selx v S run proc e S gt e S vje S 3 e S emit nv S amp O S v n vz llv2 S gt O S loop e S amp e loop e S present n then e else 2 5 5 1 9 ifne S signal x default v gather v2 in e S 5 elx n S v1 v2 0 n if n g Dom S do v until n S gt 0 S do v when n S gt O Sifnes Figure 4 Head reduction f S H 1 eoi 1 S H 2 eoi 2 1 S H 1 eoi 1 SE
7. e reacts with the big step semantics into e and the termination status is true N H e EES e then e behaves as O VN S N H e true e S LEMMA 6 If e So gt e1 S and N F e on e with Si CS thenNte a e with E E U S S PrRooF The proof is made into two parts First we prove the same property for the reduction Then we show that this is true in any context Now the following lemma shows that if an expression can react with the two semantics then the signal environment and the expression obtained at the end of the reaction are the same LEMMA 7 For every Sinit and e such that Ej 61 y e N F e e where S is the small signal environ S ment such that Sinit E S e Sinit gt 2 S2 e Yn Dom S2 S3 n f and f x fly z fy f x 2 then e1 e2 and S S2 Proor With lemma 4 there exists N2 E2 and b2 such that N2 F e Ten e2 and we can notice by construction 2 S2 is the smallest signal environment such that Sinit E S2 N and N2 are the sets of fresh names use during the reactions With some renaming we can have a set N such E1 b E2 b that N F e Z gt er and N F e Z5 ea 2 1 With lemma 2 we know that there is a unique smallest signal environment in which an expression can react with the big step semantics so S S2 Now with the determinism lemma 1 we have Fy E2 b bz and e1 e2
8. in particular classical problems appearing in process calculi such as scope extrusion phenomena The FAIR THREADS 9 27 are an extension of the reac tive approach that allows to mix cooperative and preemptive scheduling In this model several synchronous schedulers can be executed in an asynchronous way The threads can move from a scheduler to an other dynamically or can be executed asynchronously out of all schedulers The threads that can be executed alone must be implemented over the system threads it limits the number of such threads and it leads to efficiency problems Contrary to REACTIVEML in the FAIR THREADS there is only top level concurrency we cannot write e le2 e3 and there is no hierarchical control structures ULM 6 is a language dedicated to mobility It also bor rows the principles of synchronous reactive programming in troduced by Boussinot and embed it inside a call by value A calculus In ULM references are encoded like signals ac cessing a reference which is not local is delayed until it be comes present We did not address mobility issues and thus accessing a reference is instantaneous In REACTIVEML synchronization can only be done through the use of a sig nal and reactive construct must appear in particular places of the program In comparison ULM allows to insert reac tive constructs e g pause anywhere in an expression As a consequence some overhead is imposed on the execution on regular M
9. languages make this compilation difficult and calls for new program analysis 9 REFERENCES 1 R Acosta Bermejo Rejo Langage d Objets R actifs et d Agents PhD thesis Ecole des Mines de Paris 2003 2 Raul Acosta Bermejo Reactive operating system reactive java objects In NOTERE 2000 Paris November 2000 ENST 3 F Benbadis M Dias de Amorim and S Fdida ELIP Embedded location information protocol In FIP Networking 2005 Conference 2005 4 A Benveniste P Caspi S Edwards N Halbwachs P Le Guernic and R de Simone The Synchronous Languages Twelve Years Later Proceedings of the IEEE 2003 5 G Berry The constructive semantics of esterel 1998 6 G rard Boudol ULM a core programming model for global computing In Proceedings of the European Symposium on Programming 2004 7 Fr d ric Boussinot Reactive C An extension of C to program reactive systems Software Practice and Experience 21 4 401 428 Apr 1991 8 Fr d ric Boussinot Concurrent programming with Fair Threads The LOFT language 2003 9 Fr d ric Boussinot FairThreads mixing cooperative and preemptive threads in C Research report 5039 INRIA 2003 10 Fr d ric Boussinot Reactive programming of cellular automata Technical Report 5183 INRIA 2004 11 Fr d ric Boussinot and Robert de Simone The SL synchronous language Software Engineering 12 13 14 15 16 17
10. other REACTIVEML programs or OCAML li braries This translation leaves unchanged regular ML ex pressions only the type information is used whereas every reactive construction is translated into a combinator defined in OCAML Reactive programs can finally be executed by linking them with an ad hoc OCAML library As opposed to classical synchronous programs reactive programs are no more statically scheduled Programs are rather scheduled dynamically or interpreted according to the actual dependences between instructions reading or emitting signals in the programs The scheduling strategy we have implemented is a greedy strategy reminiscent to a technique introduced by Hazard known as one of the most efficient scheduling technique for JUNIOR The precise description of the scheduling technique we have implemented in REAC TIVEML is outside the scope of this paper Let us give an intuitive presentation The scheduling is based on the use of waiting queues such that an action is fired only when the signal it is waiting for is emitted During the execution the interpreter keeps track of the set W of actions waiting for the presence of a signal during one instant When W is not empty at the end of the instant pertinent informations are transfered to the next instant In order to implement a greedy scheduling technique we associate two waiting queues for every signal One queue is used for instructions waiting only one instant e g present
11. systems It provides adequate pro gramming constructs namely synchronous parallel com position broadcast communication and dynamic creation which allow for a natural implementation of the hard part of the simulation The complete REACTIVEML imple mentation with graphical interface statistics is about 1000 lines Experimental results show that the REACTIVEML im plementation is two order of magnitude faster than the orig inal C version it was able to simulate more that 1000 nodes where the original C version failed after 200 nodes and is twice faster that the ad hoc version directly programmed in NAB 23 A project is under way for using REACTIVEML for simulating network sensors taking into account the tem poral aspects of nodes e g energy consumption or failure and to connect REACTIVEML with automatic test sequences generators such as LURETTE 16 8 CONCLUSION AND RELATED WORKS In this paper we have presented an extension of an exist ing strict ML language with reactive constructs The result language is dedicated to the implementation of complex dy namic systems as found in graphical interfaces video games and simulation problems Compared to existing embedding of the reactive approach in either an imperative language 8 or an object oriented language 1 the present work provides a complete semantics of the embedding This allows a precise understanding of the communication between the two levels and reveals
12. transmitted on the signal s and starts the execution of e on the next instant When s is not emitted x takes the default value of s 4 BEHAVIORAL SEMANTICS In this section we formalize the execution of a REAC TIVEML program We base it on a behavioral semantics in the style of the logical behavioral semantics of ESTEREL 5 We define the semantics in two steps We defines the se mantics of instantaneous computations for which 0 F e before giving the semantics of sequential computations No tice that sequential does not mean imperative but it is used like in the circuit terminology An expression is sequential when its execution can take several instants 4 1 Instantaneous Computations Instantaneous expressions such that 0 e are regular ML expression which receive a standard operational seman tics For this purpose we define the set of values v such that v cln v v Ave proce A value can be an immediate constant c a signal value n belonging to a numerable set M an abstraction Az e or a value process proc e For every instantaneous expression e we define the pred icate e v stating that e evaluates to the value v We use the notation e x v for the substitution of x by v in the expression e e J v1 ez I v2 elz recz e 4v e1 e2 4 v1 v2 vibu recr ellu e1 Ave e2 Ie v2 e x ve 4v e vi elz vi 4v e1eg v let x e1 in e2 v 4 2 Sequential Computa
13. 18 19 20 21 22 23 24 25 26 27 22 4 256 266 1996 Fr d ric Boussinot Jean Ferdinand Susini Fr d ric Dang Tran and Laurent Hazard A reactive behavior framework for dynamic virtual worlds In Proceedings of the sixth international conference on 3D Web technology pages 69 75 ACM Press 2001 Fr d ric Boussinot and Jean Ferdinant Susini The sugarcubes tool box a reactive java framework Software Practice and Experience 28 14 1531 1550 1998 N Halbwachs P Raymond and C Ratel Generating efficient code from data flow programs In Third International Symposium on Programming Language Implementation and Logic Programming Passau Germany August 1991 Laurent Hazard Jean Ferdy Susini and Fr d ric Boussinot The Junior reactive kernel Research report 3732 INRIA 1999 E Jahier P Raymond and P Baufreton Case studies with Lurette V2 In Proceedings of the First International Symposium on Leveraging Applications of Formal Method 2004 G Kahn The semantics of a simple language for parallel programming In IFIP 74 Congress North Holland Amsterdam 1974 Xavier Leroy The Objective Caml system release 3 08 Documentation and user s manual Technical report INRIA 2004 Louis Mandel and Farid Benbadis Simulation of mobile ad hoc network protocols in ReactiveML Submitted to publication Louis Mandel and Marc Pouzet ReactiveML a reactive extension to ML extended vers
14. A b2 Ab23 is made from the hypothesis b3 b A b2 and b3 gt bi A bag We can prove easily that N3 UN3 C M1 U Ni N2 U Naz The last point that we have to prove is Ez U E3 E Fi U E13 g Fa U E23 From the hypothesis 3 C Fi N 2 and Es E 1 N E2 we have Es E Ei 1 Ez C Ez 2 E3 E Fig 3 Es E E2 4 The union of 1 and 3 and the union of 2 and 4 give E3 E35 Fi Fi 5 E3 E3 E Ez E23 6 the intersection of 5 and 6 is Es U E33 Es U E33 Fi U Fiz p E2 U E23 which is equal to Es E3 E Fi l E13 f E2 U E2 Case present e then e else e2 With the determinism of ML lemma 8 we have that e n e Case n S3 In this case the expression can react en n S3 0 fal H present e then e else e2 Dens e2 3 and this is trivial to check the properties false b1 Abe OC En Es and C Ni NA No e Case n S3 By hypothesis n E S3 gt n S2 So SG An E1 b en neS Mere el S Ey by Ni F present e then e else e2 rege el T E2 b ejn n So NaF e Z5 2 ei 2 E2 b2 N2 present e then e else e2 a elz 2 By induction and with the rule of present E3 b3 en neS3 Nz3Fe l 3 E3 b Ns F present e then e else e2 at eis 3 and b3 gt b A b2 and Es C Ey MB and N3 C N N N
15. L expressions Indeed reactive code is trans formed into continuation passing style by CPS transforma tion whereas OCAML code does not have to be modified We know that ML code cannot be interrupted so we do not have to introduce some mechanism to save the execution context CONCURRENTML 26 is a language that support concur rent programming and functional programming As opposed to REACTIVEML it is based on a preemptive scheduling The communication between processes is made by communi cation channels or shared memory To control concurrent ac cess to the memory CONCURRENTML uses semaphores mu tex locks and condition variables whereas in REACTIVEML we do not have to use them because we have the guaranty by the compilation of the concurrency that instantaneous actions are atomic In REACTIVEML there is a sequential run time there is no concurrency during the execution The language is very young and several extensions can be considered In particular an important work must be done concerning the efficiency of the execution in order to use REACTIVEML for programming real size simulation prob lems and to be a convincing alternative to traditional meth ods For example the recognition of subparts of a reactive program which can be compiled that is statically sched uled is still open Whereas causality inconsistencies are eliminated in the Boussinot model the scope extrusion phe nomena which is absent in existing synchronous
16. ReactiveML a Reactive Extension to ML Louis Mandel and Marc Pouzet Universit Pierre et Marie Curie LIP6 ABSTRACT We present REACTIVEML a programming language dedi cated to the implementation of complex reactive systems as found in graphical user interfaces video games or simulation problems The language is based on the reactive model in troduced by Boussinot This model combines the so called synchronous model found in ESTEREL which provides instan taneous communication and parallel composition with clas sical features found in asynchronous models like dynamic creation of processes The language comes as a conservative extension of an ex isting call by value ML language and it provides additional constructs for describing the temporal part of a system The language receives a behavioral semantics la ESTEREL and a transition semantics describing precisely the inter action between ML values and reactive constructs It is statically typed through a Milner type inference system and programs are compiled into regular ML programs The lan guage has been used for programming several complex sim ulation problems e g routing protocols in mobile ad hoc networks 1 INTRODUCTION Synchronous programming 4 has been introduced in the 80 s as a way to design and implement safety critical real time systems It is founded on the ideal zero delay model where communications and computations are supposed to be instantaneous
17. Vne Dom E1 Ey n Cc E2 n SiC S2 iff SIES The reaction of an expression e into e is defined in a transition relation of the form E b Nre e N stands for a set of fresh signal names S stands for a signal environment containing input output and local signals and E is the event made of signals emitted during the reaction b is a boolean value which is true if e has finished The execution of the program is a succession of reactions potentially infinite The execution is finished when the termination status b is true At each instant the program reads some inputs J and produces some outputs O and local signals The execution of an instant is defined by the smallest signal environment S for the order E such that E b 4 Ni jH i z i where O Ei and L U Ei ES S C S and 97 C Sf Yn Nizi n Z Dom S The smallest S denotes the signal environment in which the number of present signals is the smallest This set contains input as well as output signals this is the property of in stantaneous broadcasting of events that is all the emitted signal are seen during the current reaction The conditions S C Sf and Sf C S mean that the default value and gathering function associated to a signal stay the same dur ing several reactions We can notice that it is only necessary to keep this information for signals which are still alive at the end of the reaction they
18. cs and prove it to be equivalent Compared to existing semantics for the reactive model e g JUNIOR these two semantics express precisely the interaction between values from the host lan guage and reactive constructs and this is new Moreover the language is statically typed through a Milner type sys tem Compared to the library approach we believe that the language approach leads to a safer and a more natural pro gramming In particular the language provides a notion of signals with regular scope properties Moreover some parts of a program can be compiled vs interpreted leading to a far more efficient execution Section 2 illustrates the expressiveness of the language on some simple examples t A synchronous reactive calculus based on Boussinot s model is defined in section 3 We em bed this kernel inside a call by value ML kernel Section 4 presents its behavioral semantics and establish its two main properties in a given environment a program is determin istic and always progress Section 5 presents a transition semantics and an equivalence theorem Section 6 presents the type system which comes as a natural extension of the ML type system of the host language Implementation is sues are addressed in section 7 In section 8 we discuss related works and conclude 2 LANGUAGE OVERVIEW 2 1 A Short Introduction to ReactiveML REACTIVEML is built above OCAML 18 such that every OCAML program without objects labels and func
19. ctive model In this model the absence of x is effective in the next instant Thus the previous program is equivalent to pause emit x Now we can write the edge front detector a typical con struct appearing in control systems The behavior of the process edge is to emit s_out when s_in is present and it was absent in the previous instant let process edge s_in s_out loop present s_in then pause else await immediate s_in emit s_out end While s_in is present the process emits no value When s_in is absent no value is emitted at that instant and the control passes through the else branch At the next instant the process awaits for the presence of s_in When s_in is present then s_out is emitted since s_in was necessary absent at the previous instant The immediate keywords states that s_in is taking into account even if s_in appears at the very first instant We now introduce the two main control structures of the language the construction do e when s suspends the exe cution of a process e when the signal s is absent whereas do e until s interrupts the execution of e when s is present We illustrate these two constructions on a suspend_resume process which control the instant where a process is exe cuted We first define a process sustain parameterized by a sig nal s sustain emits the signal s at every instant let process sustain s loop emit s pause end We define now an othe
20. do appear in e The condi tion Yn Nizi1 n Z Dom S means that N is a set of fresh names The behavioral semantics is defined in figure 3 Let us comment the rules e The rules for the sequence illustrate the use of the termination status b The expression e2 is executed only if e terminates instantaneously b true e The behavior of the parallel composition is to execute e1 and eg and to terminate when both branches have terminated e The loop is defined by unfolding The termination status false guaranty that there is no instantaneous loop e signal x default e gather e2 in e declare a new sig nal The default value e1 and the gathering function e2 associated to x are evaluated at the signal decla ration The name z is substituted by a fresh name n in e e emit e1 e2 evaluates e into a signal n and adds the result of the evaluation of e2 to the multiset of emitted values on n e let e x in e1 is used to get the value associated to a signal e must be evaluated in a signal n and v is the combination of all the values emitted on n during the instant The function fold is defined as follows fold f u1 Um ve fold fm f v v2 fold fv v The reaction of the program substitutes x by v in e1 The body is executed at the next instant This in struction takes one instant because in the reactive ap proach all the emitted signal are known at the end of instant only e let x e1 in e2 evaluates e1 into
21. e emitted values 2y f vn f v2 f vi d on a signal s and 7 is the one of the combination then s has type 71 72 event If we want to define a signal sum that computes the sum of the emitted values then we can write signal sum default 0 gather in In this case the program await sum x in print_int x awaits the first instant in which sum is emitted and then at the next instant prints the sum of the values emitted sum has type int int event An other very useful signal declaration is the one that collects all the values emitted during the instant which is written simply signal s in as a short cut for signal s default Multiset empty gather Multiset add in Here the default value is the empty set and the gathering function the addition of an element in a multiset 2 2 The Sieve of Eratosthenes We consider the sieve of Eratosthenes as it can be found in 17 and is a classical in reactive calculus see 8 for ex ample The Eratosthenes sieve is an interesting program because it combines signals synchronous parallel composi tion and dynamic creation We first write the process integers which generates the sequence of naturals from an integer value n let rec process integers n s_out emit s_out n pause run integers n 1 s_out val integers int gt int a event gt process It is a recursive process that is parameterized by an integer n and a signal s_out Recurs
22. ed signals They can be emitted emit signal value or awaited to get the asso ciated value await signal pattern in expression Dif ferent values can be emitted during an instant it is called multi emission REACTIVEML adopts an original solution for that when a valued signal is declared we have to de fine how to combine values emitted during the same instant This is achieved with the construction signal name default value gather function in expression The behavior of multi emission is illustrated in Fig 1 We assume signal s declared with the default value d and the gathering function f If values v1 vn are emitted during an instant then all the await receive the value v at the next instant Getting the value associated to a signal is delayed to avoid causality problems Indeed as opposed to ESTEREL and following the reactive approach of Boussinot the fol lowing program await s x in emit s x 1 is causal the integer value x of s potentially resulting from the combi nation of several values is only available at the end of the instant Thus if x 42 during the current reaction the program will emit s 43 in the following reaction Notice that this is different from awaiting the signal presence which executes its continuation in the same instant The type of the emitted values and the type of the combi nation s result can be different This information is reported in the type of signals If T is the type of th
23. he defini tion of an anonymous process that executes p1 and emits ack In this process the signal ack is free when it is emitted on add ack is a local signal and add has a bigger scope so ack escapes its scope 3 ASYNCHRONOUS REACTIVE CALCU LUS IN ML We introduce a reactive kernel in which programs given in the introduction can be translated easily This kernel is built above a call by value functional language with an ML syntax Expressions e are made of variables a imme diate constants c pairs e e abstractions Az e appli cations e e local definitions let x e in e recursions reca e processes proc e a sequence e e a parallel synchronous composition of two expressions elle a loop loop e asignal declaration signal x default e gather e ine with a default value e1 and a combination function e2 a test of presence present e then e else e an emission of a valued signal emit e e an instantiation of a process definition run e a preemption do e until e a suspen sion do e when e and the access to the value of a signal let e x ine e x a c e e Ave ee recx e proce e e elle loop e present e then e else e signal x default e gather e ine emit e e let x e in e let e x ine rune do e until e do e when e Cons true false 0 In order to separate regular ML programs from reactive con structs expressions e must verify some well formation rules g
24. in s run shift s s_out val shift int int event gt int a event gt process Finally we define the process output which prints the prime numbers and the main process sieve let process output s_in loop await s_in prime in print_int prime end val output Ca int event gt process let process sieve signal nat default 0 gather fun x y gt x in signal prime default 0 gather fun x y gt x in run integers 2 nat run shift nat prime I run output prime val steve process The gathering functions of the signals nat and prime keep only one of the emitted values 2 3 Higher Order and Scope Extrusion We present now an example where processes are emitted on signals We encode the construction Jr Dynapar add Jr Halt of JUNIOR introduced in 1 for the programming of Agent systems This process receives some processes on the signal add and executes them in parallel let rec process dynapar add await add p in run p run dynapar add The emission of processes with free signals can lead to a scope extrusion problem a classical phenomenon in process calculi 22 It can be illustrated on the typical example of a process which emits a process p1 and awaits an acknowl edgment of its execution in order to execute a process p2 let process send add p1 p2 signal ack in emit add process run p1 emit ack await immediate ack run p2 The expression process run p1 emit ack is t
25. ion Submitted to PPDP 05 R Milner A theory of type polymorphism in programming Journal of Computer and System Science 17 348 375 1978 Robin Milner Communicating and Mobile Systems The m Calculus Cambridge University Press 1999 Network in A Box http nab epfl ch Benjamin C Pierce Basic Category Theory for Computer Scientists MIT Press 1991 Riccardo Pucella Reactive programming in Standard ML In Proceedings of the IEEE International Conference on Computer Languages pages 48 57 IEEE Computer Society Press 1998 John H Reppy Concurrent Programming in ML Cambridge University Press 1999 Manuel Serrano Fr d ric Boussinot and Bernard Serpette Scheme fair threads In Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming pages 203 214 ACM Press 2004 APPENDIX A PROOFS A 1 Proof of lemma 1 We first start with an auxiliary property The semantics of ML is deterministic LEMMA 8 For every expression e if e v and e v2 then v1 v2 Now we prove the determinism of the behavioral semantics by structural induction on the derivations We just present the most interesting case Case let e x in e There is only one rule that can be applied eni S ni di gi m1 v fold g m dy NF let e x ine eae e z v e 4 n2 S n2 d2 92 M2 v2 fold g2 M2 d2 N F let e x ine Ahle e x vo with le
26. it ted at the second instant An other choice is to execute both expressions in parallel We found it more clear to forbid the use of reactive expressions in a pair such that the evaluation order does not matter A pair will only compose instanta neous computations For example the definition let process f x e1 in e2 isa short cut for let f Axv proc e in e2 and let f x e in e2 stands for let f Aw e1 in e2 Ore lke OF er OF e 2 OF er OF e2 Ore kk eg Ore kkKa kke kk Aa e k F proce kk eez kF e1 e2 kF let z e1 in e2 1 F rune lke Ore OF e2 Ore lre 1F ez kre kF eg OFe 1Fe 1Fez 1 F loop e 1 F emit e1 e2 kF recr e 1 F ellez kt e1 e2 1 F present e then e else e2 O0Fe OF eg 1Fe OFe 1Fez Ore 1Fez Ore 1Fez 1 F signal x default e1 gather e2 ine 1 F let e1 x in e2 1 F do e2 until e1 1 F do e2 when e1 Figure 2 Well formation rules This is essentially a two level language separating regular ML expressions used for describing instantaneous computa tions and reactive constructs for describing the reactive part of a system In this way regular ML program shall be exe cuted as is without any computational impact whereas reac tive programs will be treated specially Compilation issues will be discussed in section 7 Using this kernel we can derive other operators like the following emit e Lf emite O present e1 then e2 der present e1 then e2 else present e else e2 def present e then e
27. it was possible to concil iate the basic principles of synchronous languages with the dynamic creation of processes if the system cannot react in stantaneously to the absence of an event In this way logical inconsistencies which may appear during the synchronous composition of processes disappear as well as the need of complex causality analysis to statically reject inconsistent programs This model was called the synchronous reactive model or simply reactive and identified inside SL 11 a synchronous reactive calculus derived from ESTEREL Later on the JUNIOR 15 calculus was introduced as a way to give a semantics to the SUGARCUBES 13 this last one being an embedding of the reactive model inside JAVA This model has been used successfully for the implementation of com plex interactive systems as found in graphics user interfaces video games or simulation problems 12 13 2 and appears as a competitive alternative to the classical thread based approach From these first experiments several embedding of the re active model have been developed 7 13 25 27 These im plementations have been proposed in the form of libraries in side general purpose programming languages The library approach was indeed very attractive because it gives access to all the features of the host language and it is relatively light to implement Nonetheless this approach can lead to confusions between values from the host languages used for prog
28. ive calls are made through a run We can notice that there is no instantaneous recursion because of the pause statement The type of the process is inferred by the compiler Now we define the process filter which removes all the multiple of some prime number For this purpose we de fine an auxiliary function not_multiple not_multiple is a regular OCAML function which can be used in any other OCAML expression or reactive process let not_multiple n p n mod p lt gt 0 val not_multiple int gt int gt bool let process filter prime s_in s_out loop await s_in n in if not_multiple n prime then emit s_out n end val filter int gt Ca int event gt int b event gt process It is an error to write a reactive construction such as pause in a regular OCAML expression and the compiler rejects it For example the function let f x pause x is rejected 3In the actual implementation emitted values are gathered in a list Now the process shift creates a new filter process for each newly discovered prime number We can notice that dynamic creation is done through recursion There fore as opposed to conventional synchronous programming languages REACTIVEML does not ensure an execution in bounded time and memory but this is not a surprise let rec process shift s_in s_out await s_in prime in emit s_out prime emit a discovered prime signal s default 0 gather fun x y gt x in run filter prime s_
29. iven figure 2 For this purpose we define the predicate k e where e is an expression and k 0 1 We shall say that an expression e is instantaneous or combinatorial when 0 F e can be derived whereas 1 e means that e is re active or sequential to follow classical circuit terminology A sequential expression is supposed to take time The rules are defined figure 2 A rule given in the context k k F e is a short cut for the two rules 0 F e and 1 F e So for example it means that a variable or a constant can be used in any context An abstraction Av e can also be used in an instantaneous ex pression or in a process but its body must be combinatorial For a process definition proc e the body is typed with the context 1 All the ML expressions are well formed in any context and the expressions like run loop or present can be used only in a process We can notice that there is no rules which conclude that an expression is well formed only in a context 0 Hence all the combinatorial expressions can be used in a process This rules implies some choices in the design of the lan guage For example we could allow reactive expressions to appear in a pair and thus write kre kF eg kH e1 e2 but in this case the expression emit s pause may have several semantics If the evaluation order is from left to right the signal s is emitted during the first instant while with an evaluation order from right to left the signal is em
30. l such that the treat ment of the absence to prepare the reaction for the next instant can only be done at the end of instant The reaction of an instant is stopped when there is no more reductions possible From this point the signal en vironment cannot change there is no more signal emission So all the signals not emitted are consider to be absent The rules for the end of instant s reaction are of the form S F e eo and are defined figure 5 We can notice that the rules are not given for all the expressions because they are applied only when the program cannot be reduced with Let s comment the rules of figure 5 e Values do not change at the end of an instant e The reaction of the parallel composition is the reaction of the two branches e Only the left branch of the sequence reacts because the right branch is not activated during the instant e If there is a present instruction the signal is con sidered to be absent So the else branch has to be executed at the next instant e The let n x in e gets the values associated to the sig nal n and combines them with the function fold gm d to obtain the value v Then zx is substituted by v in e for the next instant If n has not been emitted v is equal to d e The preemption occurs at the end of instant If the signal that control the do until is present the expres sion has to be preempted In this case the do until is rewritten into e For the do when
31. lse E UE2 b E UE2 by Ab2 N F e1 e2 gt e5e2 N Na F e13e2 e N No H e1 lle Z el lles E false E b N H e e e Jui eg ve S4 n v S9 n ve Nk efx n gt e Nt loop e EA ej loop e ein eau en S n d g m E b N n signal x default e gather ez ine ae e E b 1 v fodgmd ev N F ea x v gt ez F emit e1 e2 AiL O ein nes Nhe se F let e x in ey ae eilz false E b f N F let x e1 in e2 gt ez eln ngs true F O 0 s en ngs E b N F present e then e1 else e2 el en nes Nel ey fal F present e then e1 else e2 ams e fal F do e when e AES do e when n eln nes NF er gt ef N do e when e ejn ngs Nhe e E false E true 4 en neS NFe Ee ei E false E true do e when n N do e when e gt S E b e proce NFe mete N do e until e 55 O E b N F do e until e R do ej until n E b Nt rune ej s Figure 3 Behavioral Semantics The combination of this properties insures that every re active programs can be executed in REACTIVEML Notice this property is not verified a priori in ESTEREL and needs a causality analysis LEMMA 1 For every expression e the behavioral seman tics of e is deterministic i e Ve YS YN ifYn Dom S n f and f x f y 2 f y F 2 E1 b Eo b and N F e e and Nt e e then E E A b
32. lse e2 signal s ine ged signal s default 0 gather Av Ay x Wy ine def pause signal x in present x else do when s pause await immediate s aA fe i d await immediate s await s await s x in e await immediate s let s x ine In REACTIVEML signals are always valued Thus a pure signal in the ESTEREL sense is implemented with a valued signal with value At the declaration point of a signal the programmer must provide a default value e and cor responding to the instants where the signal is not emitted and a combination function e2 This combination function is used to combine all the values emitted during the same reaction The construction signal s in p is a shortcut for the signal declaration that collects all the values emitted in a multiset stands for an empty multiset and W is the union if m v1 Un and m2 v1 vz then my Y m2 01 005 Un V1 3 Vet The pause statement stops the execution for one instant Indeed as opposed to ESTEREL and following SL 11 the absence of a signal can only be decided at the end of the cur rent reaction Since x is not emitted present x will evaluate to false at the end of the reaction so the instruction will be executed during the next reaction The await immediate constructs awaits for the presence of a signal Awaiting a valued signal can be written await s x in e The access construction let s x in e awaits for the end of the instant to get the value
33. mma 8 n n2 so S n1 S n2 d g v With the property of associativity and commutativity of the gath ering functions we are sure that fold is deterministic thus v v2 Hence e x v e x vo A 2 Proof of lemma 3 By structural induction on the derivations We just present two typical cases the parallel composition and the present Case e le2 For the parallel composition there is only one rule that can be applied E19 619 Erbi 1 Ni F e e NMN F eg ep 1 S 1 2 S 1 11 HE13 b14 big E Ni Nip F llez ei Ilez 1 E2 62 E25 b23 No F e gt el No F eg gt e 1 lo 2 22 S2 S2 E21 UE23 b21 b23 1 1 Na No F e1lle2 ejs Ilez By the induction hypothesis E3 53 E33 b33 N3 H Ei E ela N35 H e2 a ea 23 3 3 and b3 gt bi A ba and b35 gt bi A b23 and E3 E Fi Ee and E3 E Ei mM E23 and Ns G Ni N No and N35 Cc Ni N Noz To apply the rule of the parallel in the environment S3 we first have to prove that N3 N Ns C 0 From the hypothesis we have N3 N Nz C Ni A N2 NA Ni N N23 By associativity and commutativity N3 N Ns C Nia A Nig A N23 N N23 With the definition of we have Ni N Ni and Na N No Hence N3 N N3 C 0 So we have 3 563 E33 639 Na Fe ea Na Her 22 eh S3 S3 31 HE33 b34 b33 E N3 lt N35 F ellez Eis Iles 3 The proof of b3 b3 b1 Ab12
34. ot modified In the typing of signal the default value e1 has the type of the associated value and the gathering function e2 is a function of an emitted value and of the combination of the previous emitted values and returns the new combination The rule for emit checks that the first argument has a signal type and that the first parameter of this type and the type of the value emitted are the same let e1 x in e gets the value associated to a signal So if e has type T T event x must have type rT The instantiation run e is applied to a process Finally the present until and when constructions can be applied to any signal The safety of the type system is proved with standard techniques 24 7 IMPLEMENTATION AND EXPERIMENTS We followed a very pragmatic approach in the design of the language and efficiency was one of our major concern We built REACTIVEML as an extension of a subset of OCAML 18 without objects labels and functors which can mix reac tive processes and regular OCAML expressions We choose OCAML with the following idea in mind OCAML will provide modular data and control structures for programming the algorithmic part of the system whereas reactive constructs will provide modular control structures for describing the temporal aspect The compilation of a REACTIVEML pro gram processes as follows programs are first typed before being translated into OCAML code This code can in turn be linked with
35. ot operational since it express what the reaction should verify and not how reactions are computed In particular the signal environment has to be guessed We present now a small step semantics where the reaction build the signal environment An instant is made into two steps The first one is an extension of the reduction semantics of ML The second one name the end of instant s reaction prepares the next instant s reaction 5 1 Reduction Semantics The reaction of an instant starts with a sequence of reac tions of the form e S gt e S Contrary to the previous semantics the signal environment S is built during the reaction To define the reaction we start with the axioms for the relation of head reduction figure 4 e The let s axiom substitutes x by v in e e The rule of the sequence remove the left branch when this is a value e When the two branches of a parallel are values the parallel is reduced into the value e The loop duplicates its body e The run instruction applied to a process definition ex ecutes it e emit n v is reduced into and adds v to the multiset of values emitted on n e The present construction can be reduced only if the signal is present in the environment e The declaration of a signal x substitutes x by n in e n is a fresh name taken in M n is added to the signal environment with the default value v1 and the gather ing function v2 Initially the multiset of val
36. r typical primitive switch is a two states Moore machine which is parameterized by two sig nals s_in and s_out Its behavior is to start the emission of s_out when s_in is emitted and to sustain this emission while s_in is absent When s_in is emitted again the emis sion of s_out is stopped and the process returns in its initial state let process switch s_in s_out loop await immediate s_in pause do run sustain s_out until s_in done end emit s vl await s x in emit s v2 d d emit s vn await s y in We CEE Vi sca tE 2 CE Sve 19 2 Figure 1 Multi emission on signal s combined with function f gives the value v at the next instant We define now the process suspend_resume parameterized by a signal s and a process p This process awaits the first emission of s to start the execution of p Then each emission of s alternatively suspends the execution of p and resumes it We implement this process with the parallel composition of 1 a do when construction that executes p only when the signal active is present and 2 the execution of a switch that controls the emission of active with the signal s let process suspend_resume s p signal active in do run p when active run switch s active Notice that suspend_resume is an example of a higher order process since it takes a process p as a parameter REACTIVEML also provides valuat
37. ramming the instant and reactive constructs This can lead to re entrance phenomena which are usually detected by run time tests Moreover signals in the reactive model are subject to dynamic scoping rules making the reasoning on programs hard Most importantly implementations of the reactive model have to compete with traditional mostly se quential implementation techniques of complex simulation problems This calls for specific compilation optimization and program analysis techniques which can be hardly done with the library approach The approach we choose is to provide concurrency at lan guage level We enrich a strict ML language with new primi tives for reactive programming We separate regular ML ex pressions from reactive ones through the notion of a process An ML expression is considered to be an atomic timeless computation whereas a process is a state machine whose be havior depends on the history of its inputs It is made of regular ML expressions and reactive expressions Regular ML expressions are executed as is without any computa tional impact whereas reactive expressions are compiled in a special way We introduce two semantics for the language The first one is a behavioral semantics in the style of the logical behavioral semantics of ESTEREL This semantics defines what is a valid reaction no matter how this reac tion is actually computed In order to derive an execution mechanism we introduce a transition semanti
38. tions The behavioral semantics describes the reaction of a ex pression to some input signal We start with some auxiliary definitions Let N a numerable set of names and Ni CN No CN The composition Ni N2 is the union of the two set and is defined only if N N No 0 A signal environment S is a function So di g1 m1 ma dk ge Mk Nk A name n is associated to a triple di gi mi where di stands for the default value of n i gi stands for a combination function and m is the multiset of values emitted during a reaction If S ni di gi mi we shall write S4 n di S9 ni gi and S ni mi We use the notation n S when the signal n is present that is S n and n S when the signal is absent that is S n 0 An event E is a function from names to multisets of values E x mi ni me nx We take the convention that if n Dom E then E n We define the union of two events 1 E2 as the event E FE U E gt such that Yn Dom E1 U Dom E2 E n E n amp E2 n And E E N E is the intersection of E and Fa Yn Dom E1 U Dom E2 E n Ei n A E2 n The operator adds a value v to the multiset of values associated to a signal n in a signal environment S no f S n ifn An S v n n Stn SI n S n w v if n n And we define the order relation E on events and lift it to signal environments Ei C E iff
39. tors is a valid program and REACTIVEML code can be linked to any OCAML library A program is a set of definitions Definitions introduce like in OCAML types values or functions REACTIVEML adds the process definition Processes are state machines whose behavior can be executed through several instants They are opposed to regular OCAML functions which are considered to be instantaneous Let us consider the pro cess hello_world that prints hello at the first instant and world at the second one the pause statement suspends the execution until the next instant let process hello_world print_string hello pause print_string world This process can be called by writing run hello_world Communication between parallel processes is made by broadcasting signals A signal can be emitted emit awaited await and we can test its presence present The fol lowing process emits the signal z every time x and y are synchronous 1The distribution of REACTIVEML and complete examples can be found at www spi lip6 fr mandel rml let process together x y z loop present x then present y then emit z pause end Unlike ESTEREL it is impossible to react instantaneously to the absence of an event Thus the following program present x then else emit x which is incorrect in ESTEREL x cannot be present and absent in the same instant and is thus rejected by a causality analysis is perfectly valid in the rea
40. ues asso ciated to n is empty e When the body of a do until construct is a value it means that it reaction is finished So the do until can be reduced into e The do when can be reduced into only when its body is a value and when the signal is present From this axioms we define the reduction e S 5 e S T e S gt T e S Env V T env S gt T w S nES e Se s T do e when n S T do e when n S where T is a context with one hole With the first rule if an expression e head reduces to e then e can be reduced in any context The second rule defines the execution of combinatorial expressions eny must be an expression which is not a value to avoid infinite reductions The last rule is the suspension The body of a do when can be executed only if the signal is present The contexts are defined as follow Tons let T ine T e Tile elll run T emit Te emit e T let T x in e present I then e else e signal x default I gather e ine signal x default e gather T ine do e until T do T until n do e when T The contexts for the parallel composition show that the eval uation order is not specified In the implementation of RE ACTIVEML the scheduling is fixed such that the execution is always deterministic but this is not specified 5 2 End of Instant s Reaction The reactive model is based on the absence of instanta neous reaction to the absence of a signa
41. ular automata programs written in LOFT by Boussinot 10 to serve as benchmarks for testing the efficiency of our im plementation This example puts emphasis on the absence of busy waiting Quiescent cells are stopped on the wait ing of an activation signal such that only active cells are executed Figure 7 compares the execution times given for LOFT REACTIVEML and an imperative version written in OcAML The imperative version scans the array of cells with for loops The numbers show that the implementation of REACTIVEML compete favorably with the LortT library Through being well known in the synchronous community this technique has unfortunately never been published so far and can only be appreciated through a careful reading of the code r lt H z AHra t T lt TC c Hte T Hre t Ht e2 72 Ae e1 2 71 x Ta HF Fei Hix Gen 1 H F e2 T2 H F let x e in e2 T2 H z n Fe 72 HFea n gt n HFe n H Fe unit H F e process H F X w e 71 Te H F ee 72 H F proc e process H run e unit HFea n Ht e T2 HFe n H F e T2 H F ellez unit Hte t H F e1 T1 T2 event Hteg n Ht e13 2 T2 H F loop e unit A emit e1 e2 unit Htesw t2 HF Fez gt 72 gt Tr Hs m1 72 event e r Ht e1 T1 T2 event H x 72 F e r H F signal s default e gather e2 in e T H F let e1 x ine 7 Hte r 7 event Htrey t HFez T H F e1 T1 T2 event Hte r H F e1 T1 T2 event Hte r
42. v eoi Vv ngs S n d g m S F ellez eoi ei lles 1 S F e1 2 eoi 1 2 v foldgmd n S SFe gt eoi e S F present n then e1 else e2 eo 2 St let n x in e gt eoi e x v S H do e until n gt eoi do e until n nes nEs Skee e ngs St do e until n gt eoi O S H do e when n gt eoi do e when n S F do e when n gt eoi do e when n Figure 5 End of instant 5 4 Equivalence In this section we show the equivalence between the two semantics We start with the proof that if an expression e reacts into an expression e with the small step semantics then it can react in the same signal environment with the big step semantics LEMMA 4 For every Sinit ande such that e Sinit gt e S then there exists N b such that N F e e with E S are PROOF By induction on the number of reductions in ej Sinit gt e S e If there is no reduction possible we have to prove that the reduction gt eoi is the same that the big step semantics cf lemma 5 e If there is at least one reduction we have to prove that one reduction followed by a big step reaction is equivalent to one big step reaction cf lemma 6 The proof is based on the following properties LEMMA 5 If e S 4 and SF e eo e then there exists N and b such that N F e e PROOF The proof is made by structural induction We have just to notice that if an expression
43. v and substitutes x by v in e2 Then it evaluates e2 e The unit expression does nothing and terminates instantaneously e In a present test if the signal is present the then branch is executed in the instant otherwise the else branch is executed at the next instant e The do when corresponds to the suspend construction of ESTEREL The difference is that the suspension is not made on the presence of a signal but on the ab sence This is due to the reactive approach the reac tion of a signal cannot depend instantaneously on the absence of a signal e The behavior of do until is the same as the kill of SL This is a weak preemption that takes one instant Indeed we cannot have strong preemption to avoid causality problems For example with a strong pre emption the following expression is not causal do await s until s done emit s e run e evaluates the expression e into a process defini tion and executes it Now we establish the main properties of the behavioral semantics stating that the reaction is deterministic for a given signal environment there is only one way a program can react And if a program is reactive 5 there exists one S such that N F e 2o e then there exists a unique smallest signal environment in which it can react The proofs are given in appendix A Ej false Ej true E2 b Ej b E2 b2 Nk ey el N ey el Nob eg gt el Ni Fe el M Fe gt e s S s S s Ej fa
Download Pdf Manuals
Related Search