IOSim: timeout can return while its assasin threas is still ailve

Open
#271 3 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
48/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Tech stack
haskell
Domain
testing

Research direction

Start by reading the IOSim implementation of timeout, its assassin thread, and the runSimStrictShutdown checks; the issue gives six reproductions using threadDelay, yield, and STM. Trace the tie cases where the assassin remains queued or has a pending ThreadKilled, then verify that all scenarios finish without FailureSloppyShutdown while preserving their stated results.

Written by the indexing model from the issue text.

Description

bug

Describe the bug
timeout can return while its assassin thread is still alive, so runSimStrictShutdown fails with FailureSloppyShutdown

In IOSim, timeout forks an assassin thread when its timer fires. If the action finishes at the same moment the timeout expires, timeout can return while the assassin is still alive. Any simulation run with runSimStrictShutdown then fails with FailureSloppyShutdown.

The result itself is correct: the leftover assassin never throws. But in simulations the action often finishes exactly at the deadline, so this makes strict shutdown unusable for code that uses timeout. GHC has no equivalent of the strict-shutdown check, so the problem only shows up in the simulator.

To Reproduce

Each scenario run with runSimStrictShutdown:

Scenario Code Result
a. timer never fires timeout 1 (threadDelay 0.5) Just ()
b. timeout wins timeout 1 (threadDelay 2) Nothing
c. tie, action finishes first timeout 1 (threadDelay 1) FailureSloppyShutdown
c′. c, then yield timeout 1 (threadDelay 1) <* yield FailureSloppyShutdown
d. tie, action yields before finishing timeout 1 (threadDelay 1 >> atomically (pure ())) FailureSloppyShutdown
d′. d, then yield timeout 1 (threadDelay 1 >> atomically (pure ())) <* yield Just ()
  • Case c: the assassin hasn't run yet. At 1s the delay timer wakes the main thread, and the timeout timer forks the assassin, which is queued behind main.
    Main leaves the TimeoutFrame, takes the lock and finishes. The assassin is still in the run queue, so TraceMainReturn lists it as running. A yield
    doesn't help: the assassin's tryPutTMVar commit yields too, so main finishes before the assassin exits.
  • Case d: the assassin holds the lock but hasn't thrown yet. The frame exit killThreads it. Killing an unmasked thread doesn't block; it only replaces the
    thread's next action with Throw ThreadKilled. So the assassin isn't dead yet when main finishes. One yield lets it terminate, which is why d′ passes.
Dominant language
Haskell
Stars
57
Forks
25
PR merge metrics
No merged PRs in 30d

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from IntersectMBO/io-sim

All issues in IntersectMBO/io-sim

Similar issues

More Haskell issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.