Skip to content

Commit

Permalink
feat: IO.getTID (#6049)
Browse files Browse the repository at this point in the history
This PR adds a primitive for accessing the current thread ID

To be used in a thread-aware trace profiler
  • Loading branch information
Kha authored Nov 16, 2024
1 parent 7643867 commit a449e3f
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 0 deletions.
3 changes: 3 additions & 0 deletions src/Init/System/IO.lean
Original file line number Diff line number Diff line change
Expand Up @@ -802,6 +802,9 @@ 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 UInt64

structure AccessRight where
read : Bool := false
write : Bool := false
Expand Down
22 changes: 22 additions & 0 deletions src/runtime/process.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,10 @@ Author: Jared Roesch
#include <limits.h> // NOLINT
#endif

#ifdef __linux
#include <sys/syscall.h>
#endif

#include "runtime/object.h"
#include "runtime/io.h"
#include "runtime/array_ref.h"
Expand Down Expand Up @@ -80,6 +84,10 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
return lean_io_result_mk_ok(box_uint32(GetCurrentProcessId()));
}

extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
return lean_io_result_mk_ok(box_uint64(GetCurrentThreadId()));
}

extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
DWORD exit_code;
Expand Down Expand Up @@ -316,6 +324,20 @@ 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) {
uint64_t tid;
#ifdef __APPLE__
lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
#elif defined(LEAN_EMSCRIPTEN)
tid = 0;
#else
// since Linux 2.4.11, our glibc 2.27 requires at least 3.2
// glibc 2.30 would provide a wrapper
tid = (pid_t)syscall(SYS_gettid);
#endif
return lean_io_result_mk_ok(box_uint64(tid));
}

extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));
Expand Down

0 comments on commit a449e3f

Please sign in to comment.