lean4
lean4 copied to clipboard
leanprover
feat: `modifyM`/`modifyGetM` for `IO.Ref`
Adds IO.Ref.modfyM / IO.Ref.modifyGetM which are monadic variants of IO.Ref.modify (ST.Prim.Ref.modify) / IO.Ref.modifyGet (ST.Prim.Ref.modifyGet). Like them, it uses ST.Prim.Ref.take to atomically modify the reference via busy-waiting, but allow users to perform BaseIO actions within the critical section. This is safe because BaseIO / ST σ α actions do not throw exceptions. Without these utilities, to modify a reference while preforming I/O, one needs to use IO.Mutex. Thus, this provides a lightweight alternative for users.
The outstanding question here is whether this is good idea or if users should be expected to use IO.Mutex if they wish to modify a reference while performing I/O.
Mathlib CI status (docs):
- ✅ Mathlib branch lean-pr-testing-3641 has successfully built against this PR. (2024-03-09 22:58:24) View Log
- ✅ Mathlib branch lean-pr-testing-3641 has successfully built against this PR. (2024-03-09 23:37:29) View Log
One potential issue is that you can get deadlocks using modify this way, right?
@mhuisi Could you elaborate? I do not see how this introduces more possibility of deadlock than IO.Ref.modify and/or IO.Mutex. The example I can think of is that if you wait on a thread within the modifyM that is also waiting to modify the reference. But the same issue appears with IO.Mutex, so it does not seem to surprising.
A common access pattern if modify allows IO would be to use modify on one IO.Ref and within that use modify on another IO.Ref. If another call site uses these modify calls in switched order, you may get deadlocks.
I agree that we can already cause deadlocks now and especially with other primitives - I just wanted to point out that this opens up this particular likely pitfall.