Reactivity of Cooperative Systems: Application to ReactiveML
Contents
1. and finally p For instance Ld s run k2 e 3 means pd K1 run K2 0 K3 RR n 8549 Reactivity of Cooperative Systems 7 Behaviors must reflect the structure of the program starting with parallel composition This is illustrated by the following example which defines a combinator 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 qi run q2 end The synchronous parallel composition terminates when both branches have terminated It means that the loop is non instantaneous if either q1 or q2 is non instantaneous To represent such processes behaviors include the parallel composition 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 qi 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 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 is2. AT ea m T U ele v gt v ula H rec x v A a T E tt 4 gt U rec t v U S CL 2 E tt E b e gt process e1 cl S 2 ause ff O EUE b y P S run e gt S E b E2 b e MA el ez gt bi A bo ff LET PAR M let e and T2 eg N 3 ES et Ti e and 2 e in e3 Ei tt Ey tt E3 b3 y e v e2 Va Gal v1 2 vo S gt 3 LET DONE AUBUER let x e and 2 e2 in e3 _ gt 3 S E tt E b E tt e gt n nes a ei En ngs present e then e else eg et el e present e then e1 else eg lt 4 e2 E tt Ett E em ngs En nes e f E ff E H do c1 when e EF do e when n S E tt FE tt e gt n nes e gt v S S EUE tt do when e _ gt U S E ff e FE e LOOP STUCK EF loop e ar e loop e Bu do e when c gt do cl when n S Ey tt E2 tt ey n Ga gt V S S E yUE2U v n tt emit eg e9 T O S Ey tt E2 b 1 sat v loop e E e Loop UNROLL E UF2 b loop e ae re Figure 3 Big step semantics RR n 8549 Reactivity of Cooperative Systems 25 Ey tt E2 tt Cy SUF 2 v2 0 tt S S v K v S E UE2 tt e1 e2 a 2 v1 V2 Ey tt Eo tt E b ei V1 e2 E v2 n fresh ela n ae c S n v1 v2 m E UEUE b signal x default e1 gather e2 ine ese E tt Ei tt E tt EN oy
3. The analysis is very useful to detect early small reactivity bugs such as the one presented Sec tion 2 1 We have also used the analysis on bigger applications a mobile ad hoc network simu lator 1800 Source Lines Of 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 RR n 8549 Reactivity of Cooperative Systems 18 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 6 5 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 schedul
4. Notre travail est appliqu et mis en uvre dans le langage synchrone fonctionnel ReactiveML Il g re la r cursivit les processus d ordre sup rieur et les signaux de premi re classe Nous prouvons la correction de notre analyse par rapport la s mantique grands pas du langage un programme bien typ avec des effets r actifs est r actif L analyse est facile mettre en uvre et assez g n rique pour tre applicable d autres mod les de concurrence tels que les coroutines Ce rapport de recherche est la version tendue de l article 20 publi dans les actes de la 21 me dition de l International Static Analysis Symposium Mots cl s Ordonnancement coop ratif Syst mes de types S mantique Langages fonction nels Langages synchrones Reactivity of Cooperative Systems 3 1 Introduction Most programming languages offer lightweight thread facilities 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 efficient 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 synchronizatio
5. 32 33 34 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 1 1990 1 34 Vouillon J Lwt a cooperative thread library In ACM workshop on ML 2008 RR n 8549 Reactivity of Cooperative Systems 22 OF e OF e2 Ore OF 61 OF eg Orv kre kre kF e1 2 kF Awe kF e1 e2 kL rec TU lke OFe kre kk eg kre k F process e 1 F rune 1 F pause kF let x ei and z2 eg ine OF e Ob eg kte U K e U e k F signal x default e gather ez ine kk emit e1 e2 Ore 1Fe lk eg OFe kre kk eg lke 1 F present e then e else e2 kt if e then e else eg 1 F loop e IF e U C c lk e2 like Ore 1H do e until e x gt ez 1 F do e when e Figure 2 Well formation rules A Well formation of expressions In order to separate pure ML expressions from reactive expressions we define a well formation predicate denoted k C e with k 0 1 An expression e is necessarily instantaneous or combinatorial if 0 C e It is reactive or sequential in classic circuit terminology if 1 e The rules defining this predicate are given in Figure 2 The design choices of t
6. E tt E HD y e x process ey ae ei EUE b y run e aoe e Case pause The derivation is already finite e Case present e then e else ca As in the first case II E tt e n S RR n 8549 Reactivity of Cooperative Systems 28 The typing rule is Pe Ti T2 event _ 0 Thke 7 Ky Th eg 7 ke T F present e then e else ez 7 Ki 0 K2 There are then two cases depending on the status of n Ifn S We notice that fst k1 e K2 fst K 0 so we can apply the induction hypothesis on the first instant behavior of e and conclude Ifn S The derivation is finite e Case do e1 when ca We can use the same reasoning It is interesting to note that the behavior associated with the expression i e k e is not equal to the behavior of the body as one might expect so that we can apply the induction hypothesis e Case let x e and x2 eg in e When we compute the first instant of a sequence there are two possible cases If k k2 4 then we have that fst K fst K1 fst k2 From 1 amp 2 we get that either x which implies that b ff or va which implies that b ff using Lemma 4 So we are sure that b A bo ff We can then apply the induction hypothesis on e1 and e2 using the rule LET PAR Otherwise we have that fst x fst K1 fst K2 fst 3 We can apply the induction hypothesis on e1 e2 and e3 using either LET PAR or LET DONE depending o
7. a process r1 gt b process r2 gt unit process rec r3 run rl run r2 r3 There is no warning when defining the combinator because it is not possible to decide its re activity Indeed the synchronous parallel composition terminates when both branches have terminated It means that the loop is non instantaneous if either q1 or q2 is non instantaneous Formally the computed behavior is reactive because free behavior variables are considered to be non instantaneous see Definition 2 The reactivity is then checked at the instantiation If we instantiate the par_comb combinator with two anonymous processes one instantaneous and the other non instantaneous then we obtain a process that is indeed reactive so no warning is printed let process pl run par_comb process process pause val pl unit process run rec r run 0 run r However if the two processes are instantaneous then the loop becomes instantaneous The behavior that results is obviously non reactive so a warning is shown let process p2 run par_comb process process val p2 unit process run rec r run 0 run 0 r W This expression may produce an instantaneous recursion Here is another more complex example using higher order functions and processes We define a function h_o that takes as input a combinator f It then creates a recursive process that 4Some behaviors are simplified using th
8. extended with constructs for creating process and running run processes waiting for the next instant pause parallel definitions let and declaring signals signal emitting a signal emit and several control structures the test of presence of a signal present the unconditional loop loop weak pre emption do until and suspension do when The expression do e until s x 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 e2 let _ e and e in 1 2 await e1 x in e2 do loop pause until e1 x e2 let rec process f 2 Tp 1 in e2 let and _ amp 1 n e2 l gt I gt I gt Z let f rec f x1 r process e1 in ez 4 2 Types Types are defined by T a T TxT T T Tprocess k 7 7 event types o T YQ 0 Ya c type schemes r 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 T T2 event of a signal is parametrized by the type 71 of emitted values and the type T2 of the received value since a gathering function of ty
9. 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 it is true for one instant it is true for the following ones e Case e1 e2 and rec x v By Hypothesis 1 e Case run e We know that 0 F e and run e is well typed The expression e rewrites to a value by Hypothesis 1 that is necessarily of the form process e because it is the only kind of value that can have type 7 process k So there exists IT such that II E tt e care process Then we can construct the following type derivation Pe T R T F process e T process k k 0 T C run process e1 T run K 4 We can apply the induction hypothesis as the first instant behavior of e1 ie fst x is smaller than the first instant behavior of run process e1 which is also the first instant behavior of run e because e and process e1 have the same type by subject reduction Indeed we have fst run x K run fst run fst x Using the induction hypothesis we can build the complete derivation of run e II Il
10. crucial as the good_rec process is reactive while bad_rec loops instantaneously As it is defined recursively the behavior asso ciated with the good_rec process must verify that x e run k The run operator is associated with running a process This equation can be solved by introducing an explicit recursion operator H so that Kk pd e run Recursive behaviors are defined as usual uo Kb yd Fi p K if fov K We denote fbu the set of free behavior variables in x 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 where is the behavior of the body of the loop is thus defined as a recursive behavior by K uo 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 define 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 Ki ka Kit k2 Kil ka KJ s L ot Ki Ko K1 K2 k K2 4 k s24 k Ko Hd C k runk Note that function calls are not non instantaneous The behavior e is as expected non instan taneous The fact that variables are considered non in
11. e gt n e v e gt H nes e gt S S S S FUE tt FUE 0 do e1 until e x gt eg gt v do e until e x gt ez f Golf S n E tt Eff e gt n n 4S ey ae el E EUE do ei until e x gt e2 a do e until e x gt e2 Figure 4 Remaining rules for the big step semantics e The do when construct executes its body only if the signal n is present If the body termi nates that is if it rewrites to a value v then the construct also terminates instantaneously and rewrites to the same value e The unconditional loop keeps executing its body until that body stops to wait for the next instant that is until its termination status b becomes false In particular an expression like loop where the body always terminates instantaneously does not have a semantics as it would require an infinite derivation tree e emit e e2 evaluates e into a signal name n and adds the result of the evaluation of e2 to the multi set of values emitted on n e The declaration of a signal evaluates the default value and combination function and then evaluates the body after substituting the variable x with a fresh signal name n In this paper we have kept implicit the sets of signal names that are used to ensure the freshness of this name see 19 for the details e The preemption in ReactiveML is weak that is a process can only be preempted at the end of the instant This is reflected by the fact that e is always eva
12. 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 U x 1 gt let x run p x and 1 run par_map p 1 in x 1 W This expression may produce an instantaneous recursion This process has instantaneous recursive calls but it is reactive because the recursion 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 9 1 in run par_map p 1 Consequently our analysis only 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 RR n 8549 Reactivity of Cooperative Systems 6 recursions through functions and processes This allows u
13. is absent This is reflected in the behavior associated with the expression Similarly for do e until e x e2 the expression e2 is executed at the instant following the presence of e e The encoding of primitives given earlier yields the expected behaviors For example con sider the case of e1 2 The nlki TF O unit O Treo Tala TF let e and O in e2 T k 0 k2 TF e1 e2 T2 K1 0 Ke It is easy to show that x1 0 k2 k1 2 We can also show that e1 e2 has a behavior RR n 8549 Reactivity of Cooperative Systems 12 equivalent to 1 amp 2 or that await e1 x in e2 has behavior e e k2 k2 reading the value of a signal takes at least one instant e The pause operator cannot be encoded using the delay to the reaction to absence as in 19 by pause signal s default gather Az Ay Q in present s then else 7 We have chosen to completely abstract values As in the imprecise example of Section 2 2 we do not consider the fact that the signal s is always absent so that only the second branch of the present is executed The consequence is that the behavior computed for this encoding that is 0 0 e 0 0 is the opposite of the expected behavior of pause e The loop construct can be encoded as a recursive process by loop e run rec 1 Ar process run z run l x process e Unlike pause we could have removed loop from our kernel and used thi
14. 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 s behavior is printed and behavior variables are denoted r let process pl val pl unit process 0 r1 let process p2 pause val p2 unit process r2 let 1 pl p2 val 1 unit process 0 r list RR n 8549 Reactivity of Cooperative Systems 13 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 inference 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 M for unification of behaviors It takes as input two beha
15. 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 Exposing concurrency in the language makes it possible to express the analysis easily which would not have been the case if concurrency had been implemented as a library e A novel approach to subeffecting 23 that is subtyping on effects based on row polymor phism 26 in Section 4 4 It allows to build a conservative extension of the existing type system with little overhead e 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 Sec tion 7 The work presented here is implemented in the ReactiveML compiler and it has already helped detecting many reactivity bugs The implementation the source code of the examples and an online toplevel are available at http reactiveml org sas14 lhttp www reactiveml org RR n 8549 D a e U N o 10 11 12 13 Reactivity of Cooperative Systems 4 2 Overview of the approach ReactiveML extends ML with programming constructs inspired from synchronous languages 6 It introduces a built in notion of parallelism
16. 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 simple 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 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 processes that is func tions whose execution can span several logical instants Processes are defined using the process keyword The clock process is parametrized by a float timer and a signal s Signals are com munication channels between processes with instantaneous broadcast The process starts by initializing a local 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 iterati
17. 0 377 Lucassen J M Gifford D K Polymorphic effect systems In Principles of Programming 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 Application to ReactiveML In Static Analysis Symposium 2014 Mandel L Pasteur C Pouzet M 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 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 Program ming Languages and Systems 11 4 1989 633 649 RR n 8549 Reactivity of Cooperative Systems 21 30 31
18. Reactivity of Cooperative Systems Application to ReactiveML extended version Louis Mandel C dric Pasteur RESEARCH REPORT N 8549 June 2014 Project Teams PARKAS ISSN 0249 6399 ISRN INRIA RR 8549 FR ENG I d informatics mathematics Reactivity of Cooperative Systems Application to ReactiveML extended version Louis Mandel C dric Pasteur Project Teams PARKAS Research Report n 8549 June 2014 29 pages Abstract Cooperative scheduling enables efficient sequential implementations 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 language 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 reactiv
19. allest signal environment S the set of present signals such that 49 E b Ci mans Ci 1 which means that during the instant 7 in the signal environment S the expression e rewrites to e 41 and emits the signals in The boolean b indicates if e 1 has terminated Additional conditions express for instance the fact that the emitted values in FE must agree with the signal environment An execution 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 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 x This function is formally defined by fst k1 if k fst k1 fst k2 otherwise fst k1 k2 l fst ud x fst k d ud K The important property of this function is that if a behavior of e is reactive as defined in Section 3 2 then fst x is finite Hence we can prove by induction on the size of fst x that the semantics derivation is finite The soundness theorem is stated as follows Theorem 2 Soundness IPT Ce Yl K andr and k are reactive and we suppose that function S E b calls terminate then there exists e such that e rar e andT He rT K with K reactive Proof The proof has two parts The first part is the p
20. ant of and all the recursions inside k 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 ud k In the case of the sequence K1 K2 we can 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 The behaviors 0 and e are always reactive The other rules only checks that sub expressions are reactive Using this definition we can see for example that the behavior uo is reactive pre el dtd preg Ob d e p 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 behav ior resp is the neutral element of and resp The relation also satisfies the following rules where op is or or il am Ki K2 K Ka K Ky K2 Ko 1 Ld Ky UQ Ke run K run k2 K1 OP K2 K1 OP Ka It is easy to show for example that uo e 0 run run pd e run An important property of this relation is that
21. d behavior K We write F e r 0 when the behavior of the expression e is equivalent to 0 The initial typing environment Ip gives the types of primitives To true bool fst Vay a2 a1 X a2 gt a1 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 e 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 x behavior and the MASK rule are related to subeffecting and will be discussed in Section 4 4 e 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 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 e 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 a
22. e effects is reactive The analysis is easy to implement and generic enough to be applicable to other models of concurrency such as coroutines This research report is the extended version of the article 20 published at the 21st International Static Analysis Symposium Key words Cooperative scheduling Type systems Semantics Functional languages Syn chronous languages RESEARCH CENTRE PARIS ROCQUENCOURT Domaine de Voluceau Rocquencourt B P 105 78153 Le Chesnay Cedex R activit des Syst mes Coop ratifs Application ReactiveML version tendue R sum L ordonnancement coop ratif permet l impl mentation s quentielle efficace de la concurrence Il est largement utilis pour fournir des threads l gers sous forme de biblioth ques ou de constructions de programmation dans de nombreux langages de programmation Toutefois il appartient aux programmeurs d appeler des primitives de coop ration pour assurer la r activit de leurs programmes Nous pr sentons une analyse statique qui v rifie la r activit des programmes en les abstrayant en comportements l aide d un syst me de types effets Notre objectif est de trouver un bon compromis entre la complexit de l analyse et sa pr cision pour les programmes r actifs typiques La simplicit de l analyse est obligatoire pour que le programmeur soit en mesure de comprendre les messages d erreur et comment r soudre les probl mes de r activit
23. e extension described in Appendix D RR n 8549 Reactivity of Cooperative Systems 16 applies f to itself and runs the result 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 rl 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 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
24. eML 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 Shttp x10 lang org RR n 8549 Reactivity of Cooperative Systems 19 The analysis is also restricted to the first order setting In ULM 7 each recursive 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 straightforward 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 usef
25. er 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 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 behavio
26. er 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 Ku e 0 ilk K K KK u r ruk 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 calling 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 3Precedence of operators is the following from highest to lowest run
27. es given in Section 3 2 are easily translated into an algorithm for checking the reactivity of behaviors that is polynomial in the size of behav iors Inference simplifies behaviors during the computation but does not necessarily compute the smallest behavior possible For instance simplifying can be costly in some cases so it only checks simple cases e g if k 0 or K e 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 6 3 Handling references References are not included in the kernel of our language However they are relevant as they can be used to encode recursivity as in the following example that creates a process that loops instantaneously let landin let ref process in f process run f If val landin unit gt unit process rec rl run 0 r1 W This expression may produce an instantaneous recursion As our analysis does not have any special case for recursive processes and only relies on unifica tion it is able to detect such reactivity problems even though there is no explicit recursion 6 4 Evaluation
28. his analysis like the fact that pairs must be instantaneous are discussed in 19 k F e means that 1 F e or OF e that is that e can be used in any context This is true of any instantaneous expressions as there is no rule with 0 e in the conclusion The important point is that the body of functions must be instantaneous while the body of a process may be reactive B Big step semantics The big step semantics has been introduced in 19 We recall its definition here since it is used in the soundness theorem of the type system B 1 Notations Signal environment A signal environment S is a function S di 91 7 1 m1 dk gk mr nx that maps a signal name n to a tuple di gi mi where d is the default value of the signal gi its combination function and m is the multi set of values emitted during the reaction If the signal n has the type 71 72 event then these fields have the following types di T gi T1 gt T2 gt T2 Mi T2 multiset RR n 8549 Reactivity of Cooperative Systems 23 We denote S n di S9 ni gi and S ni mi We also define S n fold gi mi di where fold f v1 W m vo fold f m f v v2 fold f 0 v2 v We denote n S when the signal n is present that is when S n 4 0 and n Z S otherwise Events An event E is a function mapping a signal name to a multi set of values E 2 mi na S Mr nx Events represent the values emitted during an instan
29. inite behavior i e H k gt fatl E K Proof By induction on the structure of behaviors This property is used in the soundness proof to guaranty that at each instant the reaction is finite since its behavior is finite C 2 Soundness We do not try to prove that functions terminate and we focus completely on processes We assume that all functions terminate which is reflected in the APP rule of Figure 1 by the fact that the behavior of the application is always the instantaneous behavior 0 This hypothesis is made possible by the syntactic distinction between functions and processes It must be expressed formally with respect to the big step semantics before we can show soundness To do so we reuse the predicate 0 C e which is defined in Appendix A and means that the expression e is surely instantaneous Hypothesis 1 Function calls always terminate For any expression e such that OH e there exists a finite derivation II and a value v such that IT E tt e gt U S We first need to prove the soundness of our definition of non instantaneous behavior as expressed in the following lemma RR n 8549 Reactivity of Cooperative Systems 27 Lemma 4 An expression whose behavior is not instantaneous never reduces instantaneously E b Cheirlx A KL A ee gt b ff Proof By induction on the derivation of the big step semantics We can now prove the soundness theorem Proof The proof has two parts
30. it preserves reactivity It is expressed as follows Property 1 if k k2 and RH k then RH ka Proof By induction on the proof of k ke RR n 8549 Reactivity of Cooperative Systems 9 4 The type and effect system The link between processes and behaviors is done by a type and effect system 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 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 A type system is a simple way to specify a higher order static analysis It can be implemented efficiently using classic destructive unification techniques 16 4 1 Abstract syntax We consider here a kernel of ReactiveML v c v v n Az e process e II x c e e Ave ee rec x v process e run e pause let x e and qx 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
31. luated regardless of the status of the signal n It also means that when the signal is present e2 is executed at the next instant C Proof of soundness The intuition of the proof of soundness Theorem 2 is that the first instant of a reactive be havior is a finite behavior without any recursion We then prove the finiteness of the semantics derivation by induction on the size of behaviors RR n 8549 Reactivity of Cooperative Systems 26 C 1 First instant of a behavior Definition 3 The first instant of a behavior denoted fst k is the part of the behavior that cor responds to the execution of the first instant of the corresponding process It is formally defined by fst fst run x run fst x fst k1 fst K2 fst k1 K2 fst K1 fst K2 fst k1 k2 ee Tery Teatri Tata otherwise fst ud r fst K d ud K fst 0 fst e 0 r fst k1 k2 In the case of a recursive behavior the first instant behavior is well defined only if the behavior is reactive that is if the recursion is not instantaneous Definition 4 A behavior is finite denoted k K if it does not contain any recursive behavior The finite behaviors k are defined by k u 0 D K k k k k k un We can now express the most important property of reactive behaviors that is that the first instant of a reactive behavior is finite Property 3 If k is reactive Definition 2 then fst x is a f
32. lways terminate instantaneously That is why there is no behavior associated with functions there are no behaviors on arrow types unlike traditional type and effect systems RR n 8549 Reactivity of Cooperative Systems 11 T lt T x T lt To c Thke m 0 The g 7 0 Thka 7 0 Tke 7 0 TF e1 2 T1 X T2 0 Txinte r 0 Thea rm n 0 Th eg 72 0 APP TF Aze gt T2 0 UG eg 74 0 T x rHv r 0 Threcx v rT 0 The rlk PROCESS T F process e T process K K 0 TF e rprocess K _ 0 T F pause unit Tt run c T l run DG TR Db eg 7 K2 Tai gen m e1 T 2 gen T2 e2 l F e3 T ka T F let x e and to eg ines T Ky K2 3 Thre 7 0 The n nm 1m 0 DE Ti Ta event C6 Tl T signal x default e gather es ine 7T 0 K The m 72 event _ 0 Tre 7tl ki Th eg 7 ka T F present e then e else ca 7 k1 0 Ko T Fe 71 72 event _ 0 Treg 0 The rlk T F emit e e2 unit 0 TF loop e unit 0 K Deu T e TF e 1 72 event _ 0 LI 72 2 T ke T F do e until e x gt e2 T K1 k2 Pe T R Tt e m 72 event _ 0 T H doe whene 7 K e The rTlk o g fbv T T oe The r x pg e Figure 1 Type and effect rules e In the case of present e then e else ez the first branch cu is executed immediately if the signal e is present and the second branch eg is executed at the next instant if it
33. n European Sym posium on Programming 2004 8 Boudol G Typing termination in a higher order concurrent imperative language Infor mation and Computation 208 6 2010 716 736 RR n 8549 Oo 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 Reactivity of Cooperative Systems 20 Boussinot F Reactive C an extension of C to program reactive 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 International 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 Transac tions 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 34
34. n primitives like locks The downside of cooperative scheduling is that it is necessary to make sure that threads actually cooperate e 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 e Blocking functions like operating system primitives for I O cannot be called The solution to the latter is simple never use blocking functions inside cooperative threads All the facilities mentioned earlier provide either I O libraries compatible with cooperative scheduling or a means to safely call blocking functions 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 complete 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 Sec tion 6 5 The contributions of this paper are the following e A
35. n 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 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 O 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 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 local signal s 2 2 Intuitions and limitations In the previous example we have seen the first cause of non reactivity instantaneous 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
36. n the values of b and bo e Case loop e We have that fst 0 0 fst so we can apply the induction hypoth esis on e As the behavior 0 is reactive we know that By applying Lemma 4 we get that b ff so we reconstruct the complete derivation for e using the LOOP STUCK rule D Simplifying behaviors The behaviors computed by the type system of Section 4 are very big For instance the behavior associated with the timer example is 0 0 0 0 0 This behavior is unnecessarily detailed and as big as the source program It is however equivalent to 0 We would like to use the equivalence relation on behaviors defined in Section 3 3 in our type system to reduce the size of the computed behaviors This can be expressed as a new typing rule that allows to simplify behaviors at any time using the equivalence relation We denote Hs the type system augmented with the new rule Pae T R ki K Equtv S k1 1 2 Tg e 7 ke RR n 8549 Reactivity of Cooperative Systems 29 In order to use this rule we have to show that it is admissible that is that it does not change the set of accepted programs This is ensured by the fact that the equivalence relation preserves reactivity Property 1 which is one of the conditions requested by the soundness proof Hence an expression of type 7 and of behavior has also type 7 and behavior x if 7 is equivalent to T and K to K Prope
37. of reactivity although there is no explicit recursive process 6 Discussion 6 1 The run operator So far we have not justified the presence of the run operator in the language of behaviors It is there to ensure that even after adding simplification to the type system the behavior associated with a recursive process is always a recursive behavior that is wd k with fou x Suppose that we remove the run operator from the language of behaviors Now consider the process rec p process run p In the type system without run we could give it the instantaneous behavior 0 and miss the instantaneous recursion I tg p Bprocess 0 e 0 I tg runp 6 0 e O e 0 l ksrunp 8B 0 I Fs process run p 8 process 0 e 0 EQUIV T Fs rec p process run p Bprocess 0 0 RR n 8549 Reactivity of Cooperative Systems 17 where IY Tp Bprocess 0 e Thanks to the addition of run run p now has a behavior equal to run Then the only way to type the process is to give it the behavior ud run 6 amp where is not constrained This also explains why there is no equivalence rule to simplify a run For instance run 0 is not equivalent to 0 6 2 Implementation The type inference algorithm of ReactiveML has been extended to compute the behaviors of processes with minimal impact on its structure and complexity thanks to the use of row poly morphism for subeffecting see Section 4 4 The rul
38. on 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 instant let process print_clock s loop do print_string top print_newline 7 The vocabulary is the one of synchronous languages not the one of FRP RR n 8549 14 17 18 19 Reactivity of Cooperative Systems 5 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 o
39. pe T T2 72 is applied RR n 8549 Reactivity of Cooperative Systems 10 Types schemes quantify universally over type variables and behavior variables 9 We denote ftv r resp fbu 7 the set of type resp behavior variables free in r and fu r ftu r fou r Instantiation and generalization are defined in a classic way ola T lt Va o olo RI lt Y 0 gen r e T 7 if e is expansive gen r e T Va V T where 6 fu r fu T otherwise Analogously to the treatment of references in ML we must be careful not to generalize ex pressions 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 Here is an example of program wrong program that would have been accepted if there is no distinction between expansive and non expansive expressions let emit_s signal s default gather fun x y gt x y in fun x gt emit x in emit_s 1 emit_s error 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 7 7 if they have the same structure and their behaviors are equivalent 4 3 Typing rules Typing judgments are given by T e 7 amp meaning that in the type environment I the expression e has type T an
40. r 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 emission on a second channel in a given program The idea of using a type and effect 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 Reactiv
41. roof that the result is well typed We use classic syntactic techniques for type soundness 24 on the small step semantics described in 19 RR n 8549 Reactivity of Cooperative Systems 15 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 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 run q 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 row variables that appear only once are printed The analysis can also handle combinators For instance the type system computes the following behavior for the par_comb example of Section 3 1 let process par_comb q1 q2 loop run q1 run q2 end val par_comb
42. rty 5 fT Cae TR then Ce withk K dnd YT Proof Straightforward by induction on the type derivation The immediate consequence of this property is that the augmented type system is also sound We can also simplify some rules by combining the original rule with the EQUIV rule TF g e1 T2 0 TF 2 71 4 Ta gt Ta lU T x n r eventkse Tl T Hs signal x default e gather ez nc Tl Thse Tl Fg e 11 72 event 0 Pse TR T Hs doe whene 7 k T Fs loop e unit 6 RR n 8549 informatics mathematics TUA RESEARCH CENTRE PARIS ROCQUENCOURT Domaine de Voluceau Rocquencourt B P 105 78153 Le Chesnay Cedex Publisher Inria Domaine de Voluceau Rocquencourt BP 105 78153 Le Chesnay Cedex inria fr ISSN 0249 6399
43. s encoding without affecting the results given by the reactivity analysis Indeed by applying the rules here we have that loop Vo a process d a process ud run run If we assume that T F e T K then the behavior of this encoding is run Lud run K run g It is not equivalent to in the sense of Section 3 3 but it is reactive iff K is reactive as the run operator does not influence reactivity see Definition 2 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 e 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 An example of typing derivation justifying the presence of the run operator will be given in Section 6 1 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
44. s 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 Q in present s then else implicit pause O 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 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 serv
45. stantaneous means that any process taken as argument is supposed to be non instantaneous The reactivity is then checked when this variable is instantiated with the actual behavior of the process For the sequential and the RR n 8549 Reactivity of Cooperative Systems 8 parallel composition only one of the two behaviors have to be non instantaneous to makes the whole behavior non instantaneous For a non deterministic choice the two behaviors have to be non instantaneous to be sure that the behavior is non instantaneous since only one of the two behaviors will be actually executed Finally the instantaneity of a recursive behavior or a run only depends on the instantaneity of their body A behavior is said to be reactive if for each recursive behavior ud K the recursion variable does not appear in the first instant of the body K 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 k is reactive if OH k where the relation Rt K is defined by ER RF ki not K1 RF k2 RFO RF RF RF ki ko RF k Kit Ot ko RF k RF k2 RF ki RF k2 RUuU F k RE ki k2 RF k k2 RF k k2 RF ud rk REkK Re run The predicate R C means that the behavior is reactive with respect to the set of variables R that is these variables do not appear in the first inst
46. t S is the event associated with the signal environment S Operations on signal environments and events The union of events is the point wise union that is if E E U Eo then for all n Dom E1 U Dom E2 E n E n En Similarly the inclusion of events is the point wise inclusion We define the inclusion of signal environments by RL E So iff SP C SF B 2 Big step semantics At each instant the program reads inputs J and produces outputs O The reaction of an expression is defined by the smallest signal environment S for the relation E such that i i41 where LU E ES 1 Si Ove E 2 S C Sfp and 7 C SF 3 1 The signal environment must contain the inputs and emitted signals 2 The outputs are included in the set of emitted signals 3 Default values and combination functions are kept from one instant to the next The rules defining the relation are given in Figure 3 and Figure 4 e The rule for pause shows the meaning of the boolean b if it is false it means that the expression is stuck waiting for the next instant e The let and construct executes its two branches in parallel until both are terminated the termination status is tt e The present construct executes the then branch immediately if the signal is present but it executes the else branch on the next instant if it is absent RR n 8549 Reactivity of Cooperative Systems 24 Fy tt Eo tt Est Et y pL
47. ul 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 arti cle We are grateful for the proofreading and discussions with Guillaume Baudart and Adrien Guatto Finally we also thank the reviewers for there numerous comments and suggestions References 1 Abel A Pientka B Well founded recursion with copatterns In International Conference on Functional Programming 2013 2 Amadio R Dabrowski F Feasible reactivity in a synchronous 7 calculus In Principles and Practice of Declarative Programming 2007 221 230 3 Amtoft T Nielson F Nielson H Type and Effect Systems Behaviours for Concurrency Imperial College Press 1999 4 Atkey R McBride C Productive coprogramming with guarded recursion In Interna tional Conference on Functional Programming 2013 5 Barthe G Frade M J Gim nez E Pinto L Uustalu T Type based termination of recursive definitions Mathematical Structures in Computer Science 14 01 2004 97 141 6 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 7 Boudol G ULM A core programming model for global computing I
48. viors and returns a substitution that maps behavior variables to behaviors that we denote 61 k1 2 gt Ka During unification the behavior of a process is always either a behavior variable a row K or a recursive row uo x Therefore the unification algorithm only has to consider these cases HLR R b gt Ld l if occur check x br K otherwise Uk 9 R Un kK gt l HLR 1 ko Da hi gt k2 D pi k d p fresh Urn wos Ki G1 K2 Un Ka D Ki d1 let Ki yd k pi in HLR Ki bi K2 It should be noted that unification never fails so that we obtain a conservative 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 unreadable The purpose of the MASK rule is to remedy this by using effect masking 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 Comparison with traditional approaches Usually subeffecting is not e
49. xpressed as a syntax directed rule For instance in 31 23 it is defined as we reuse the notations of our type system for comparison The rlk KCK Dies The order E on effects is given by set inclusion when effects are sets 31 of regions for example In our case it is defined by K1 K2 k C RL Ko Kg Eki ko erie 1E Ko In the work of Amtoft et al 3 effects must be simple that is effects on arrows are syntactically forced to be variables A constraint set C is added to the type system to keep track of the RR n 8549 Reactivity of Cooperative Systems 14 relations between variables and effects Subeffecting is then expressed as T Cke 7t k T CU k E OLE process e Tr process 0 These three formulations appear to be equivalent Indeed our system and the one of Amtoft et al 3 are just syntax directed versions of the classic approach where the subsumption rule is mixed with lambda abstractions or process abstractions in our case 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 big 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 sm
Download Pdf Manuals
Related Search