IO Tasks

Stream: lean4

[Mac]

I use Task and IO.asTask heavily in Lake for parallel building, but there are some details to the implementation I am not sure I understand properly, so I am hoping to clarify them here:

• What is the difference between IO.wait task and task.get?
• What is the difference between IO.mapTask f task and IO.asTask do IO.wait task; act?
• Similarly, What is the difference between IO.mapTasks f tasks and IO.asTask do let xs ← tasks.mapM IO.wait; f xs?

[Sebastian Ullrich]

What is the difference between IO.wait task and task.get?

The former is a side effect, so it will always be executed even if the return value is not acutally used.

What is the difference between IO.mapTask f task and IO.asTask do IO.wait task; act?

The former doesn't uselessly block a thread

Similarly, What is the difference between IO.mapTasks f tasks and IO.asTask do let xs ← tasks.mapM IO.wait; f xs?

ditto

[Wojciech Nawrocki]

To expand on the latter two answers a bit, the thread pool needs to know the dependency graph between tasks in order to schedule them correctly. Using IO.wait does not register a dependency and will result in a deadlock when there are few threads in the pool and a task gets scheduled before its dependency. So within tasks, you should always use mapTask (wait is okay on the main thread).

[Gabriel Ebner]

IO.wait does not register a dependency and will result in a deadlock when there are few threads in the pool

Lean 3 used to spawn a new thread in this case, does Lean 4 no longer do this?

[Sebastian Ullrich]

It doesn't. That does mean that you need to be mindful of not blocking the pool for too long (or even deadlocking it), and use Task.Priority.dedicated otherwise. I'm not sure if the Lean 3 approach was more sensible, it sure sounds like a recipe for tanking performance. It looks like professional implementation of growing thread pools (most of Rust's seem to be fixed?) are at least very careful about injecting new threads.

[Notification Bot]

Mac has marked this topic as unresolved.

[Mac]

Another question in regards to IO Tasks: is IO.mapTask f task significantly more efficient than IO.bindTask task (pure <$> f) or is it just more convenient?

[Mac]

The particular case I am most curious about is IO.mapTask (do ...; pure x) task vs IO.bindTask task do ...; pure <| pure x.

[Sebastian Ullrich]

It is more efficient, but probably not significantly