Additional concurrency primitives #1555
Conversation
| prelude | ||
| import Init.Data.List | ||
|
|
||
| namespace Std |
There was a problem hiding this comment.
@digama0 I'll defer to your judgement on the naming here.
| Locks a `BaseMutex`. Waits until no other thread has locked the mutex. | ||
|
|
||
| The current thread must not have already locked the mutex. | ||
| Reentrant locking is undefined behavior (inherited from the C++ implementation). |
src/Init/System/Mutex.lean
Outdated
| abbrev AtomicT := StateRefT' IO.RealWorld | ||
|
|
||
| /-- `mutex.atomically k` runs `k` with access to the mutex's state while locking the mutex. -/ | ||
| def Mutex.atomically [Monad M] [MonadLiftT BaseIO M] [MonadFinally M] |
There was a problem hiding this comment.
Is uppercase M a Scala influence 😄 ? (As I said before I would even be in favor of switching to this naming style, but that's a different discussion)
There was a problem hiding this comment.
Please let's keep the current naming convention for now.
There was a problem hiding this comment.
I think I wrote this a couple weeks back when Monad M was just gaining traction. It's uppercase because it's a type. I've changed it to m in this PR. But there's plenty of other occurrences, check out rg 'Monad M'.
There was a problem hiding this comment.
Yes, it seems they all come from @EdAyers :)
| 5. `promise.result.get` now returns `a` | ||
|
|
||
| Every promise must eventually be resolved. | ||
| Otherwise the memory used for the promise will be leaked, |
There was a problem hiding this comment.
Couldn't we skip the Deactivated state in this case? We would need more data in the lean_task_impl so that deactivate_task can identify this case I suppose.
There was a problem hiding this comment.
Indeed, we'd need more data. Right now, a Promised task looks the same as a Running task. And Running tasks are owned by the worker (and thus can't be freed).
This PR adds several additional concurrency primitives, as described in RFC #1280.
BaseMutexis a mutexMutex αis a mutex with guarded stateα(like in Rust)Condvaris a condition variablePromisecreates a task whose value will be set laterThere's also two very unoptimized queue-like primitives building on top of these:
Channelwithch.recv? : BaseIO (Option α)AsyncChannelwithch.recvAsync : BaseIO (Task (Option α))The channels don't perform too badly, based on some extremly quick benchmarking results.
Channeltransports messages at 400kHz,AsyncChannelat 700kHz on a slow machine. This seems in the same ballpark as Rust's MPSC channels, which seem to be roughly at 900kHz (I didn't run the benchmark locally).Maybe it's worth removing
Channeland only keep theAsyncChannelas it is faster (and more general).