work around gettid not being available on glibc 2.27 and macOS

leanprover · Oct 28, 2024 · c7086cd · c7086cd
1 parent e298702
commit c7086cd
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 7 deletions.
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
@@ -802,8 +802,11 @@ def run (args : SpawnArgs) : IO String := do
 
 end Process
 
-/-- Returns the thread ID of the calling thread. -/
-@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt32
+/--
+Returns an ID identifying the current thread. May not be identical to the operating system's thread
+id.
+-/
+@[extern "lean_io_get_thread_id"] opaque getLeanThreadID : BaseIO UInt64
 
 structure AccessRight where
   read : Bool := false

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
@@ -434,7 +434,7 @@ which is reported in the returned snapshot.
 -/
 def runAsyncAsSnapshot (act : TermElabM Unit) (desc := "") : TermElabM (Task Language.SnapshotTree) := do
   let t ← runAsync do
-    let tid ← IO.getTID
+    let tid ← IO.getLeanThreadID
     modifyTraceState fun _ => { tid }
     try
       withTraceNode `Elab.async (fun _ => return desc) do

diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
@@ -65,7 +65,7 @@ structure TraceElem where
 
 structure TraceState where
   /-- Thread ID, used by `trace.profiler.output`. -/
-  tid     : UInt32 := 0
+  tid     : UInt64 := 0
   traces  : PersistentArray TraceElem := {}
   deriving Inhabited
 

diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp
@@ -316,9 +316,17 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
     return lean_io_result_mk_ok(box_uint32(getpid()));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
-    static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
-    return lean_io_result_mk_ok(box_uint32(gettid()));
+extern "C" LEAN_EXPORT obj_res lean_io_get_thread_id(obj_arg) {
+    uint64_t tid;
+#ifdef LEAN_WINDOWS
+    tid = GetCurrentThreadId();
+#elif defined(__APPLE__)
+    pthread_threadid_np(NULL, &tid);
+#else
+    // should use gettid, but that is glibc 2.30+
+    tid = static_cast<uint64>(pthread_self())));
+#endif
+    return lean_io_result_mk_ok(box_uint64(static_cast<uint64>(pthread_self())));
 }
 
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {