Deadlock with Tasks

Stream: lean4

[Thomas Vigouroux]

Hey there,

I've been using tasks for a while now, and i recently updated to 4.14

It seems that this introduces a reproducible deadlock in my code.

Is there something that changed recently-ish?

[Thomas Vigouroux]

Wait actually, the deadlock seems to happen in earlier versions of lean, so I am definitely doing something wrong here

What are the does/don't about Tasks ?

[Sebastian Ullrich]

Do avoid Task.get in non-dedicated tasks as having all tasks in the thread pool wait on it will lead to deadlocks

[Thomas Vigouroux]

Hmm so from what I can see I only call it once...

[Thomas Vigouroux]

The code is here by the way: https://git.sr.ht/~vigoux/busybeaver/tree/733fdfcef00587f38e16e2c161d500516bf629a0/item/Busybeaver/Enumerate/Impl.lean

[Thomas Vigouroux]

The idea is that the BBComputeP functions does some kind of parallel fold operation on a tree

[Thomas Vigouroux]

Does List.waitAll count as a Task.get?

[Sebastian Ullrich]

If you look at the stack traces in a debugger, it should tell you where they are stuck

[Thomas Vigouroux]

Can you display stakes for multiple thread though?

[Henrik Böving]

You can either switch to another thread and do a backtrace:

th 3
bt

or show all:

th apply all bt

[Thomas Vigouroux]

'Kay, I'll have a look then

From what I've seen, there remains 4 threads running and doing nothing but using each one core

[Thomas Vigouroux]

Which surprises me actually, is there some kind of spin loop?