Reactivity of Cooperative Systems
Contents
1. Time refinement in a functional synchronous language In Principles and Practice of Declarative Programming 2013 Marlow S Jones S Thaller W Extending the Haskell foreign function interface with concurrency In Haskell 04 ACM 2004 22 32 Nielson F Nielson H Type and effect systems Correct System Design 1999 Pierce B Types and programming languages The MIT Press 2002 Potop Butucaru D Edwards S A Berry G Compiling Esterel Springer 2007 26 27 28 29 30 31 32 33 34 R my D Type inference for records in a natural extension of ML Theoretical Aspects of Object Oriented Programming MIT Press 1993 R my D Using understanding and unraveling the OCaml language from practice to theory and vice versa In Applied Semantics Springer 2002 413 536 Reppy J Concurrent programming in ML Cambridge University Press 2007 Sijtsma B A On the productivity of recursive list definitions Transactions on Programming Languages and Systems 11 4 1989 633 649 Syme D Petricek T Lomov D The F asynchronous programming model Practical Aspects of Declarative Languages 2011 175 189 Talpin J P Jouvelot P The type and effect discipline In Logic in Computer Science 1992 Tardieu O de Simone R Loops in Esterel Transaction on Embedded Computing 4 4 2005 708 750 Tofte M Type inference for polymorphic references Information and computation 89 12. Ki J k2 Kil Ko e ot Kj Ka 1 Ki K2 1 ki K2 4 k k24 ki tk KJ KJ Hok runk Note that function calls are not non instantaneous The fact that variables are considered non instantaneous means that any process taken as argument is sup posed to be non instantaneous The reactivity is then checked when this variable is instantiated with the actual behavior of the process A behavior is said to be reactive if for each recursive behavior ud kK the recursion variable does not appear in the first instant of the body This enforces that there must be at least one instant between the instantiation of a process and each recursive call and is formalized in the following definition Definition 2 Reactive behavior A behavior x is reactive if Jt k where the relation RF r is defined by pg R RF ki not K1 1 RE ke RFO RF RF o RF k1 k2 RF ki Kit OF Ke RF k RF ke RF k RF k2 RF k1 k2 RF k Ke RF 4 ke RU F k REK RF wd k RE rusk The predicate R F means that the behavior is reactive with respect to the set of variables R that is these variables do not appear in the first instant of and all the recursions inside are not instantaneous The rule for a variable checks that is not a recursion variable introduced in the current instant The recursion variables are added to the set R when checking the reactivity of a recursive behavior pd k In the case of the sequence K1 K2 we can
3. extended version of the paper the implementation the source code of the ex amples and an online toplevel are available at http reactiveml org sas14 2 Overview of the approach ReactiveML extends ML with programming constructs inspired from synchronous languages 6 It introduces a built in notion of parallelism where time is defined as a succession of logical instants Each parallel process must cooperate to let time elapse It is a deterministic model of concurrency that is compatible with the dynamic creation of processes 9 Synchrony gives us a simple definition for reactivity a reactive ReactiveML program is one where each logical instant terminates Let us first introduce ReactiveML syntax and informal semantics using a sim ple program that highlights the problem of non reactivity Then we will discuss the design choices and limitations of our reactivity analysis using a few other examples 5 http www reactiveml org Qa a RF U Ne 11 12 13 14 15 2 1 A first example We start by creating a process that emits a signal every timer seconds let process clock timer s let time ref Unix gettimeofday in loop let time Unix gettimeofday in if time time gt timer then emit s time time end In ReactiveML there is a distinction between regular ML functions and pro cesses that is functions whose execution can span several logical instants Pro cesses are defined using
4. or a recursive row pd x Therefore the unification algorithm only has to consider these cases Ux K s b gt u r if occur check amp pb gt K otherwise Ux K Us K Q U K1 1 K2 Q2 d1 6 k2 63611 k OI fresh Un Uh Ki 1 K2 Un Ke u1 Ki 1 let K ugi k 1 in Ux Ki 61 Ki 1 62 It should be noted that unification never fails so that we obtain a conser vative extension of ReactiveML type system This unification algorithm reuses traditional techniques for handling recursive types 13 The last case unfolds a recursive row to reveal the row variable so that it can be unified with other rows A downside of our approach is that it introduces one behavior variable for each process so that the computed behaviors may become very big and unread able The purpose of the MASK rule is to remedy this by using effect mask ing 18 The idea is that if a behavior variable appearing in the behavior is free in the environment it is not constrained so we can give it any value In particular we choose to replace it with e which is the neutral element of so that it can be simplified away 4 5 Proof of soundness We now present the proof sketch of the soundness of our analysis that is that at each instant the program admits a finite derivation in the big step semantics of the language and rewrites to a well typed program with reactive effects The b
5. 1990 1 34 Vouillon J Lwt a cooperative thread library In ACM workshop on ML 2008
6. 7 0 K IF e m 72 event _ 0 Pre k1 Th eg 7T ke IT F present e then e1 else e2 T k1 0 k2 I Fei 1 72 event 0 Pre m 0 Tre t kt I emit e e2 unit 0 I F loop e unit 0 K Pre t ka I he 11 72 event _ 0 I x 72 eg 7 ke I F do e1 until e x gt e2 T k1 k2 Tre t amp T bhe m 72 event _ 0 Ma je Ber p g fov l 7 1ASK I F doe whene r r o Tre T Klgee Fig 1 Type and effect rules The PROCESS rule stores the behavior of the body in the type of the process as usual in type and effect systems The presence of the behavior and the MASK rule are related to subeffecting and will be discussed in Section 4 4 A design choice made in ReactiveML is to separate pure ML expressions that are surely instantaneous from processes For instance it is impossible to call pause within the body of a function that must be instantaneous A static analysis used for efficient code generation performed before typing checks this well formation of expressions denoted k F e in 19 and recalled in Appendix A 20 Requiring the behavior of some expressions like the arguments of an application or the body of a function to be equivalent to 0 does not add any new constraint with respect to this existing analysis We do not try to prove the termination of pure ML functions without any reactive behavior The APP rule shows that we assume that function calls always
7. Code a sensor network simulator 1700 SLOC and a mixed music sequencer 3400 SLOC There is no warning for both simulators For the mixed music sequencer there are warnings on eleven processes Eight warnings are due to structural recursions similar to the example par_map Most of them come from the fact that the program is a language interpreter defined as a set of mutually recursive processes on the abstract syntax tree Another warning comes from a record containing a process that is not annotated with a non instantaneous behavior The last two warnings are due to loops around the execution of a musical score In this case the analysis does not use the fact that the score is a non empty list In all these cases it was easy for the programmer to check that these warnings were false positives The last three warnings can be removed by adding a pause in parallel to the potentially instantaneous expressions Other models of concurrency We have already extended our analysis to take into account time refinement 21 We believe this work could be applied to other models of concurrency One just needs to give the behavior e to operations that cooperate with the scheduler like yield We are considering an extension to the X10 language where cooperation points could be clocks In a synchronous world the fact that each process cooperates at each instant implies the reactivity of the whole program as processes are executed in lock step In
8. e behavior is printed and behavior variables are denoted r let process pl val p1 unit process 0 r1 let process p2 pause val p2 unit process r2 let 1 p1 p2 val 1 unit process 0 r list If the behavior of a process had been exactly equal to the behavior of its body this expression would have been rejected by the type system The consequence of the typing rule for processes is that the principal type of an expression process e is always of the form where is the behavior of e and a free variable The idea to use a free type variable to represent other possible types is reminiscent of Remy s row types 26 It makes it possible to implement subeffecting using only unification without manipulating constraint sets as in traditional approaches 31 3 It thus becomes easier to integrate it into any existing ML type inference implementation For instance OCaml type infer ence is also based on row polymorphism 27 so it would be easy to implement our type system on top of the full language We can reuse any existing inference algorithm like algorithm W or M 16 and add only the following algorithm U for unification of behaviors It takes as input two behaviors and returns a substitution that maps behavior variables to behaviors that we denote gt amp 1 2 gt K During unification the behavior of a process is always either a behavior variable a row k
9. remove variables from R if k is non instantaneous One can also check from the definition of k as a recursive behavior that this definition also implies that the body of a loop is non instantaneous 3 3 Equivalence on behaviors We can define an equivalence relation on behaviors that will be used to simplify the behaviors The relation is reflexive symmetric and transitive closure of the following rules The operators and and are idempotent and associative and are commutative but not The 0 behavior resp e is the neutral element of and resp The relation also satisfies the following rules where op is or or Ky Ko ki Ko Ky Ky k2 Ko HO Ky LO K2 run K run k2 K1 Op k2 A op Kh It is easy to show for example that uo e 0 run run uo e run An important property of this relation is that it preserves reactivity It is ex pressed as follows Property 1 if k k2 and RF r then RF kg Proof By induction on the proof of k kg 4 The type and effect system The link between processes and behaviors is done by a type and effect sys tem 18 following the work of Amtoft et al 3 The behavior of a process is its effect computed using the type system After type checking the compiler checks the inferred behaviors and prints a warning if one of them is not reactive The type system is a conservative extension of the original one
10. the two following processes let rec process good_rec pause run good_rec let rec process bad_rec run bad_rec pause W This expression may produce an instantaneous recursion The order between the recursive call and the pause statement is crucial as the good_rec process is reactive while bad_rec loops instantaneously As it is defined recursively the behavior k associated with the good_rec process must verify that k run x The run operator is associated with running a process This equation can be solved by introducing an explicit recursion operator u so that k pd e run Recursive behaviors are defined as usual pd r kio uo K Lo K K if g fov r We denote fbu the set of free behavior variables in There is no operator for representing the behavior of a loop Indeed a loop is just a special case of recursion The behavior of a loop denoted K where is the behavior of the body of the loop is thus defined as a recursive behavior by K yd K run 3 2 Reactive behaviors Using the language of behaviors we can now characterize the behaviors that we want to reject that is instantaneous loops and recursions To formally de fine which behaviors are reactive we first have to define the notion of a non instantaneous behavior i e processes that take at least one instant to execute Definition 1 Non instantaneous behavior A behavior is non instantaneous denoted k if Kit k2
11. x f fix f x val fix Ca gt b gt a gt b gt a gt b let process main let process p k v print_int v run k v 1 in run fix p 0 val main a process run rec r run r W This expression may produce an instantaneous recursion In the example the analysis detects the problem of reactivity although there is no explicit recursive process 6 Discussion Implementation The type inference algorithm of ReactiveML has been ex tended to compute the behaviors of processes with minimal impact on its struc ture and complexity thanks to the use of row polymorphism for subeffecting see Section 4 4 The rules given in Section 3 2 are easily translated into an algo rithm for checking the reactivity of behaviors that is polynomial in the size of behaviors In practice the analysis has an impact on the type checking time but it is negligible compared to the global compilation time For example on a 1 7GHz Intel Core i5 with 4Go RAM the compilation of the examples of the ReactiveML distribution about 5000 lines of code takes about 0 15s where 0 02s are spent in the type checker 0 005s without the reactivity analysis Then it takes 3 5s to compile the generated OCaml code Evaluation The analysis is very useful to detect early small reactivity bugs such as the one presented Section 2 1 We have also used the analysis on bigger appli cations a mobile ad hoc network simulator 1800 Source Lines Of
12. Reactivity of Cooperative Systems Application to ReactiveML Louis Mandel and C dric Pasteur 1 Coll ge de France 2 DI Ecole normale sup rieure now at ANSYS Esterel Technologies 3 INRIA Paris Rocquencourt Abstract Cooperative scheduling enables efficient sequential imple mentations of concurrency It is widely used to provide lightweight threads facilities as libraries or programming constructs in many programming languages However it is up to programmers to actually cooperate to ensure the reactivity of their programs We present a static analysis that checks the reactivity of programs by abstracting them into so called behaviors using a type and effect system Our objective is to find a good compromise between the complexity of the analysis and its precision for typical reactive programs The simplicity of the analysis is mandatory for the programmer to be able to understand error messages and how to fix reactivity problems Our work is applied and implemented in the functional synchronous lan guage ReactiveML It handles recursion higher order processes and first class signals We prove the soundness of our analysis with respect to the big step semantics of the language a well typed program with reactive effects is reactive The analysis is easy to implement and generic enough to be applicable to other models of concurrency such as coroutines 1 Introduction Most programming languages offer lightweight thread facilitie
13. The notions of reactivity and equivalence are lifted from behaviors to types A type is reactive if it contains only reactive behaviors Two types are equivalent also denoted T T2 if they have the same structure and their behaviors are equivalent 4 3 Typing rules Typing judgments are given by e r amp meaning that in the type environ ment I the expression e has type 7 and behavior x We write e 7 _ 0 when the behavior of the expression e is equivalent to 0 The initial typing en vironment I gives the types of primitives Io true bool fst Vay 02 01 X a2 gt a43 The rules defining the type system are given in Figure 1 If all the behaviors are erased it is exactly the same type system as the one presented in 19 which is itself an extension of the ML type system We discuss here the novelties of the rules related to behaviors T lt I a T lt Io c TFre n 0 Th eg 7 0 Tra 7 0 Tre 7r 0 IE e1 2 71 X T2 0 Tja m be t2 0 Tre m7an 0 Th eg 7 _ 0 APP Tb Awe 71 gt T2 0 Tre e2 71 0 Tje reu 7 _ 0 Tre t k PROCESS 7 rrecx v 7 0 I process e Tprocess k 0 I he 7 process K _ 0 I pause unit e Th rune 7 runk TPre n e DChee t2 K2 T a1 gen Ti e1 I 2 gen T2 e2 l F e3 7 K3 I F let z e1 and z2 e2 in e3 T k1 K2 3 Tre m 0 TPhre 1 9 347 0 I x m 72 eventhe 7 kK I signal x default e gather ez in e
14. another model assumptions on the fairness of the scheduler may be required This should not be a major obstacle as these hypotheses are already made in most systems e g in Concurrent Haskell 15 The distinction between processes and functions is important to avoid showing a warning for all recursive functions 7 Related work The analysis of instantaneous loops is an old topic on which much has already been written even recently 1 14 4 It is related to the analysis of productivity and deadlocks in list programs 29 or guard conditions in proof assistants 5 etc Our purpose was to define an analysis that can be used in the context of a general purpose language mutable values recursion etc We tried to find a good compromise between the complexity of the analysis and its precision for typical reactive programs written in ReactiveML The programmer must not be surprised by the analysis and the error messages We focus here only on directly related work Our language of behaviors and type system are inspired by the work of Amtoft et al 3 Their analysis is defined on the ConcurrentML 28 language which extends ML with message passing primitives The behavior of a process records emissions and receptions on communication channels The authors use the type system to prove properties on particular examples not for a general analysis For instance they prove that emission on a given channel always precedes the emis sion on a second
15. cal signal s 2 2 Intuitions and limitations In the previous example we have seen the first cause of non reactivity instan taneous loops The second one is instantaneous recursive processes let rec process instantaneous s emit s run instantaneous s W This expression may produce an instantaneous recursion The execution of emit is instantaneous therefore the recursive call creates a loop that never cooperates A sufficient condition to ensure that a recursive process is reactive is to have at least one instant between the instantiation of the process and any recursive call The idea of our analysis is to statically check this condition This condition is very strong and is not always satisfied by interesting reactive programs For instance it does not hold for a parallel map the let and construct executes its two branches in parallel matching is instantaneous let rec process par_map p 1 match 1 with 1 gt 0 x 1 gt let x run p x and 1 run par_map p 1 in x P W This expression may produce an instantaneous recursion This process has instantaneous recursive calls but it is reactive because the re cursion is finite if the list 1 is finite As the language allows to create mutable and recursive data structures it is hard to prove the termination of such processes For instance the following expression never cooperates let rec 1 0 1 in run par_map p 1 Consequently our analysis onl
16. channel in a given program The idea of using a type and effect 8 http x10 lang org system for checking reactivity or termination is not new For instance Boudol 8 uses a type and effect system to prove termination of functional programs using references by stratifying memory to avoid recursion through references Reactivity analysis is a classic topic in synchronous languages that can also be related to causality In Esterel 25 the first imperative synchronous language it is possible to react immediately to the presence and the absence of a signal The consequence is that a program can be non reactive because there is no consistent status for a given signal the program supposes that a signal is both present and absent during the same instant This problem is solved by checking that programs are constructively correct 25 Our concurrency model inherited from the work of Boussinot 9 avoids these problems by making sure that processes are causal by construction We then only have to check that loops are not instantaneous which is called loop safe by Berry 25 It is easy to check that an Esterel program is loop safe as the language is first order without recursion 32 Closer to ReactiveML the reactivity analysis of FunLoft 2 not only checks that instants terminate but also gives a bound on the duration of the instants through a value analysis The analysis is also restricted to the first order setting In ULM 7 each recursi
17. e a in e2 do loop pause until e1 gt e2 let rec process f 1 p 1 ineg 4 let f rec f z xrp process e1 in ez let and _ amp 1 n e2 l gt I gt I gt 4 2 Types Types are defined by Tu a T TXxT T T Tprocess K 7 7 event types o T YQ o Ya o type schemes I 0 T 0 environments A type is either a type variable a a base type T like bool or unit a product a function a process or a signal The type of a process is parametrized by its return type and its behavior The type T1 T2 event of a signal is parametrized by the type T of emitted values and the type T2 of the received value since a gathering function of type T gt T2 gt T is applied Types schemes quantify universally over type variables and behavior vari ables We denote ftu T resp fbu 7 the set of type resp behavior variables free in 7 and fu r ftu r fov r Instantiation and generalization are defined in a classic way ola T lt Ya o olo k lt Y co gen T e l T if e is expansive gen r e T Va Vo r where a fu r fu L otherwise Analogously to the treatment of references in ML we must be careful not to generalize expressions that allocate signals We use the syntactic criterion of expansive and non expansive expressions 33 An expression is expansive if it can allocate a signal or a reference in which case its type should not be generalized
18. ful for the proofreading and discussions with Guillaume Baudart and Adrien Guatto Finally we also thank the reviewers for there numerous comments and suggestions References 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 Abel A Pientka B Well founded recursion with copatterns In International Conference on Functional Programming 2013 Amadio R Dabrowski F Feasible reactivity in a synchronous z calculus In Principles and Practice of Declarative Programming 2007 221 230 Amtoft T Nielson F Nielson H Type and Effect Systems Behaviours for Concurrency Imperial College Press 1999 Atkey R McBride C Productive coprogramming with guarded recursion In International Conference on Functional Programming 2013 Barthe G Frade M J Gim nez E Pinto L Uustalu T Type based termina tion of recursive definitions Mathematical Structures in Computer Science 14 01 2004 97 141 Benveniste A Caspi P Edwards S A Halbwachs N Guernic P L De Simone R The synchronous languages twelve years later In Proc of the IEEE 2003 Boudol G ULM A core programming model for global computing In European Symposium on Programming 2004 Boudol G Typing termination in a higher order concurrent imperative language Information and Computation 208 6 2010 716 736 Boussinot F Reactive C an extension of C to program reacti
19. ics derivation is finite The soundness theorem is stated as follows Theorem 1 Soundness If rr e 7 and T and k are reactive and we suppose that function calls terminate then there exists e such that e a e and Tk e 7 k with x reactive Proof The proof has two parts The first part is the proof that the result is well typed We use classic syntactic techniques for type soundness 24 on the small step semantics described in 19 The proof of equivalence of the two semantics is also given in the same paper The second part is the proof that the semantics derivation of one instant is finite by induction on the size of the first instant behavior of well typed expressions We only consider one instant because thanks to type preservation if the theorem is true for one instant it is true for the following ones The details of the proof are given in Appendix C 20 5 Examples We present here the result of the analysis on some examples These examples can be downloaded and tried at http reactiveml org sas14 Using a type based analysis makes it easy to deal with cases of aliasing as in the following example let rec process p let q fun x gt x p in rung val p a process rec r run r W This expression may produce an instantaneous recursion The process q has the same type as p and thus the same behavior so the instantaneous recursion is easily detected As for objects in OCaml 27 ro
20. ig step semantics of ReactiveML also called the behavioral semantics in reference to the semantics of Esterel 25 describes the reaction of an expression during an instant i by the smallest signal environment S the set of present signals such that Ej ei gt 641 Si which means that during the instant i in the signal environment S the expres sion e rewrites to e 4 and emits the signals in E The boolean b indicates if 41 has terminated Additional conditions express for instance the fact that the emitted values in must agree with the signal environment An execu tion of a program comprises a succession of a potentially infinite number of reactions and terminates when the status b is equal to true The definition of the semantics was introduced in 19 and is recalled in Appendix B 20 A program is reactive if at each instant the semantics derivation of e is finite To prove that we first isolate the first instant of the behavior of e noted fst This function is formally defined by fst 0 fst e 0 fst K1 k2 fst K1 fst K2 fst d terina fst K1 if Ki fst run run fst sa fst K1 fst Kk2 otherwise fst K1 k2 fst K1 fst Ke fst ud r fst K d pd K The important property of this function is that if a behavior x of e is reactive as defined in Section 3 2 then fst is finite Hence we can prove by induction on the size of fst K that the semant
21. instant let process print_clock s loop do print_string top print_newline when s done end W Line 11 characters 2 78 this expression may be an instantaneous loop Once again this loop can be instantaneous but this time it depends on the presence of the signal While the signal s is absent the process cooperates When it is present the body of the do when executes and terminates instantaneously So the body of the loop also terminates instantaneously and a new iteration of the loop is started in the same logical instant Since the signal is still present 5 The vocabulary is the one of synchronous languages not the one of FRP 17 19 the body of the do when executes one more time and so on This process can also be fixed by adding a pause statement in the loop We can then declare a local signal s and put these two processes in parallel The result is a program that prints top every second let process main signal s default gather fun x y gt in run print_clock s run clock 1 s The declaration of a signal takes as arguments the default value of the signal and a combination function that is used to compute the value of the signal when there are multiple emissions in a single instant Here the default value is O and the signal keeps this value in case of multi emission The operator represents synchronous parallel composition Both branches are executed at each instant and communicate through the lo
22. of ReactiveML that is it is able to assign a behavior to any ReactiveML program that was accepted previously It is an important feature as we only want to show warnings and not reject programs 4 1 Abstract syntax We consider here a kernel of ReactiveML v c v v n Az e process e II e zx c e e Ax e ee rec z v process e run e pause let x e and x e in e signal x default e gather e in e emit e e present e then e else e loop e do e until e x gt e do e when e Values are constants c integers unit value etc pairs of values signal names n functions and processes The language is a call by value lambda calculus extended with constructs for creating process and running run processes waiting for the next instant pause parallel definitions let and declaring sig nals signal emitting a signal emit and several control structures the test of presence of a signal present the unconditional loop loop weak preemp tion do until and suspension do when The expression do e until s x gt e2 executes its body e and interrupts it if s is present In case of preemption the continuation ez is executed on the next instant binding x to the value of s We denote _ variables that do not appear free in the body of a let and the unique value of type unit From this kernel we can encode most constructs of the language e1 eg let e and e2 in QO 1 2 await
23. plete without using Lwt The goal of this paper is to design a static analysis called reactivity analysis to statically remedy this problem of absence of cooperation points The analysis checks that the programmer does not forget to cooperate with the scheduler Our work is applied to the ReactiveML language 19 which is an extension of ML with a synchronous model of concurrency 6 Section 2 However we believe that our approach is generic enough to be applied to other models of concurrency Section 6 The contributions of this paper are the following A reactivity analysis based on a type and effect system 18 in Section 4 The computed effects are called behaviors 3 and are introduced in Section 3 They represent the temporal behaviors of processes by abstracting away values but keeping part of the structure of the program and are used to check if processes cooperate or not A novel approach to subeffecting 23 that is subtyping on effects based on row polymorphism 26 in Section 4 4 It allows to build a conservative extension of the existing type system with little overhead A proof of the soundness of the analysis Section 4 5 a well typed program with reactive effects is reactive The paper ends with some examples Section 5 discussion Section 6 and related work Section 7 The work presented here is implemented in the Reac tiveML compiler and it has already helped detecting many reactivity bugs An
24. s either integrated in the language like the asynchronous computations 30 of F or available as a library like GNU Pth 12 for C Concurrent Haskell 15 or Lwt 34 for OCaml These libraries are based on cooperative scheduling each thread of execution cooperates with the scheduler to let other threads execute This enables an ef ficient and sequential implementation of concurrency allowing to create up to millions of separate threads which is impossible with operating system threads Synchronization also comes almost for free without requiring synchronization primitives like locks The downside of cooperative scheduling is that it is necessary to make sure that threads actually cooperate Control must regularly be returned to the scheduler This is particularly true for infinite loops which are very often present in reactive and interactive systems Blocking functions like operating system primitives for I O cannot be called The solution to the latter is simple never use blocking functions inside coop erative threads All the facilities mentioned earlier provide either I O libraries compatible with cooperative scheduling or a means to safely call blocking func tions See Marlow et al 22 for an overview on how to implement such libraries Dealing with the first issue is usually the responsibility of the programmer For instance in the Lwt manual 11 one can find do not write function that may take time to com
25. terminate instantaneously In the case of present e then e else e2 the first branch e is executed immediately if the signal e is present and the second branch ez is executed at the next instant if it is absent This is reflected in the behavior associated with the expression Similarly for do e until e z e2 the expression ez is executed at the instant following the presence of e The reason why the behavior associated with loop is equal to 0 and not simply will be explained in Section 4 5 Intuitively the soundness proof will use an induction on the size of the behaviours and thus requires the behavior of a sub expression to always be smaller This also applies for signal and do when Finally note that there is no special treatment for recursive processes We will see in the next section that recursive behaviors are introduced during unification 4 4 Subeffecting with row polymorphism The typing rule PROCESS for the creation of processes intuitively mean that a process has at least the behavior of its body The idea is to add a free behavior variable to represent other potential behaviors of the process This subtyping restricted to effects is often referred to as subeffecting 23 we can always replace an effect with a bigger i e less precise one It allows to assign a behavior to any correct ReactiveML program For instance it is possible to build a list of two processes with different behaviors the
26. the process keyword The clock process is parametrized by a float timer and a signal s Signals are communication channels between processes with instantaneous broadcast The process starts by initializing a lo cal reference time with the current time line 2 read using the gettimeofday function of the Unix module from the standard library Then it enters an infinite loop line 3 to 6 At each iteration it reads the new current time and emits the unit value on the signal s if enough time has elapsed line 5 The compiler prints the following warning when compiling this process W Line 3 characters 2 115 this expression may be an instantaneous loop The problem is that the body of the loop is instantaneous It means that this process never cooperates so that logical instants do not progress In ReactiveML cooperating is done by waiting for the next instant using the pause operator We solve our problem by calling it at the end of the loop line 6 if time time gt timer then emit s time time pause end The second part of the program is a process that prints top every time a signal s is emitted The do when construct executes its body only when the signal s is present i e it is emitted It terminates by returning the value of its body instantaneously after the termination of the body Processes have a consistent view of a signal s status during an instant It is either present or absent and cannot change during the
27. the signal s could be present the recursion would be instantaneous Finally we only guarantee that the duration of each instant is finite not that the program is real time that is that there exists a bound on this duration for all instants as shown in this example let rec process server add await add p ack in run server add let v run p in emit ack v The server process listens on a signal add to receive both a process p and a signal ack on which to send back results As it creates one new process each time the add signal is emitted this program can execute an arbitrary number of processes at the same time It is thus not real time but it is indeed reactive as waiting for the value of a signal takes one instant one has to collect and combine all the values emitted during the instant 3 The algebra of behaviors The idea of our analysis is to abstract processes into a simpler language called behaviors following Amtoft et al 3 and to check reactivity on these behaviors The main design choice is to completely abstract values and the presence of signals It is however necessary to keep an abstraction of the structure of the program in order to have a reasonable precision 3 1 The behaviors The algebra of behaviors is given by k 0 ile k KK yo ruk 6 Precedence of operators is the following from highest to lowest run and finally u For instance yd K run k2 k3 means pd k1 r
28. un K2 0 K3 Actions that take at least one instant to execute i e surely non instantaneous actions such as pause are denoted e Potentially instantaneous ones like call ing a pure ML function or emitting a signal are denoted 0 The language also includes behavior variables to represent the behaviors of processes taken as arguments since ReactiveML has higher order processes Behaviors must reflect the structure of the program starting with parallel composition This is illustrated by the following example which defines a com binator par_comb that takes as inputs two processes q1 and q2 and runs them in parallel in a loop let process par_comb q1 q2 loop run q1 run q2 end The synchronous parallel composition terminates when both branches have ter minated It means that the loop is non instantaneous if either q1 or q2 is non instantaneous To represent such processes behaviors include the parallel com position simply denoted Similarly we can define another combinator that runs one of its two inputs depending on a condition c let process if_comb c q1 q2 loop if c then run q1 else run q2 end In the case of if_comb both processes must be non instantaneous As we want to abstract values we represent the different alternatives using a non determinstic choice operator and forget about the conditions It is also necessary to have a notion of sequence denoted in the language of behaviors as illustrated by
29. ve call induces an implicit pause Hence it is impossible to have instantaneous recursions at the expense of expressivity For instance in the server example of Section 2 2 a message could be lost between receiving a message on add and awaiting a new message The causality analysis of Lucid Synchrone 10 is a type and effect system using row types It is based on the exception analysis defined by Leroy et al 17 Both are a more direct application of row types 26 whereas our system differs in the absence of labels in rows 8 Conclusion We have presented a reactivity analysis for the ReactiveML language The idea of the analysis is to abstract processes into a simpler language called behaviors using a type and effect system Checking reactivity of behaviors is then straight forward We have proven the soundness of our analysis that is that a well typed program with reactive effects is reactive Thanks in particular to the syntactic separation between functions and processes the analysis does not detect too many false positives in practice It is implemented in the ReactiveML compiler and it has been proven very useful for avoiding reactivity bugs We believe that this work can be applied to other models of cooperative scheduling Acknowledgments This work would not have been possible without previous experiments made with Florence Plateau and Marc Pouzet Timothy Bourke helped us a lot in the preparation of this article We are grate
30. ve systems Software Practice and Experience 21 4 1991 401 428 Cuogq P Pouzet M Modular Causality in a Synchronous Stream Language In European Symposium on Programming 2001 Dimino J Lwt User Manual 2014 http ocsigen org lwt Engelschall R Portable multithreading The signal stack trick for user space thread creation In USENIX Annual Technical Conference 2000 Huet G A unification algorithm for typed A calculus Theoretical Computer Science 1 1 1975 27 57 Jeffrey A Functional reactive programming with liveness guarantees In Inter national Conference on Functional Programming 2013 Jones S Gordon A Finne S Concurrent Haskell In Principles of Programming Languages 1996 295 308 Lee O Yi K Proofs about a folklore let polymorphic type inference algorithm Transactions on Programming Languages and Systems 20 4 1998 707 723 Leroy X Pessaux F Type based analysis of uncaught exceptions Transactions on Programming Languages and Systems 22 2 2000 340 377 Lucassen J M Gifford D K Polymorphic effect systems In Principles of Pro gramming Languages 1988 Mandel L Pouzet M ReactiveML a reactive extension to ML In Principles and Practice of Declarative Programming 2005 Mandel L Pasteur C Reactivity of cooperative systems extended version Re search Report 8549 INRIA 2014 Available at http reactiveml org sas14 Mandel L Pasteur C Pouzet M
31. w variables that appear only once are printed The analysis can also handle combinators like the par_comb and if_comb ex amples of Section 3 1 Here is another more complex example using higher order functions and processes We define a function h_o that takes as input a combi nator f It then creates a recursive process that applies f to itself and runs the result T Some behaviors are simplified using the extension described in Appendix D 20 let h_o f let rec process p let q f p in run q in p val h_o a process run rl r2 gt a process r1 gt a process run rl r2 If we instantiate this function with a process that waits an instant before calling its argument we obtain a reactive process let process good run h_o fun x gt process pause run x val good a process run run rec rl run run rl This is no longer the case if the process calls its argument instantaneously The instantaneous recursion is again detected by our static analysis let process pb run h_o fun x gt process run x val pb a process run run rec rl run run rl1 W This expression may produce an instantaneous recursion Another process that can be analyzed is a fix point operator It takes as input a function expecting a continuation and applies it with itself as the continuation This fix point operator can be used to create a recursive process let rec fix f
32. y prints warnings and does not reject programs ML functions are always considered instantaneous So they are reactive if and only if they terminate Since we do not want to prove their termination our analysis has to distinguish recursions through functions and processes This allows us to assume that ML functions always terminate and to issue warnings only for processes Furthermore we do not deal with blocking functions such as I O primitives that can also make programs non reactive Indeed such functions should never be used in the context of cooperative scheduling There are standard solutions for this problem 22 This analysis does not either consider the presence status of signals It over approximates the possible behaviors as in the following example let rec process imprecise signal s default gather fun x y gt O in present s then else implicit pause Q run imprecise W This expression may produce an instantaneous recursion The present then else construct executes its first branch instantaneously if the signal is present or executes the second branch with a delay of one instant if the signal is absent This delayed reaction to absence first introduced by Boussinot 9 avoids inconsistencies in the status of signals In the example the signal is absent so the else branch is executed It means that the recursion is not instantaneous and the process is reactive Our analysis still prints a warning because if
Download Pdf Manuals
Related Search