New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Additional concurrency primitives #1280
Comments
FWIW, I think the LSP comment should be restated to point out that this is only a problem with clients without (correct) |
I'm pretty sure that neovim completely ignores the version field (and doesn't set |
Yikes, I assumed that they would at least ignore diagnostics with regressing version numbers... I only checked that lsp-mode set |
Another interesting primitive is Promise (α : Type) : Type
Promise.new [Nonempty α] : BaseIO (Promise α)
Promise.resolve : α → Promise α → BaseIO Unit
Promise.result : Promise α → Task α The semantics is that the task |
@ydewit Thanks for the references! If you look closely the split is already there:
|
Yes, I see now! I think that I unconsciously was assuming that even though all Tasks are a Future, not necessarily all Futures are Tasks, if they can be represented as something other than a Task. |
@gebner Should we close this issue? |
Lean only has a single concurrency primitive right now,
Task
, which is very nice when it fits your use case (and also hard to misuse) but you can't easily use it to achieve mutual exclusion. The most complex concurrent program (to my knowledge) in Lean so far is the LSP server, and it already casually mentions possible race conditions in its comments:To be clear, the concrete issue here is that something can happen between
cancelTk.check
andpublishDiagnostics
. (Of course, it's not just thepublishDiagnostics
call that is a problem. Every otherpublish*
call falls prey to the same race condition.)The obvious fix for this race condition is to add a mutex primitive and then just acquire the lock to execute
cancelTk.check
andpublishDiagnostics
atomically. A concrete API proposal could look like this:Alternatively we could add proper locking to
IO.Ref
. Right now,IO.Ref
s use busy waiting in case of concurrent modifications, so they cannot (practically) be used for mutual exclusion. Adding locking toIO.Ref
has several issues. One is a performance issue. We'd need to allocate a mutex for everyIO.Ref
used from multiple threads and the default mutex implementations take something like 40 bytes of memory and some overhead. We could do our own implementation or integrate something like parking lot to make this cheaper though. The other issue is when to allocate this mutex, e.g. a reference might first be taken in a single-thread context, and only then be sent to another thread while it is still taken.Other useful primitives would be condition variables and (blocking) queues:
See also Haskell's
MVar
s for another reference-like concurrency primitive that can be used to directly build queues.The text was updated successfully, but these errors were encountered: