From 7c552380dab06fc6b074a03546beb5351e30d379 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 1 Sep 2022 13:33:34 +0200 Subject: [PATCH] feat: `Mutex`, `Condvar` --- src/Init/System.lean | 1 + src/Init/System/Mutex.lean | 123 ++++++++++++++++++++++++++++++++++++ src/runtime/CMakeLists.txt | 2 +- src/runtime/init_module.cpp | 3 + src/runtime/mutex.cpp | 78 +++++++++++++++++++++++ src/runtime/mutex.h | 12 ++++ 6 files changed, 218 insertions(+), 1 deletion(-) create mode 100644 src/Init/System/Mutex.lean create mode 100644 src/runtime/mutex.cpp create mode 100644 src/runtime/mutex.h diff --git a/src/Init/System.lean b/src/Init/System.lean index 5538d24944..8c0766bc23 100644 --- a/src/Init/System.lean +++ b/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 diff --git a/src/Init/System/Mutex.lean b/src/Init/System/Mutex.lean new file mode 100644 index 0000000000..4b5740fea4 --- /dev/null +++ b/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 diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index f7f9aedd11..37c4e42bbd 100644 --- a/src/runtime/CMakeLists.txt +++ b/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}) diff --git a/src/runtime/init_module.cpp b/src/runtime/init_module.cpp index a10ad2e5b7..f562dca698 100644 --- a/src/runtime/init_module.cpp +++ b/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(); diff --git a/src/runtime/mutex.cpp b/src/runtime/mutex.cpp new file mode 100644 index 0000000000..32d6c35b35 --- /dev/null +++ b/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 +#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(h); +} +static void basemutex_foreach(void *, b_obj_arg) {} + +static mutex * basemutex_get(lean_object * mtx) { + return static_cast(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(h); +} +static void condvar_foreach(void *, b_obj_arg) {} + +static condition_variable * condvar_get(lean_object * mtx) { + return static_cast(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 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() { +} + +} diff --git a/src/runtime/mutex.h b/src/runtime/mutex.h new file mode 100644 index 0000000000..779f1e9815 --- /dev/null +++ b/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(); +}