Using Task to parallelize recursive function

Stream: lean4

[Thomas Vigouroux]

Hey there.

I have a recursive function that follows the structure of a tree in a DFS manner.

I'd like to make that parallel, while keeping a proof of its correctness (which I already have, so if the changes are somewhat minimal, I'll take it).

Is it possible to use Task.spawn on the recursive call to make it parallel or would I need to make a custom task list setup?

[Thomas Vigouroux]

I tried something but it seems I that I am getting a deadlock for some reason

[Sebastian Ullrich]

Are you blocking on tasks? You should only do that once on the top level of your function

[Thomas Vigouroux]

Thanks for the advice ! I ended up writing something along the lines of

def myFn (T: Tree): Result :=
  let rec loop (T: Tree): Task Result := ...
  loop T |>.get

And that worked !

[Thomas Vigouroux]

Related to that: in my implementation I have a parameter to set the "depth" at which I split into multiple tasks.

Unfortunately, the complexity of the subtasks in each branch is not uniform, so at some point I have only one task remanining for a very long time, which could probably be broken into subtasks.

Would it be possible to have a function of Task, like Task.has_inactive_core, that evaluates to true if there are inactive cores and false otherwise ?

[Thomas Vigouroux]

Something along the lines of

opaque Task.inactiveCores : Unit -> Bool

[Daniel Weber]

That function wouldn't be pure, so I think it has to be unsafe

[Thomas Vigouroux]

It would be a problem for me because it would require marking the enclosing function unsafe too, which prevents me from proving anything about it

[Daniel Weber]

Perhaps something like docs#withPtrAddr could be done, then, although I'm not sure

[Thomas Vigouroux]

That's what I thought too
Another thing I am thinking about is making bindings into openmp and adding a bunch of lemmas about the correctness of openmp