How do tasks map to parallelism?

Stream: lean4

[Henrik Böving]

I have this piece of code on todays nightly:

def fib (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

def main : IO Unit := do
  let tasks ← List.range 8 |>.mapM fun i =>
    IO.asTask do
      IO.println s!"{fib (35 + i)}"
  for t in tasks do
    let _ ← IO.wait t

to try and get Lean to compute all of the fib numbers in parallel. However when I execute it and check my htop I see that Lean is going completely single core here. I thought that Tasks are our unit of parallelism but that doesn't seem to be happening here? What am I doing wrong?

[Henrik Böving]

Interesting. If I just spawn a ton of additional tasks I can see all of them in my htop, now I'm even more confused as to why these tasks where each of them is clearly taking a bit of time to compute do seemingly not show up there /o\

[Mario Carneiro]

what is the definition of fib?

[Mario Carneiro]

(I would hope that an actual computation of fib 35 is not so slow as to be good for benchmarking!)

[Mario Carneiro]

are you running this in the interpreter or compiled?

[Henrik Böving]

Edited. I am running compiled and the computation does take roughly 8 seconds overall and reports a cpu load of 99%.

[Mario Carneiro]

Looking at the C code, it appears the fib computation has been lifted out of the IO.asTask

[Henrik Böving]

Gaaaah

[Henrik Böving]

And I thought I had outsmarted the compiler by using a variable...

[Mario Carneiro]

actually, looking at the lean code this isn't even the compiler getting smart, there really isn't anything forcing the computation to be delayed

[Mario Carneiro]

because do x just macro expands to x

[Mario Carneiro]

meaning the code is essentially IO.asTask (IO.println (fib (35 + i)))

[Mario Carneiro]

which of course evaluates fib before constructing the task

[Henrik Böving]

Ah that also explains why it started working when I switched over to Task.spawn instead....

[Henrik Böving]

do we have an API that ...does not do this? For IO tasks that is

[Mario Carneiro]

if you do something like do pure (); IO.println s!"{fib (35 + i)}" it will probably work

[Mario Carneiro]

just anything to wrap a thunk around the computation

[Henrik Böving]

yeah that works...

[Henrik Böving]

Well thank you^^ But we should certianly fix this

[Mario Carneiro]

A version of asTask that takes Unit -> IO A would presumably work

[Henrik Böving]

I mean is it even reasonable to have asTask if it has this footgun? Why not just refactor generally?

[Mario Carneiro]

I wouldn't put the blame on asTask, this is true for anything that takes an argument of type IO A

[Mario Carneiro]

it's certainly a bit frustrating since IO is already a thunk type

[Mario Carneiro]

but when you write an expression which evaluates to a function type, how do you know whether it should be eta-expanded or not? I don't see how the do notation could do this correctly either

[Henrik Böving]

Right, by "refactoring in general" I didn't mean changing the IO behavior in general, I was more thinking about changing the type of IO.asTask. I believe this to be reasonable because the usual floating computations around behavior in a single threaded context is fine right. It should be about the same speed (modulo cache) and do the same interactions with the environment and produce the same result. But in an IO.asTask context lifting things out of the argument does actually (as we can see) potentially drastically impact what is going to happen.

[Mario Carneiro]

like I said, the same issue happens for any function which takes an argument of type IO A

[Mario Carneiro]

because if you have such an argument you presumably are interested in not running it yet

[Mario Carneiro]

so running the first part of it is probably wrong

[Mario Carneiro]

...except when you do want to precalculate part of it, and there are issues in the other direction too

[Sebastian Ullrich]

For many of these lifting pure computations over them does not matter. Changing the signature of asTask does not sound too far-fetched to me

[Yury G. Kudryashov]

BTW, what Lean does(not) calculate at compile time? AFAIR, Haskell inlines a lot.

[Sebastian Ullrich]

Inlining itself should not change when something is computed, except by enabling other optimizations

[Sebastian Ullrich]

In theory, do could insert a call of

def defer [Monad m] (f : Unit → m α) : m α :=
  pure () >>= f

but that's not as clear-cut in a language where one might actually want to look at the resulting term

[Mario Carneiro]

here's a trick that seems to work without changing the type signature of asTask:

@[macro_inline] def IO.asTask' (m : IO A) : BaseIO (Task (Except Error A)) :=
  IO.asTask fun w => m w

def main : IO Unit := do
  let tasks ← List.range 8 |>.mapM fun i =>
    IO.asTask' do
      IO.println s!"{fib (35 + i)}"
  for t in tasks do
    let _ ← IO.wait t