Zulip Chat Archive

Stream: lean4

Topic: Nondeterministic number of threads created

Thomas Murrills (Apr 14 2025 at 04:17):

Is this expected behavior? When running the following under lean --run <filename> on nightly (and earlier, e.g. 4.17.0), I sometimes get 7 total threads, sometimes 12, sometimes 5...

def foo (x : Nat) : IO Unit := do
  IO.println s!"Starting task {x}…"
  IO.sleep ((x.toUInt32 + 1) * 30000)
  IO.println s!"Finishing task {x}…"

def main : IO Unit := do
  for n in [:10] do
    let _ ← (foo n).asTask
  IO.println "Done main!"

When it starts with a certain number of threads, that number never increases; it will wait until a task is done to start the next.

Example output for e.g. 7 total threads (2 basic threads, plus one for each running task, I suppose) is

Output

Thomas Murrills (Apr 14 2025 at 04:21):

I'll also note that using e.g. lean --threads=10 --run <filename> produces the same nondeterministic behavior, which seems strange to me.

Thomas Murrills (Apr 14 2025 at 04:36):

Also (perhaps more importantly): I hit a segfault when trying .asTask (prio := .dedicated) here without supplying --threads=10; and when I do supply --threads=10, I see Starting task n... in the terminal but not Finished task n....

The latter might just be me not having the right expectations, but I hope segfaults during innocent attempts at thread management aren't intentional! :sweat_smile:

Thomas Murrills (Apr 14 2025 at 04:38):

(Sometimes using prio := .dedicated without a --threads argument is a segfault immediately after Done main!, but sometimes it's this:

error

and sometimes the output is simply

Done main!
Starting task 0…

(or just Done main!) with no apparent error.)

Thomas Murrills (Apr 14 2025 at 04:50):

I suppose this might be two (or more) separate issues discovered while attempting to reach the same goal (namely, consistently create 10 concurrent task threads), so apologies if it turns out they don't share the same root cause! :)

Sebastian Ullrich (Apr 14 2025 at 07:54):

This might be a corner case at the end of main so try waiting for the tasks

Thomas Murrills (Apr 15 2025 at 00:55):

To update this topic, the segfault and error messages with (prio := dedicated) were indeed caused by main not waiting for dedicated tasks by default, and this has now been changed in lean4#7958 thanks to quick work by @Henrik Böving :)

Thomas Murrills (Apr 15 2025 at 00:58):

The only remaining issues in this topic are now

  1. the number of threads in the thread pool appears to be nondeterministic, and not as large as it could/should be
  2. using --threads does not change that behavior

Sebastian Ullrich (Apr 15 2025 at 06:36):

I believe that, too, will be resolved if you wait for your tasks!

Thomas Murrills (Apr 15 2025 at 07:32):

To be clear I do mean when not using prio := .dedicated, which was an attempt to work around the thread nondeterminism issue! :) (Waiting does indeed resolve the issue when using prio := .dedicated.)

Thomas Murrills (Apr 15 2025 at 07:33):

Just to cover all bases, though, waiting does not seem to resolve issues 1 and 2 (assuming I haven't done anything wrong):

def foo (x : Nat) : IO Unit := do
  IO.println s!"Starting task {x}…"
  IO.sleep ((x.toUInt32 + 1) * 3000)
  IO.println s!"Finishing task {x}…"

def main : IO Unit := do
  let mut tasks := Array.mkEmpty 10
  for n in [:10] do
    tasks := tasks.push <|← (foo n).asTask
  IO.println "Started all tasks."
  for task in tasks do
    let _ ← IO.wait task
  IO.println "Done main!"

The following run used --threads=10 but had 7 total threads (note that task 5 doesn't start until another task ends).

Output

Last updated: May 02 2025 at 03:31 UTC