Re: [Caml-list] [ANN] PEC ver. 1.1
(2012/04/19 7:32), Daniel Bünzli wrote: Yes because the semantics of [e] is violated, it has three values at the same time, the current value during the update cycle, the value 1 and the value 2. Now suppose I reason about the semantics of [e] in this program, it has a well-defined outcome *for [e] itself* if I send it a value [v]. However if you now add a new module that uses [e] and does : Thank you for helping me understand with your explanation. If I understand correctly sending [v] to [e] immediately during update cycle are violate the semantics because it cause more than one values on one event at the same time. Using React, let e, sender = E.create () in let e' = E.map (fun x - Queue.add q (fun () - sender 1); x + 1) e in let e'' = E.map (fun x - Queue.add q (fun () - sender 2); x + 1) e in does this code violate the semantics of events? If so, PEC is also unsound. I'd like to know PEC is unsound or not. So if I understand correctly you are doing manual memory management via (un)subscribe of the leaves of the dependency tree and instead of having weak forward pointers from events to their dependents you have regular backward pointers from events to the events they depend on. Once these leaves are subscribed we can follow them backwards to find out what their primitive event set is and understand what needs to be updated along the way. Yes, exactly. It may be an interesting approach to avoid weak pointers but I'd need more thinking to convince me it can correctly handles all the dark sides of leaks, fixed point definitions, signal initialization and dynamically changing dependency graph. By the way you still need to update the events in the correct order/and or only once to prevent glitches, how do you achieve that ? To prevent glitches, PEC distinct one update cycle to another by time identity. And calculated results are cached for same update cycle. Update order is straight forward. Just follow from leaf to primitive source event. It's not problem because only one primitive value changes at one update cycle. Best Regards, Ogasawara -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Call for participation iFM ABZ 2012 - program available
CALL FOR PARTICIPATION iFM ABZ 2012 ** 9th International Conference on Integrated Formal Methods (iFM 2012) 3rd International Conference on ASM, Alloy, B, VDM, and Z (ABZ 2012) Joint conferences in honour of Egon Boerger's 65th birthday, for his contribution to state-based formal methods 18 - 21 June 2012 CNR - Pisa, Italy http://ifm-abz.isti.cnr.it/ ** The iFM and ABZ conferences are co-located in order to host a joint conference in honour of Egon Boerger's 65th birthday. The conferences are organized by the Formal Methods Tools Lab at ISTI-CNR and take place at the Area della Ricerca CNR in Pisa from 18 to 21 June. The iFM conference series presents research on the combination of (formal and semi-formal) methods for system development, regarding modeling and analysis, and covers all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice. The ABZ conference is dedicated to the cross-fertilization of five related state- and machine-based formal methods, namely Abstract State Machines, Alloy, B, VDM and Z, which share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. KEYNOTES: * Egon Boerger (University of Pisa, Italy): Contribution to a Rigorous Analysis of Web Application Frameworks * Muffy Calder (University of Glasgow, United Kingdom): Process Algebra for Event-Driven Runtime Verification: a case study of wireless network management * Ian J. Hayes (University of Queensland, Australia): Integrated operational semantics: small-step, big-step and multi-step The joint conference is preceded by a full day devoted to two free TUTORIALS: * Eric C.R. Hehner and Lev Naiman (University of Toronto, Canada): Practical Predicative Programming Primer * Joost-Pieter Katoen, Thomas Noll (RWTH Aachen University, Germany), Alessandro Cimatti and Marco Bozzano (FBK, Trento, Italy): Safety, Dependability and Performance Analysis of Extended AADL Models The full program is available online: http://ifm-abz.isti.cnr.it/ IMPORTANT: The early registration fee deadline is 18 May. Students get a discount. The deadline for poster tool demo submissions is 22 April. -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] [ANN] PEC ver. 1.1
Le jeudi, 19 avril 2012 à 10:59, Satoshi Ogasawara a écrit : If I understand correctly sending [v] to [e] immediately during update cycle are violate the semantics because it cause more than one values on one event at the same time. Yes. Using React, let e, sender = E.create () in let e' = E.map (fun x - Queue.add q (fun () - sender 1); x + 1) e in let e'' = E.map (fun x - Queue.add q (fun () - sender 2); x + 1) e in does this code violate the semantics of events? Yes. It has the same problem. Let's start with : let e, sender = E.create () in let e' = E.map (fun x - Queue.add q (fun () - sender 1); x + 1) e in Since the thunk is delayed to be executed after the update cycle we *could* say that an occurence of [e] at time [t] defines the occurence of [e] at time [t + dt]. Note however that this is a bad idea, the right way to solve these problems is to use fixed point operators, see [1]. Now this is all fine, during the update cycle, which is made under a synchrony hypothesis (i.e. it takes no time, see [2]), we are defining the occurence of [e] at time [t + dt] as being 1. So far so good. But now we change the program and add let e, sender = E.create () in let e' = E.map (fun x - Queue.add q (fun () - sender 1); x + 1) e in let e'' = E.map (fun x - Queue.add q (fun () - sender 2); x + 1) e in This is not fine at all, during the update cycle, which again, takes no time, i.e. everything therein happens simultaneously at time [t], we are defining the occurence of [e] at time [t + dt] as being 1 and 2 at the same time. A schizophrenic event which obviously violates the semantics of events since an event must have at most one occurence at any given time [t]. So basically when you allow feedback from primitive events to primitive events you have to be very careful. Maybe that's needed in practice, again, I don't have enough experience to assert that, but if you do it you should make sure that the semantics of events is not violated. If so, PEC is also unsound. I'd like to know PEC is unsound or not. PEC may not be unsound as a whole. However the idea that you can just send to primitive events during update cycles and not bother is unsound with respect to the semantics of events as soon as you send two different values to the same primitive event. To prevent glitches, PEC distinct one update cycle to another by time identity. And calculated results are cached for same update cycle. Update order is straight forward. Just follow from leaf to primitive source event. It's not problem because only one primitive value changes at one update cycle. Right. But you still have to maintain some kind of mapping between the primitive event and the leaves they may influence to know which ones to update when the corresponding primitive event occurs. Do you store that in the primitive event itself or do you use a global data structure ? While I'm not very fond of the sub/unscribe part I think it's an interesting implementation and may try, once I get some time, to adapt it to React to see what we can get from it (I also think that the resulting implementation could be much simpler). One can in fact argue that using React you also have to do the same manual management by having to keep reference on leaf events to avoid them being gc'd. The difference is that PEC trusts the client to perform unsubscribes correctly to avoid leaks while React allows not to bother about that at all (but Weak pointers have their cost). Besides it may be the case that in practice sub/unsuscribe calls are not that plentyfull; I would count one subscribe and no unsubscribe in the breakout.ml example of React's distribution. Best, Daniel [1] http://erratique.ch/software/react/doc/React.E.html#VALfix [2] http://erratique.ch/software/react/doc/React#simultaneity -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] [ANN] PEC ver. 1.1
Le jeudi, 19 avril 2012 à 12:31, Daniel Bünzli a écrit : While I'm not very fond of the sub/unscribe part I think it's an interesting implementation and may try, once I get some time, to adapt it to React to see what we can get from it (I also think that the resulting implementation could be much simpler). In fact, if I really understood what you are doing, I think there is a performance problem with your approach. Suppose we have the following configuration where L is a subscribed leaf event, that depends on N events that eventually lead to the primitive events P1 ... PN : L | \ ... \ ° ° ° | \ ... \ ° ° ° | \ ... \ ... ...... |\\ P1 P2 ... PN If P1 occurs then you start walking back from L, but you don't know where P1 is so you have to walk down every branch until you find P1 and then walk back from there up to L to make the update. Contrast this with (weak) forward pointers: you just start from P1 and walk *once* up to L. Is that correct ? Best, Daniel -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] [ANN] PEC ver. 1.1
Thank you for helping me understand with your explanation. Your event semantics has two invariant. 1. for all e, t : occurrence of [e] at time [t] is one or zero. 2. if primitive [e] is occurred in time [t], update cycle runs in time [t]. Do you have any experience to proof a theorem against event combination term by using above axiom and event combinators semantics? I'm interested in this kind of reasoning. (2012/04/19 19:31), Daniel Bünzli wrote: Right. But you still have to maintain some kind of mapping between the primitive event and the leaves they may influence to know which ones to update when the corresponding primitive event occurs. Do you store that in the primitive event itself or do you use a global data structure ? Primitive events has list of leaves. Best Regards, Ogasawara -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] [ANN] PEC ver. 1.1
(2012/04/19 19:57), Daniel Bünzli wrote: Le jeudi, 19 avril 2012 à 12:31, Daniel Bünzli a écrit : If P1 occurs then you start walking back from L, but you don't know where P1 is so you have to walk down every branch until you find P1 and then walk back from there up to L to make the update. Contrast this with (weak) forward pointers: you just start from P1 and walk *once* up to L. Is that correct ? It's correct. But the performance can be optimized in future I think. When subscribing a event, we can collect and store information about tree structure. Present implementation discards these information. Best Regards, Ogasawara -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Kendall tau in OCaml
Hello, Is there some Kendall tau implementation out there in OCaml? I'm looking for something with better complexity than N^2, if that's possible, as I have a lot of points... Regards, F. -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Kendall tau in OCaml
I have a very efficient C implementation wrapped properly in OCaml here: https://github.com/alexy/katz/blob/master/kendall.ml A+ On Thu, Apr 19, 2012 at 7:51 PM, Francois Berenger beren...@riken.jp wrote: Hello, Is there some Kendall tau implementation out there in OCaml? I'm looking for something with better complexity than N^2, if that's possible, as I have a lot of points... Regards, F. -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
