Re: [TYPES] Questions regarding a clock inference system for data-flow languages

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Thanks a lot for your explanations Adrien,

> Date: Fri, 30 Aug 2013 18:01:42 +0200
> From: [email protected]
> To: [email protected]
> CC: [email protected]
> Subject: Re: [TYPES] Questions regarding a clock inference system for data-flow languages
>
> Hello Rajagopal and TYPES list,
>
> I am doing my PhD under the supervision of prof. M. Pouzet and A.
> Cohen, working on extended clock calculi for data-flow langages. I'll
> try to answer your questions to the best of my knowledge.
>
> From: Rajagopal Pankajakshan <[email protected]>
> To: "[email protected]" <[email protected]>
> Subject: [TYPES] Questions regarding a clock inference system for
> data-flow languages Date: Fri, 30 Aug 2013 07:15:24 +0000
> Sender: "Types-list" <[email protected]>
>
> > During my internship at google this summer I was assigned to study
> > type theory applied to stream-processing languages. One approach we
> > considered was that of the so called clock calculi, as found for
> > instance in Lucid-Synchrone [3].
>
> First, you may want to read "Clocks at First Class Abstract
> Types" (Colaço and Pouzet, EMSOFT'03), because the section dedicated to
> clock typing in EMSOFT'04 is indeed very terse. However, the full
> system as implemented in Lucid Synchrone has never been described
> anywhere, as far as I know.

I had a look at the suggested [EMSOFT'03] paper and there seems to be the same problem there in Figure 3.  Since a stream type s is also a clock cl you can use the (let) rule to generalise its type the same way, even thought the intended rule is (let-clock).
 
> > Lucid-synchrone defines a type inference system to analyse
> > synchronisation between data-flow streams. In this calculus, a stream
> > clock s can be the base execution clock, the sample of another clock
> > s on some condition (a name X or a variable n) or a variable α. The
> > paper claims that clock analysis can be performed using
> > Hindley-Milner type inference.
>
> It is indeed HM-like, but it needs to be extended with first-class
> abstract datatypes (restricted existential types) à la Laufer &
> Odersky. See EMSOFT'03 above for references.
>
> > The basic mechanism of type polymorphism is to universally quantify
> > the free clocks α1,...,αn and names X1,...,Xm of a definition in its
> > context H, here:
> >
> > gen(H, cl) = ∀α⃗.∀X⃗.cl where α⃗ = FV(cl) - FV(H) and X⃗ = FN(cl)
> > - FN(H)
> >
> > This allows to reuse that definition where it is used, by considering
> > an instantiation relation:
> >
> > cl[⃗s/α⃗][⃗c/X⃗] ≤ ∀α⃗.∀X⃗.cl
> >
> > My first question arises from the understanding that names X do not
> > seem to have the same status as variables α in this type system. They
> > are generalised and instantiated in the same manner. For instance,
> > consider the following Lucid program:
> > node flip (x) = x when yes where clock yes = true
> >
> > The boolean stream function flip samples all occurrence of x
> > according to a local stream yes. According to the type system [3,
> > figure 5], it has clock ∀α.∀X.α→α on X, as the following derivation
> > shows:
> >
> > |- true : s
> > _________________________________________________________________________
> > |- clock yes = true : (m:s)
> > _________________________________________________________________________
> > [yes : (m:s), x : s] |- x when yes : s on m
> > _________________________________________________________________________
> > [x : s] |- x when yes where clock yes = true : s on m (m not in
> > [x : s])
> > _________________________________________________________________________
> > |- node flip (x) = x when yes where clock yes = true : [flip : s->s
> > on m]
> >
> > Gen([],s->s on m) = ∀s∀m.s->s on m
>
> If I'm not mistaken, in your example m is a name, not a condition
> variable X. Thus it does not get generalized by Gen(). Indeed this
> program gets rejected by Lucid v3, as you note: a condition name may
> not escape its scope.

The m&ns are really arbitrary in this example, I presume the intended meaning would probably to use is with names, but the judgment equally holds with variables as it should, shouldn't it:

|- true : s
_________________________________________________________________________
|- clock yes = true : (X:s)
_________________________________________________________________________
[yes : (X:s), x : s] |- x when yes : s on X
_________________________________________________________________________
[x : s] |- x when yes where clock yes = true : s on X (X not in [x : s])
_________________________________________________________________________
|- node flip (x) = x when yes where clock yes = true : [flip : s->s on X]

Gen([],s->s on X) = ∀s∀X.s->s on X

> > The opposite stream function flop, below, can also be given type
> > ∀t∀n.t-> t on n.
> >
> > node flop (x) = let x when no where clock no = false : [flop :
> > ∀s∀n.t->y on n]
> >
> > Now, if we let H = [flip,:∀s∀m.s-> s on m,flop:∀t∀n.t-> t on n] then,
> > by rule (Inst) in [3, Figure 5], we can assign the same clock to of
> > flip and flop with the following type derivation
>
> > u -> u on o ≤ ∀s.∀m.s->s on m u -> u on o ≤ ∀t.∀n.t->t on n
> > ______________________________ ______________________________
> > H[x:s] |- flip : u -> u on o H[x:s] |- flop : u -> u on o
> > H[x:s] |- x : s
> > _______________________________________________________________________________
> > H[x:s] |- flip (x) : u on o H[x:s] |- flop (x) : u on o
> > ______________________________________________________________ H[x:s]
> > |- flip (x) + flop (x) : u on o
> > ______________________________________________________________ (1)
> > H |- node sum (x) = flip (x) & flop (x) : [sum : u-> u on o]
>
> > Doesn't function flipflop deadlock or does this mean that it needs a
> > buffer ?
>
> Indeed, from the pure data-flow point of view, this program either
> needs an infinite buffer on the left input of (&), or deadlocks if (&)
> is synchronous (i.e. has no buffers on its inputs and outputs).

Right, so the clocking rules fail to check the program synchronous from the (where) rule, in fact.

> > I tried to figure this out by testing the example with the
> > implementation of Lucid-Synchrone available on the web [2].
> > Actually, it behaves differently from what the paper says. For
> > instance, if we try to define function flip as above, the compiler
> > says:
> >
> > "This expression has clock 'c but is used with clock (__c1:'d)"
> >
> > It refuses to consider the assumption 'c as a sampled clock (__c1:'d)
> > generated by the when operator. Shouldn't it infer (__c1:'d) instead ?
> > However, if we add a clock declaration to do that:
> >
> > let node sample (x, clock y) = x when y
> > let node yes (x) = sample (x, true)
> > let node no (x) = sample (x, false)
> > let node yesandno (x) = yes x & no x
> >
> > then the compiler replies:
> >
> > # lucyc -i yesandno.ls
> > val sample : 'a * bool => 'a
> > val sample :: 'a * 'a -> 'a on ?_y0
> > val yes : 'a => 'a
> > val yes :: 'a -> 'a on ?_y0
> > val no : 'a => 'a
> > val no :: 'a -> 'a on ?_y0
> > val yesandno : bool => bool
> > val yesandno :: 'a -> 'a on ?_y0
> >
> > and produces a Caml program. But there are so many clocks in it that
> > I can't really figure out what it does.
>
> Strange, this code fails to compile on my machine with the same version
> of the compiler. The clock types that you get are clearly incorrect.
> This bug seems to be triggered by the "clock" keyword on inputs. If you
> remove it, you get a saner clock signatures and "yes" and "no" are
> rejected:
>
> val sample : 'a * clock => 'a
> val sample :: 'a * (__c0:'a) -> 'a on __c0
> val yes : 'a => 'a
> File "test.ls", line 2, characters 27-34:
> >let node yes (x) = sample (x, true)
> > ^^^^^^^
> This expression has clock 'b * 'c,
> but is used with clock 'b * (__c1:'b).

I just used the bytecode distribution available from your website: http://www.di.ens.fr/~pouzet/lucid-synchrone/lucid-synchrone-3.0b.byte.tar.gz (md5 87ffdb559ad882a0d92a1213466c2a3c).  It would be kind if you could update it.

> > Instead, I looked as the user manual [1] to
> > determine which of [2] or [3] to focus on. Concerning instantiation,
> > page 67, it says something different:
> >
> > "The clock (carrier-clock : stream-clock) of a stream e means that
> > e has value carrier-clock which has the stream clock stream-clock.
> > The value may be either a global value (defined at top-level) or an
> > identifier. This identifier is unique and is an abstraction of the
> > actual value of e."
> >
> > I don't understand how this uniqueness rule is specified in the paper
> > [3] and, more generally, how it relates to type polymorphism.
> > Doesn't it instead refer to existential quantification ? Also, in
> > which cases does it apply in the implementation ?
>
> You are right and I have a hard time figuring out from EMSOFT'04 too.
> It appears in a clearer form in EMSOFT'03, but I believe the final
> system of LSv3 is still quite a bit different.
>
> The basic idea is simple: you may not have an expression with a clock
> "'a on ?_c" if the condition ?_c is not present in the current scope.
> Thus, when clocking "e where D", one basically checks that the
> conditions "?_c_i" appearing in the clock type of "e" are still present
> in current environment.
>
> It may help to consider this property in relation with the code
> generation scheme. In the generated code, equations get translated to
> imperative statements, each one conditioned according to its clock type
> interpreted as a boolean formula. The current values of both clocks
> variables and conditions will thus have to be accessible from the
> current scope, at run-time.
>
> The compiler could automatically pass condition variables around, but
> it is a design choice that prof. Pouzet deliberately rejected.
>
> > In the end, I'm a bit confused and wonder whether polymorphism
> > matters at all. As long as one is not using streams of functions,
> > doesn't a simple sub-typing rule suffice (to handle a base clock and
> > samples "c on x") ?
>
> I am not sure to follow what you have in mind, but note that in Lucid
> Synchrone, a node do not have a single "base clock" in general. Please
> consider the following example, where f is parametric in two clock
> variables that get instantiated to two different clock types in g:
>
> # cat when.ls
> let node f x y = (0 fby x, 0 fby y)
> let node g x c = f x (x when c)
> # lucyc -i test.ls
> val f : int -> int => int * int
> val f :: 'a -> 'b -> 'a * 'b
> val g : int -> clock => int * int
> val g :: 'a -> (__c0:'a) -> 'a * 'a on __c0
>
> Also, and although experts on this list are far more knowledgeable than
> me on this matter, it seems to be common knowledge that type inference
> for HM-style parametric polymorphism is simpler (and thus easier to
> implement) and more scalable than (non-structural?) subtyping. An
> implementation of clock typing following the principles outlined above
> and using destructive unification takes less than a thousand lines of
> ML code and is very efficient.
>
> To conclude, you may be interested in the heavily simplified version of
> clock typing that appears in "Clock-Directed Modular Code Generation
> for Synchronous Data-Flow Languages" by Biernacki et al. (LCTES'08),
> even if it is restricted to the first-order setting. The paper may also
> serve as a nice introduction to the code generation machinery.

Thanks a lot for these detailed explanations, I will certainly look at the other LCTES'08 paper. 
 
> Hope that helps, do not hesitate to send me follow-up questions.

Sure, regards.

--- Raj

> -- Adrien Guatto
> http://www.di.ens.fr/~guatto/index_en.html