-
Notifications
You must be signed in to change notification settings - Fork 21
Conversation
It may be wise to leave this unmerged until Mirage 3 is safely released. |
Just so that I can get a quick look before reinstalling half my mirage switch: Could you pastebin before/after for some medium-sized unikernel ? |
Ok, Change 2 is incorrect because it doesn't launch the sub-connect concurrently, it makes them sequential. Here is the original version. First, all the tasks are forced, which make them execute concurrently, then they are lwt-bound. let f11 = lazy (
let __time1 = Lazy.force time1 in
let __pclock1 = Lazy.force pclock1 in
let __mclock1 = Lazy.force mclock1 in
__time1 >>= fun _time1 ->
__pclock1 >>= fun _pclock1 ->
__mclock1 >>= fun _mclock1 ->
Unikernel1.start _time1 _pclock1 _mclock1
) Here is the new version, the tasks are forced and lwt-bound immediately, in a sequential order. let f11 = lazy ( Lazy.force pclock1 >>= fun _pclock1 ->
Lazy.force mclock1 >>= fun _mclock1 ->
Unikernel1.start () _pclock1 _mclock1) |
(To see why this is important more concretely: consider the case where you have two main devices that both launch servers listening on different ports. The "main" Mirage device will connect on both. It must do so concurrently) |
Thanks for taking a look at this, @Drup. Could you be even more concrete? e.g. with a pointer to some code. The code that |
@yallop |
It's ok; I see what you mean. I'll take another look at combining forcing and binding. |
Having looked at this a bit more, I think an applicative approach could work well here. We could generate something like this pure Unikernel1.start <$> lazy () <$> pclock1 <$> mclock1 in place of the current let f11 = lazy (
let __time1 = Lazy.force time1 in
let __pclock1 = Lazy.force pclock1 in
let __mclock1 = Lazy.force mclock1 in
__time1 >>= fun _time1 ->
__pclock1 >>= fun _pclock1 ->
__mclock1 >>= fun _mclock1 ->
Unikernel1.start _time1 _pclock1 _mclock1
) With some care it should be possible to arrange to run the applicative so that all the laziness is forced before blocking. |
@yallop I agree. The code is made to precisely emulate the applicative behavior. :) Currently, functoria asks for the dsl to provide monad-like operator, but that monad doesn't include the lazyness aspect. I guess we could touch that a bit ? |
That would be lovely alongside the other code like the cmdliner exposure which has similar idioms. |
@Drup: is there a reason why the "main" code forces values sequentially? Is it important to preserve that behaviour? |
@yallop I think that is the list of special init tasks. The sequence seems to be:
|
Thanks, @talex5. Do you think it would be worth making the dependencies explicit in the data flow? i.e. returning a value from each task that can be used as input to subsequent tasks? |
I originally made a PR in which init tasks were just normal jobs with dependencies, but it was felt that this list-based system was simpler and good enough. |
The problem with making that part of the data flow explicit is that suddenly, everyone must depend on the key device. People must remember to declare dependency towards the key device (and, spoiler, they won't). The graph becomes mostly unreadable and you get some other annoying issues, and we don't even really gain anything. From an abstract point of view, I would really like it, it would be much more elegant. Currently, there is an ugly hack to find back the key device in the graph and do the init properly. It's a very practical approach. If you have a concrete proposition that doesn't make everything else worse, I'm all hear. |
Thanks, @Drup. That all makes sense. Surfacing the dependencies is valuable, but I can see how it could lead to a tangle. I'll give it some thought. In the meantime, I'll pull some of the less controversial changes here into a separate pull request. |
Here's an outline of a possible approach that leaves the device code ignorant of laziness. The idea is to use an explicit representation of the forced computation to ensure that all forcing of lazy values occurs before all use of First, the code for each device is a closed function expression: (fun x y z ->
Foo.connect x y z) A function, val lift : 'a -> 'a t Lazy.t A second function, val ( <$> ) : ('a -> 'b) t Lazy.t -> 'a Lwt.t Lazy.t -> 'b t Lazy.t Finally, val run : 'a Lwt.t t Lazy.t -> 'a And here's a simple implementation: type _ t =
V : 'a -> 'a t
| App : ('a -> 'b) t * 'a Lwt.t -> 'b t
let lift v = lazy (V v)
let rec run' : 'b 'c. 'b t -> ('b -> 'c Lwt.t) -> 'c Lwt.t =
fun e k -> match e with
| V v -> k v
| App (f, v) -> run' f (fun g -> v >>= fun w -> k (g w))
let run v = Lwt_main.run (run' (Lazy.force v) (fun x -> x))
let (<$>) f x = lazy (App (Lazy.force f, Lazy.force x)) You might then write code like this: let p = lazy (P.connect ())
let m = lazy (M.connect ())
let d = run (lift connect <$> p <$> m <$> m) The tricky part is ensuring that the thunks are forced before any binding takes place. Representing the computation using What do you think, @Drup? |
ping @Drup |
Sorry for the delay! @yallop I believe this is a good idea! Your API looks good. I wonder how generic we can make it. |
This one seems relevant to resurrect again :-) |
Indeed! |
6bb36f9
to
d812364
Compare
sorry for being late to the party, but I'm wondering what the status of this PR is? it looks like this would be a good improvement for functoria. AFAICT @yallop most recent suggestion from #104 (comment) to use an explicit representation of the forced computation is not yet implemented -- @yallop any chance you have some time to develop this code and rebase this PR on master? I can rebase the accompanied PR in mirage if you like. |
Actually, the last set of patches implement the idea of separating values and computations. The code looks decent at a glance, but it breaks everything single device in existence. :/ |
@Drup I searched through GitHub for mentions of |
d812364
to
cadcf00
Compare
I've rebased against |
thanks @yallop, if you get around doing that, that'd be great. as mentioned earlier, I'm happy to rebase your mirage/mirage#790 PR once this is settled :D |
It would be nice to merge that PR at one point, as simpler code is always nicer :-) @yallop do you think you could update these patches to make it inline with the above discussion? |
The functoria codebase has changed a little bit, but this is still a very much wanted code generator simplification. @yallop if you are still interested to implement these changes, I'll be super happy to merge them :-) |
Actually this repository is not active anymore, so please feel free to move your patch to mirage/mirage ! |
This PR makes a few changes to the code generated by functoria to make it smaller and simpler. The aims are readability and simplicity, not performance, but there might be some small performance improvements.
The typical space savings are around 40-45%. For example,
main.ml
file forconduit_server
drops from 199 lines to 115 linesmain.ml
file forconsole
drops from 80 lines to 43 linesThe code is simplified/shrunk in three main ways:
First, there's a distinction between between effectful and non-effectful initialization code in the return type of
connect
. (This is perhaps a first step in the direction of generating code at a slightly higher level than string concatenation.)The implementer of
connect
tags the generated code withVal
orEff
according to whether it's a simple value or a possibly-effectful computation, and the caller ofconnect
uses the tag to determine whether the value can be safely inlined. For effectful computations the generated code follows the previous scheme: a top-level binding is emittedwhich is used in
connect
code for other modules:For effect-free computations the top-level binding is omitted and the value is instead inlined directly:
Second, the code that forces lazy values and the code that executes the resulting
Lwt
computations are combined, avoiding an intermediate binding. Before:After:
(This changes evaluation order slightly, so it would be a good idea for someone to confirm that the change is safe.)
Finally, the layout is now a little more compact. For example, short expressions now occupy a single line. Before:
After: