Async concurrently has confusing behavior in case of errors

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When executing Async.concurrently actions that raise IO errors, the correctness of program side-effects seems to depend on the order in which actions are passed to Async.concurrently. This may be specific to sleep effects.

Context

I was working on my own small programs to explore Lean's async functionality.

Steps to Reproduce

Run the following program with Lake (e.g. lake exe program):

import Std.Async
import Std.Time

open Std.Async (Async sleep)
open Std.Time

public def sleepAndPrint (sleepDurationSeconds : Nat) : Async Unit := do
  sleep (Millisecond.Offset.ofSeconds (Second.Offset.ofNat sleepDurationSeconds))
  IO.println s!"Called sleep for {sleepDurationSeconds} seconds"

public def sleepAndPrintError (sleepDurationSeconds : Nat) : Async Unit := do
  sleepAndPrint sleepDurationSeconds
  IO.println s!"Raising error after {sleepDurationSeconds} seconds sleep call"
  throw (IO.userError s!"Error after {sleepDurationSeconds} seconds sleep call")

public def blockAndPrint (action: Async Unit) : IO Unit := do
  try
    Async.block action
  catch e =>
    IO.println s!"Caught error: {e}"

def main : IO Unit := do
  IO.println "Short-circuiting sleep operations on errors"

  let action1 := sleepAndPrint 1
  let action2 := sleepAndPrint 2
  let action3 := sleepAndPrint 3

  let action1Error := sleepAndPrintError 1
  let action2Error := sleepAndPrintError 2

  IO.println "\nError first, shorter sleep first"
  blockAndPrint (do
    let _ ← (Async.concurrently action1Error action2)
  )

  IO.println "\nError first, shorter sleep second"
  blockAndPrint (do
    let _ ← (Async.concurrently action2Error action1)
  )

  IO.println "\nError second, shorter sleep first"
  blockAndPrint (do
    let _ ← (Async.concurrently action1 action2Error)
  )

  IO.println "\nError second, shorter sleep second"
  blockAndPrint (do
    let _ ← (Async.concurrently action2 action1Error)
  )

  IO.println "\nArrays of action with the error in the middle"

  IO.println "\nAscending sleep durations"
  blockAndPrint (do
    let _ ← (Async.concurrentlyAll #[action1, action2Error, action3])
  )

  IO.println "\nDescending sleep durations"
  blockAndPrint (do
    let _ ← (Async.concurrentlyAll #[action3, action2Error, action1])
  )

Expected behavior: I expect the print statements following sleep operations to either output after the sleep operations finish (because that is where they are written in the code) or not at all, depending on how Async chooses to short-circuit concurrent actions.

Actual behavior: Print statements are output both before and after some sleep operations. In other words, they are output out of order relative to where they appear in the code, and are executed multiple times. See comments in the output below.

Short-circuiting sleep operations on errors

Error first, shorter sleep first
Called sleep for 1 seconds
Raising error after 1 seconds sleep call
Caught error: Error after 1 seconds sleep call

Error first, shorter sleep second
Called sleep for 2 seconds                     // BUG? Duplicate and out of order output
Called sleep for 1 seconds
Called sleep for 2 seconds
Raising error after 2 seconds sleep call
Caught error: Error after 2 seconds sleep call

Error second, shorter sleep first
Called sleep for 1 seconds
Called sleep for 2 seconds
Raising error after 2 seconds sleep call
Caught error: Error after 2 seconds sleep call

Error second, shorter sleep second
Called sleep for 1 seconds
Raising error after 1 seconds sleep call
Called sleep for 2 seconds                     // Inconsistent behavior: The action is not short-circuited
Caught error: Error after 1 seconds sleep call

Arrays of action with the error in the middle

Ascending sleep durations
Called sleep for 1 seconds
Called sleep for 2 seconds
Raising error after 2 seconds sleep call
Caught error: Error after 2 seconds sleep call

Descending sleep durations
Called sleep for 3 seconds                     // BUG? Duplicate and out of order output
Called sleep for 1 seconds
Called sleep for 2 seconds
Raising error after 2 seconds sleep call
Called sleep for 3 seconds                     // Inconsistent behavior: The action is not short-circuited
Caught error: Error after 2 seconds sleep call

Versions

• Lean 4.31.0, commit ad1c983a43face43c3e69b72f7db105f40ef280a
• Target: x86_64-unknown-linux-gnu
• Fedora Linux 44 (Toolbx Container Image)

Additional Information

Please let me know if you need additional information

Impact

Undetermined

Start with the reproducer in examples/sleep/lean/pure_lean/ShortCircuit.lean and run it with lake exe program. Then inspect the Std.Async implementations of Async.concurrently and Async.concurrentlyAll, comparing the reported output with the expected short-circuit behavior; done means the reproduced cases behave consistently without duplicate or out-of-order effects.