Another IO Task question

Stream: lean4

[Mac]

Is there a more efficient way to perform a (t : IO (Task a)) -> IO a conversion than t >>= IO.wait? As, unless I am mistaken, that spawns a thread and then has the main thread wait on it and is thus much less efficient than just executing the task in the main thread.

[Mario Carneiro]

isn't the existence of a Task a already committing to the task existing on its own thread?

[Mario Carneiro]

that is, Task a is the type of potentially already-started computations returning a value of type a

[Mario Carneiro]

if you want a task that has not yet been started you can use the type IO a instead of Task a. IO (IO a) -> IO a can be done without fork join

[Mac]

I am actually not sure about this. The docs for IO.asTask sounds like what you said could be possible. However, I would think that IO (Task a) would spawn a Task when the monad is unpacked (ex, via bind), not immediately. Having a Task a around outside a monad definitely does mean what you said, though.

[Mario Carneiro]

well, in an IO (Task a) we don't actually know if the task has been started or not. It might as well be pure t where t : Task a is currently running on another thread

[Mario Carneiro]

in any case, the only thing we can do with such a value is run it (on some thread) to get a Task a of unknown provenance

[Mac]

Mario Carneiro said:

well, in an IO (Task a) we don't actually know if the task has been started or not. It might as well be pure t where t : Task a is currently running on another thread

I am not sure how legal what you are saying is. As the IO (Task a) generated by pure t is a very different kind of task than the one generated by IO.asTask.

[Mario Carneiro]

That said, in the internals of Task one can presumably say what state the task is in and where it is running, so IO.wait can probably avoid the overhead if it sees the task is already complete

[Mario Carneiro]

Mac said:

Mario Carneiro said:

well, in an IO (Task a) we don't actually know if the task has been started or not. It might as well be pure t where t : Task a is currently running on another thread

I am not sure how legal what you are saying is. As the IO (Task a) generated by pure t is a very different kind of task than the one generated by IO.asTask.

That's true, but my point is they have the same type, so any function accepting one has to be prepared to deal with the other

[Mac]

true, but all these functions are constant so they aren't really listening to the type system. My point is that there could be an IO.join that inspects the task internals and notices it has yet to be started and instead just invokes the closure rather than spawning the task. (For already spawned tasks it just waits on them.)

[Mario Carneiro]

are you sure it isn't already doing that?

[Mac]

There isn't a function that I know of that could do this.

[Mario Carneiro]

I mean IO.wait could just do that

[Mac]

In IO.wait the object is a pure Task a so it is definitely already spawned.

[Mario Carneiro]

If Tasks are definitely already started, then I don't think there is any type that represents both not started and started tasks, so the type signature will determine already whether it needs to be on another thread or not

[Mac]

After looking at the internals, since an IO object is just a closure and invoking the closure starts the task. Since there is no way inspect into the closure / inform it to not spawn the task, I guess this is, in fact, impossible.

[Mario Carneiro]

right, a IO (Task a) is just a function that returns an already spawned task, there isn't any point to intercept it

[Mac]

:(

[Mario Carneiro]

What's the motivation? Why would you not know whether the task is started or not?

[Mac]

Mario Carneiro said:

right, a IO (Task a) is just a function that returns an already spawned task, there isn't any point to intercept it

Not that it does necessarily return an already spawned task. The function itself be the thing the spawns the task (as it is in IO.asTask's case).

[Mario Carneiro]

sure, but it can do that at any point in the function and you aren't instrumenting the code

[Mario Carneiro]

by the time the function returns, the task is started. Before the function is called, it may or may not be started (it doesn't even really exist as a thing yet)

[Mario Carneiro]

so this isn't a type that does what you want

[Mac]

Mario Carneiro said:

What's the motivation? Why would you not know whether the task is started or not?

In Lake, build tasks are IO actions that may be run asynchronously, thus I have to choose between representing them as IO a or IO (IOTask a).

[Mac]

The former is inefficient in the case of asynchronous tasks, the later is inefficient in the case of synchronous tasks.

[Mario Carneiro]

How about IO (IO a) then? The idea is you execute in the outer IO if you want it to run immediately and in the inner IO if you want to allow it to be scheduled flexibly

[Mario Carneiro]

this assumes that build tasks can decide for themselves which category they want to be in

[Mac]

How does that help?

[Mac]

More accurately, how are you proposing to represent them as IO (IO a)?

[Mario Carneiro]

I don't understand the question. Build tasks have that type, they return whatever type a is behind two layers of IO, and you use do ... pure (pure a) for sync actions and pure (do ... pure a) for async actions

[Mario Carneiro]

and then the harness runs all the outer IOs to get a List (IO a) or whatever the data structure is and puts them in a thread pool or what have you

[Mac]

Ah, this may be the key:

Mario Carneiro said:

this assumes that build tasks can decide for themselves which category they want to be in

Its exactly the opposite, the build manager is determining whether they are sync or async.

[Mario Carneiro]

Here the build manager gets to decide how to schedule the async parts, and the outer IO is for mandatory sync actions

[Mario Carneiro]

for a fully synchronous build manager you would just run both layers immediately

[Mario Carneiro]

and an async build manager could go through the list and call IO.asTask on each one to get a list of tasks

[Mario Carneiro]

or do that up to numThreads times and manage the parallelism

[Mac]

I honestly am very confused about what you are describing.

[Mac]

Currently, each build target has some task IO PUnit that builds the artifact. I can make this asynchronous by running IO.asTask to get an IO (IOTask PUnit) or I can just run this synchronously by using the monad itself. I fail to see how this can be usefully made into an IO (IO PUnit) action.

[Mario Carneiro]

That corresponds to the inner IO in my version. The outer IO is for things that have to be run on load time; if this is not necessary then IO Unit should suffice

[Mac]

However, I will note that your suggestion of using m (m a) (ex. IO (IO a))) for asynchronous actions is what Haskell does, so if there was an efficient way of mirroring that in Lean, I would be all ears.

[Mac]

Mario Carneiro said:

That corresponds to the inner IO in my version. The outer IO is for things that have to be run on load time; if this is not necessary then IO Unit should suffice

So how is that different from what I am doing?

[Mario Carneiro]

def buildTask1 : IO (IO Unit) := do
  println! "I always run immediately"
  pure do
    println! "I run when this task is scheduled"

def buildTask2 : IO (IO Unit) := pure (pure ())


def buildManager : IO Unit := do
  -- run sync actions
  let ios : List (IO Unit) ← [buildTask1, buildTask2].mapM id
  -- split off the first task, because we want to run it on the main thread
  let io1 :: ios ← ios | panic! ""
  -- start async actions in parallel
  let tasks ← ios.mapM IO.asTask
  -- Run the first task on the main thread
  let result1 ← io1
  -- block on the async tasks
  let results ← tasks.mapM IO.wait
  -- do something with results

[Mac]

Again, in Lake there is no 'I always run immediately', there is only 'I run when the task is scheduled' in build tasks.

[Mac]

which just reduces this example to what I already have.

[Mario Carneiro]

Without the outer IO, the only difference is that the first line is just let ios : List (IO Unit) := [buildTask1, buildTask2]

[Mario Carneiro]

you still have flexibility in when to schedule things

[Mario Carneiro]

I'm not sure how you want to determine what to run where though

[Mac]

The problem is that a build task A may or may not wish to build other things and it may want to do so asynchronously. If it does, it is now left with a IOTask instead of an IO, so it has to wait on it to covert into an IO. However, a build task B may then choose to to ran A asynchronously as well, which means I end up be with a dead thread (as it reduces to essentially `IO.asTask (IO.wait t)).

[Mario Carneiro]

Do you want task B to call task A directly, or ask the build manager to do it?

[Mac]

task B calls A directly (in the current implementation)

[Mario Carneiro]

So is the asynchrony because task B has something else to do while A runs?

[Mac]

yes, task A or B may depending on 10 different tasks, so it wants to build them all asynchronously.

[Mario Carneiro]

because if it's just creating the task and waiting on it immediately then that's obviously useless

[Mario Carneiro]

okay, so it can just do that then, right? It just starts all the tasks, and waits on all the results

[Mac]

Yes, but A already does that, so B is now waiting on A's thread which is waiting on its own dependency's threads.

[Mario Carneiro]

shouldn't B be waiting on A?

[Mac]

yep, typo -- fixed.

[Mario Carneiro]

okay so where's the problem? If B wants to run A on its own thread it can do so

[Mac]

But that's the problem since A is a collection of asynchronous tasks, spawning it on new thread is silly.

[Mario Carneiro]

So then B can not run it async

[Mac]

And therein lies the problem, how is B to know which to do?

[Mario Carneiro]

how is anything to know which to do?

[Mac]

Exactly, hence my problem.

[Mario Carneiro]

what's the ideal decision procedure here

[Mario Carneiro]

it's certainly harder from B's myopic point of view, but even from a global view I'm not sure what you want to do about it

[Mac]

What B would like to do is, if A is a collection of async tasks, add them to the async queue. Otherwise, run it as a new thread (and add it to the queue).

[Mario Carneiro]

if you want to be able to make global decisions here, though, you should probably have B not call A directly and use the build manager as middle man

[Mac]

I don't really want a global decision here. This mostly a decision on the intersection point.

[Mario Carneiro]

Can A have some metadata saying "I am a collection of async tasks"? Then the library can provide a function which is "run async if this is a sync action, and run sync if this is a collection of async actions"

[Mario Carneiro]

you can make the setting of that flag less error prone by having a special constructor for "aggregate tasks"

[Mac]

Yeah, I was probably being a little to narrow minded. I could just use a new monad that is either an IO or an IO (IOTask a). I was just trying to get away with just using IO.

[Mario Carneiro]

well, in my version it's still just an IO a, or rather (IO a) x Bool

[Mario Carneiro]

I don't think IO (IOTask a) is helpful, that's for already started tasks so it is more appropriate as the return type of library functions

[Mac]

IO (IOTask a) is an IOTask spawner -- it is not for already started tasks.

[Mac]

Though you can of course inject an already existing task with pure.

[Mario Carneiro]

well yes, but when would a build task ever want to have a type like that?

[Mario Carneiro]

when it can just return the result

[Mario Carneiro]

unless you are interested in the inner/outer IO approach from before

[Mac]

If the task is just a collection of asynchronous tasks (or a collection + a post-completion action)?

[Mac]

I should probably be using IO Unit/IOTask PUnit more to make it clearer that a is not a result in this system.

[Mario Carneiro]

A collection of asynchronous tasks could have type List (IO a), i.e. literally a collection

[Mario Carneiro]

I was wondering about that; this is a lot harder if you want to be type parametric

[Mario Carneiro]

so the monad might be Sum (IO a) (List (IO a))

[Mario Carneiro]

well, there are some decisions to be made about when a task becomes a collection and vice versa

[Mac]

Mario Carneiro said:

A collection of asynchronous tasks could have type List (IO a), i.e. literally a collection

I assume you mean Array (IOTask a). That is fine if it just a collection. However, if it is a collection and then an action, then it is not.

[Mario Carneiro]

not IOTask, IO

[Mac]

That would be a collection of synchronous actions, not asynchronous tasks.

[Mario Carneiro]

It is a collection of not-yet-started tasks

[Mario Carneiro]

you use IO.asTask to start them

[Mac]

In this case they are already started though.

[Mario Carneiro]

The advantage of waiting to start the tasks until you have the complete collection is that you get more parallelism

[Mac]

A build target A often comes with the a list of additional targets Bs as dependencies. Each as a task field that, when run, will materialize the target. The build target A's task will run these tasks and (after they are finished) perform its own build.

[Mac]

Mario Carneiro said:

The advantage of waiting to start the tasks until you have the complete collection is that you get more parallelism

You often can't do this because the task itself might determine which tasks to run.

[Mac]

In building a Lean module, for example, we learn which tasks to run by reading the imports and we only want to run the task once for the same import. Thus we determine which module tasks are built while building.

[Mario Carneiro]

With the Sum (IO Unit) (List (IO Unit))monad, there are two ways to implement A.task. If it has a lot of additional work to do, then it chooses the first variant: it has to implement an IO Unit, which runs runMany Bs for the list of tasks Bs, gets the results, and does what it needs to do. If it has nothing to do besides aggregating the Bs, then it calls collect Bs which produces the List (IO Unit) variant by concatenating all the subtasks in the Bs

[Mac]

The most common cases for build tasks, imo, are the following:

• Do nothing, the file is an input
• Build something (ideally synchronously) and then perform an action (ex. building a .o file)
• Build many things (ideally asynchronously) and then perform an action (ex. building a static/shared library)
• Do something heavily complex (i.e., intermingle building and determining which things to build)

[Mario Carneiro]

In all of those examples, you already know whether you are async or sync

[Mario Carneiro]

and IO Unit already handles those cases

[Mac]

Yes the task itself knows whether it wants to be synchronous or asynchronous. However, it does not know whether its dependents do.

[Mario Carneiro]

it knows whether it wants to run its direct children on the same thread or not

[Mac]

Yes, but it doesn't know whether its direct children are run on the same thread or not.

[Mac]

Options 1 and 2 are synchronous build tasks, options 3 and 4 are asynchronous tasks.

[Mario Carneiro]

if it is responsible for starting the children then it can do so

[Mac]

It is only necessarily responsible for finishing its dependents, not starting them.

[Mario Carneiro]

def doNothing : IO Unit := pure ()

def buildSyncThen (a b : IO Unit) : IO Unit := a *> b

def buildAsyncThen (as : List (IO Unit)) (b : IO Unit) : IO Unit := do
  let as ← as.mapM IO.asTask
  let _ ← as.mapM IO.wait
  b

def doSomethingElse (f : IO (List (IO Unit))) : IO Unit := do
  let as ← f
  buildAsyncThen as ()

[Mac]

Your buildAsyncThen is very inefficient if spawned asynchronously. It spawns a thread that does nothing but wait until it is dependents are finished.

[Mario Carneiro]

That's what the collection thing was about

[Mario Carneiro]

if you keep metadata on the tasks to be able to say which ones are "heavy" and which are "light" then you can avoid spawning threads for light tasks

[Mario Carneiro]

if b is heavy then buildAsyncThen might not be so useless

[Mac]

It still is, because before it does b it is just a thread that is sitting around doing nothing.

[Mario Carneiro]

really, I think you need a green threads implementation

[Mario Carneiro]

In fact, isn't Task doing that already?

[Mario Carneiro]

I'm not sure that these are actually system threads

[Mac]

For example, consider: buildAsyncThen [buildAsyncThen [...] a1, ...., buildAsyncThen [...] a10] b. The outer buildAsyncThen spawns 10 threads that wait for the inner tasks to complete and if those tasks are complex they may be sitting around for a while eating up the thread pool doing nothing.

[Mario Carneiro]

In that case you might want something like this:

structure BuildTask where
  deps : Array (IO Unit)
  main : IO Unit

then buildAsyncThen is a combinator that combines the deps

[Mac]

These are the reasons IO.mapTask/IO.mapTasks/IO.bindTask exist, specifically to avoid creating such threads.

[Mac]

See Sebastian's comment on my previous IO Task question: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20IO.20Tasks/near/248579994

[Mac]

Also see Wojciech's comment below that where he explains that consuming the thread pool can actually lead to deadlock (and no tasks completing).

[Mac]

Thus, things that lead to IO.asTask (IO.wait task *> something) have to be avoid like the plague.

[Mac]

Mario Carneiro said:

In that case you might want something like this:

structure BuildTask where
  deps : Array (IO Unit)
  main : IO Unit

then buildAsyncThen is a combinator that combines the deps

This can't be done for the reason I already described. There are build tasks that don't know their dependencies until main is run.

[Mario Carneiro]

It would be great if there was a version of IO.asTask that yielded a TaskBuilder which you can use to construct a dependency graph with map/bind before starting it

[Mario Carneiro]

Mac said:

This can't be done for the reason I already described. There are build tasks that don't know their dependencies until main is run.

For tasks like that you would just have empty deps

[Mario Carneiro]

they would just start their deps directly inside main

[Mario Carneiro]

the deps represent dependencies known in advance, which can be used to aggregate the leaves in your nested buildAsyncThen example

[Mac]

So then what is the point of the deps then?

[Mario Carneiro]

for dependencies that need to be computed first, there is nothing for it but to run the action and tie up a thread

[Mac]

Sorry, I wrote that before I read your last response.

[Mac]

The problem with the Lean build system is that all the simple tasks depend on the big complex task that can't be represented as an IO.

[Mario Carneiro]

what can't be represented as IO?

[Mac]

The package build.

[Mario Carneiro]

why?

[Mac]

Building o files, the static lib, and the exe are simple tasks but they don't know what files to build until the package build has been computed and launched.

[Mac]

The package build returns a NameMap of modules to their associated active build target / task which the rest (i.e., the o files, static lib, and exe) use to know what to build and what to depend on.

[Gabriel Ebner]

Mac said:

My point is that there could be an IO.join that inspects the task internals and notices it has yet to be started and instead just invokes the closure rather than spawning the task. (For already spawned tasks it just waits on them.)

I didn't read the whole thread, but I just wanted to say this proposal here is a terrible idea because it executes the task with a nondeterministic (and potentially very small) stack size.