feat: Mutex, Condvar

src/Init/System.lean

@@ -7,4 +7,5 @@ prelude
 import Init.System.IO
 import Init.System.Platform
 import Init.System.Uri
+import Init.System.Mutex
 import Init.System.Promise

src/Init/System/Mutex.lean

@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+prelude
+import Init.System.IO
+import Init.Control.StateRef
+
+namespace IO
+
+private opaque BaseMutexImpl : NonemptyType.{0}
+
+/--
+Mutual exclusion primitive (a lock).
+
+If you want to guard shared state, use `Mutex α` instead.
+-/
+def BaseMutex : Type := BaseMutexImpl.type
+
+instance : Nonempty BaseMutex := BaseMutexImpl.property
+
+/-- Creates a new `BaseMutex`. -/
+@[extern "lean_io_basemutex_new"]
+opaque BaseMutex.new : BaseIO BaseMutex
+
+/--
+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).
+-/
+@[extern "lean_io_basemutex_lock"]
+opaque BaseMutex.lock (mutex : @& BaseMutex) : BaseIO Unit
+
+/--
+Unlocks a `BaseMutex`.
+
+The current thread must have already locked the mutex.
+Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).
+-/
+@[extern "lean_io_basemutex_unlock"]
+opaque BaseMutex.unlock (mutex : @& BaseMutex) : BaseIO Unit
+
+private opaque CondvarImpl : NonemptyType.{0}
+
+/-- Condition variable. -/
+def Condvar : Type := CondvarImpl.type
+
+instance : Nonempty Condvar := CondvarImpl.property
+
+/-- Creates a new condition variable. -/
+@[extern "lean_io_condvar_new"]
+opaque Condvar.new : BaseIO Condvar
+
+/-- Waits until another thread calls `notifyOne` or `notifyAll`. -/
+@[extern "lean_io_condvar_wait"]
+opaque Condvar.wait (condvar : @& Condvar) (mutex : @& BaseMutex) : BaseIO Unit
+
+/-- Wakes up a single other thread executing `wait`. -/
+@[extern "lean_io_condvar_notify_one"]
+opaque Condvar.notifyOne (condvar : @& Condvar) : BaseIO Unit
+
+/-- Wakes up all other threads executing `wait`. -/
+@[extern "lean_io_condvar_notify_all"]
+opaque Condvar.notifyAll (condvar : @& Condvar) : BaseIO Unit
+
+/-- Waits on the condition variable until the predicate is true. -/
+def Condvar.waitUntil [Monad m] [MonadLift BaseIO m]
+    (condvar : Condvar) (mutex : BaseMutex) (pred : m Bool) : m Unit := do
+  while !(← pred) do
+    condvar.wait mutex
+
+/--
+Mutual exclusion primitive (lock) guarding shared state of type `α`.
+
+The type `Mutex α` is similar to `IO.Ref α`,
+except that concurrent accesses are guarded by a mutex
+instead of atomic pointer operations and busy-waiting.
+-/
+structure Mutex (α : Type) where private mk ::
+  private ref : IO.Ref α
+  mutex : BaseMutex
+
+instance [Nonempty α] : Nonempty (Mutex α) :=
+  let ⟨ref⟩ := inferInstanceAs (Nonempty _)
+  let ⟨mutex⟩ := inferInstanceAs (Nonempty _)
+  ⟨{ref, mutex}⟩
+
+instance : Coe (Mutex α) BaseMutex where coe := Mutex.mutex
+
+/-- Creates a new mutex. -/
+def Mutex.new (a : α) : BaseIO (Mutex α) :=
+  return { ref := ← mkRef a, mutex := ← BaseMutex.new }
+
+/--
+`AtomicT α m` is the monad that can be atomically executed inside a `Mutex α`,
+with outside monad `m`.
+The action has access to the state `α` of the mutex (via `get` and `set`).
+-/
+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]
+    (mutex : Mutex α) (k : AtomicT α m β) : m β := do
+  try
+    mutex.mutex.lock
+    k mutex.ref
+  finally
+    mutex.mutex.unlock
+
+/--
+`mutex.atomicallyOnce condvar pred k` runs `k`,
+waiting on `condvar` until `pred` returns true.
+Both `k` and `pred` have access to the mutex's state.
+-/
+def Mutex.atomicallyOnce [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
+    (mutex : Mutex α) (condvar : Condvar)
+    (pred : AtomicT α m Bool) (k : AtomicT α m β) : m β :=
+  let _ : MonadLift BaseIO (AtomicT α m) := ⟨liftM⟩
+  mutex.atomically do
+    condvar.waitUntil mutex pred
+    k

src/runtime/CMakeLists.txt

@@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
-process.cpp object_ref.cpp mpn.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})

src/runtime/init_module.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "runtime/io.h"
 #include "runtime/stack_overflow.h"
 #include "runtime/process.h"
+#include "runtime/mutex.h"
 
 namespace lean {
 extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
@@ -19,6 +20,7 @@ extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
     initialize_object();
     initialize_io();
     initialize_thread();
+    initialize_mutex();
     initialize_process();
     initialize_stack_overflow();
 }
@@ -28,6 +30,7 @@ void initialize_runtime_module() {
 void finalize_runtime_module() {
     finalize_stack_overflow();
     finalize_process();
+    finalize_mutex();
     finalize_thread();
     finalize_io();
     finalize_object();

src/runtime/mutex.cpp

@@ -0,0 +1,78 @@
+/*
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Gabriel Ebner
+*/
+#include <lean/lean.h>
+#include "runtime/mutex.h"
+#include "runtime/io.h"
+#include "runtime/object.h"
+#include "runtime/thread.h"
+
+namespace lean {
+
+static lean_external_class * g_basemutex_external_class = nullptr;
+static void basemutex_finalizer(void * h) {
+    delete static_cast<mutex *>(h);
+}
+static void basemutex_foreach(void *, b_obj_arg) {}
+
+static mutex * basemutex_get(lean_object * mtx) {
+    return static_cast<mutex *>(lean_get_external_data(mtx));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_basemutex_new(obj_arg) {
+    return io_result_mk_ok(lean_alloc_external(g_basemutex_external_class, new mutex));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_basemutex_lock(b_obj_arg mtx, obj_arg) {
+    basemutex_get(mtx)->lock();
+    return io_result_mk_ok(box(0));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_basemutex_unlock(b_obj_arg mtx, obj_arg) {
+    basemutex_get(mtx)->unlock();
+    return io_result_mk_ok(box(0));
+}
+
+static lean_external_class * g_condvar_external_class = nullptr;
+static void condvar_finalizer(void * h) {
+    delete static_cast<condition_variable *>(h);
+}
+static void condvar_foreach(void *, b_obj_arg) {}
+
+static condition_variable * condvar_get(lean_object * mtx) {
+    return static_cast<condition_variable *>(lean_get_external_data(mtx));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_condvar_new(obj_arg) {
+    return io_result_mk_ok(lean_alloc_external(g_condvar_external_class, new condition_variable));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_condvar_wait(b_obj_arg condvar, b_obj_arg mtx, obj_arg) {
+    unique_lock<mutex> lock(*basemutex_get(mtx), std::adopt_lock_t());
+    condvar_get(condvar)->wait(lock);
+    lock.release();
+    return io_result_mk_ok(box(0));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_one(b_obj_arg condvar, obj_arg) {
+    condvar_get(condvar)->notify_one();
+    return io_result_mk_ok(box(0));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_all(b_obj_arg condvar, obj_arg) {
+    condvar_get(condvar)->notify_all();
+    return io_result_mk_ok(box(0));
+}
+
+void initialize_mutex() {
+    g_basemutex_external_class = lean_register_external_class(basemutex_finalizer, basemutex_foreach);
+    g_condvar_external_class = lean_register_external_class(condvar_finalizer, condvar_foreach);
+}
+
+void finalize_mutex() {
+}
+
+}

src/runtime/mutex.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#pragma once
+
+namespace lean {
+void initialize_mutex();
+void finalize_mutex();
+}