feat: implement the basic libuv event loop

Co-authored-by: Henrik Böving <hargonix@gmail.com>

src/Std/Internal.lean

@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 prelude
 import Std.Internal.Parsec
+import Std.Internal.UV
 
 /-!
 This directory is used for components of the standard library that are either considered

src/Std/Internal/UV.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init.System.IO
+import Init.System.Promise
+
+namespace Std
+namespace Internal
+namespace UV
+
+namespace Loop
+
+/--
+Options for configuring the event loop behavior.
+-/
+structure Loop.Options where
+  /--
+  Accumulate the amount of idle time the event loop spends in the event provider.
+  -/
+  accumulateIdleTime : Bool := False
+
+  /--
+  Block a SIGPROF signal when polling for new events. It's commonly used for unnecessary wakeups
+  when using a sampling profiler.
+  -/
+  blockSigProfSignal : Bool := False
+
+/--
+Configures the event loop with the specified options.
+-/
+@[extern "lean_uv_event_loop_configure"]
+opaque configure (options : Loop.Options) : BaseIO Unit
+
+/--
+Checks if the event loop is still active and processing events.
+-/
+@[extern "lean_uv_event_loop_alive"]
+opaque alive : BaseIO Bool
+
+end Loop
+
+end UV
+end Internal
+end Std

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 mutex.cpp libuv.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/event_loop.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

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "runtime/process.h"
 #include "runtime/mutex.h"
 #include "runtime/init_module.h"
+#include "runtime/libuv.h"
 
 namespace lean {
 extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
@@ -24,6 +25,7 @@ extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
     initialize_mutex();
     initialize_process();
     initialize_stack_overflow();
+    initialize_libuv();
 }
 void initialize_runtime_module() {
     lean_initialize_runtime_module();

src/runtime/libuv.cpp

@@ -2,21 +2,35 @@
 Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Author: Markus Himmel
-*/
+Author: Markus Himmel, Sofia Rodrigues
+ */
+#include <pthread.h>
 #include "runtime/libuv.h"
+#include "runtime/object.h"
+
+namespace lean {
 
 #ifndef LEAN_EMSCRIPTEN
 #include <uv.h>
 
+extern "C" void initialize_libuv() {
+    initialize_libuv_loop();
+
+    lthread([]() { event_loop_run_loop(&global_ev); });
+}
+
+/* Lean.libUVVersionFn : Unit → Nat */
 extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
     return lean_unsigned_to_nat(uv_version());
 }
 
 #else
 
+extern "C" void initialize_libuv() {}
+
 extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
     return lean_box(0);
 }
 
 #endif
+}

src/runtime/libuv.h

@@ -2,9 +2,28 @@
 Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Author: Markus Himmel
+Author: Markus Himmel, Sofia Rodrigues
 */
 #pragma once
 #include <lean/lean.h>
+#include "runtime/uv/event_loop.h"
+#include "runtime/alloc.h"
+#include "runtime/io.h"
+#include "runtime/utf8.h"
+#include "runtime/object.h"
+#include "runtime/thread.h"
+#include "runtime/allocprof.h"
+#include "runtime/object.h"
 
+namespace lean {
+#ifndef LEAN_EMSCRIPTEN
+#include <uv.h>
+#endif
+
+extern "C" void initialize_libuv();
+
+// =======================================
+// General LibUV functions.
 extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg);
+
+}

src/runtime/uv/event_loop.cpp

@@ -0,0 +1,129 @@
+/*
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sofia Rodrigues
+*/
+#include "runtime/uv/event_loop.h"
+
+namespace lean {
+#ifndef LEAN_EMSCRIPTEN
+using namespace std;
+
+event_loop_t global_ev;
+
+// Utility function for error checking. This function is only used inside the
+// initializition of the event loop.
+static void check_uv(int result, const char * msg) {
+    if (result != 0) {
+        std::string err_message = std::string(msg) + ": " + uv_strerror(result);
+        lean_internal_panic(err_message.c_str());
+    }
+}
+
+// The callback that stops the loop when it's called.
+void async_callback(uv_async_t * handle) {
+    uv_stop(handle->loop);
+}
+
+// Awakes the event loop and stops it so it can receive future requests.
+void event_loop_wake(event_loop_t * event_loop) {
+    int result = uv_async_send(&event_loop->async);
+    (void)result;
+    lean_assert(result == 0);
+}
+
+// Initializes the event loop
+void event_loop_init(event_loop_t * event_loop) {
+    event_loop->loop = uv_default_loop();
+    check_uv(uv_mutex_init_recursive(&event_loop->mutex), "Failed to initialize mutex");
+    check_uv(uv_cond_init(&event_loop->cond_var), "Failed to initialize condition variable");
+    check_uv(uv_async_init(event_loop->loop, &event_loop->async, NULL), "Failed to initialize async");
+    event_loop->n_waiters = 0;
+}
+
+// Locks the event loop for the side of the requesters.
+void event_loop_lock(event_loop_t * event_loop) {
+    if (uv_mutex_trylock(&event_loop->mutex) != 0) {
+        event_loop->n_waiters++;
+        event_loop_wake(event_loop);
+        uv_mutex_lock(&event_loop->mutex);
+        event_loop->n_waiters--;
+    }
+}
+
+// Unlock event loop
+void event_loop_unlock(event_loop_t * event_loop) {
+    uv_mutex_unlock(&event_loop->mutex);
+    if (event_loop->n_waiters == 0) {
+        uv_cond_signal(&event_loop->cond_var);
+    }
+}
+
+// Runs the loop and stops when it needs to register new requests.
+void event_loop_run_loop(event_loop_t * event_loop) {
+    while (uv_loop_alive(event_loop->loop)) {
+        uv_mutex_lock(&event_loop->mutex);
+
+        if (event_loop->n_waiters != 0) {
+            uv_cond_wait(&event_loop->cond_var, &event_loop->mutex);
+        }
+
+        if (event_loop->n_waiters == 0) {
+            uv_run(event_loop->loop, UV_RUN_ONCE);
+        }
+
+        uv_mutex_unlock(&event_loop->mutex);
+    }
+}
+
+/* Std.Internal.UV.Loop.configure (options : Loop.Options) : BaseIO Unit */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ ) {
+    bool accum = lean_ctor_get_uint8(options, 0);
+    bool block = lean_ctor_get_uint8(options, 1);
+
+    event_loop_lock(&global_ev);
+
+    if (accum && uv_loop_configure(global_ev.loop, UV_METRICS_IDLE_TIME) != 0) {
+        return io_result_mk_error("failed to configure global_ev.loop with UV_METRICS_IDLE_TIME");
+    }
+
+    #if!defined(WIN32) && !defined(_WIN32)
+    if (block && uv_loop_configure(global_ev.loop, UV_LOOP_BLOCK_SIGNAL, SIGPROF) != 0) {
+        return io_result_mk_error("failed to configure global_ev.loop with UV_LOOP_BLOCK_SIGNAL");
+    }
+    #endif
+
+    event_loop_unlock(&global_ev);
+
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+/* Std.Internal.UV.Loop.alive : BaseIO UInt64 */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ ) {
+    event_loop_lock(&global_ev);
+    int is_alive = uv_loop_alive(global_ev.loop);
+    event_loop_unlock(&global_ev);
+
+    return lean_io_result_mk_ok(lean_box(is_alive));
+}
+
+void initialize_libuv_loop() {
+    event_loop_init(&global_ev);
+}
+
+#else
+
+/* Std.Internal.UV.Loop.configure (options : Loop.Options) : BaseIO Unit */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ ) {
+    return io_result_mk_error("lean_uv_event_loop_configure is not supported");
+}
+
+/* Std.Internal.UV.Loop.alive : BaseIO UInt64 */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ ) {
+    return io_result_mk_error("lean_uv_event_loop_alive is not supported");
+}
+
+#endif
+
+}

src/runtime/uv/event_loop.h

@@ -0,0 +1,48 @@
+/*
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sofia Rodrigues
+*/
+#pragma once
+#include <lean/lean.h>
+#include "runtime/io.h"
+#include "runtime/object.h"
+
+namespace lean {
+
+void initialize_libuv_loop();
+
+#ifndef LEAN_EMSCRIPTEN
+using namespace std;
+#include <uv.h>
+
+// Event loop structure for managing asynchronous events and synchronization across multiple threads.
+typedef struct {
+    uv_loop_t  * loop;      // The libuv event loop.
+    uv_mutex_t   mutex;     // Mutex for protecting shared resources.
+    uv_cond_t    cond_var;  // Condition variable for thread synchronization.
+    uv_async_t   async;     // Async handle to notify the main event loop.
+    _Atomic(int) n_waiters; // Atomic counter for managing waiters.
+} event_loop_t;
+
+// The multithreaded event loop object for all tasks in the task manager.
+extern event_loop_t global_ev;
+
+// =======================================
+// Event loop manipulation functions.
+void event_loop_init(event_loop_t *event_loop);
+void event_loop_cleanup(event_loop_t *event_loop);
+void event_loop_lock(event_loop_t *event_loop);
+void event_loop_unlock(event_loop_t *event_loop);
+void event_loop_wake(event_loop_t *event_loop);
+void event_loop_run_loop(event_loop_t *event_loop);
+
+#endif
+
+// =======================================
+// Global event loop manipulation functions
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ );
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ );
+
+}