libs: Simplify implementations of thread parking and guard::enable

Fixes #226.

Author: RyanGlScott

libs/Patches.md

@@ -238,6 +238,17 @@ into the main commit for that patch, and then the *Update* line can be removed.
   This feature was using an `AtomicPtr<()>` with a cast from function
   pointer to `*mut ()` that we don't support in its initializer.
 
+* Simplify implementations of thread parking and `guard::enable` (last applied: January 22, 2025)
+
+  The real implementations of these parts of the code use low-level,
+  OS-specific primitives (e.g., system calls) that Crucible cannot support. We
+  uniformly replace these parts of the code with simpler implementations:
+
+  * We use the `unsupported` configuration for thread parking, where all
+    parking-related functions are treated as no-ops.
+  * We use the Wasm configuration for the internal `guard::enable` function,
+    which simply leaks everything.
+
 # Notes
 
 This section contains more detailed notes about why certain patches are written

libs/std/src/sys/sync/thread_parking/mod.rs

@@ -1,45 +1,10 @@
-cfg_select! {
-    any(
-        all(target_os = "windows", not(target_vendor = "win7")),
-        target_os = "linux",
-        target_os = "android",
-        all(target_arch = "wasm32", target_feature = "atomics"),
-        target_os = "freebsd",
-        target_os = "openbsd",
-        target_os = "dragonfly",
-        target_os = "fuchsia",
-        target_os = "hermit",
-    ) => {
-        mod futex;
-        pub use futex::Parker;
-    }
-    any(
-        target_os = "netbsd",
-        all(target_vendor = "fortanix", target_env = "sgx"),
-        target_os = "solid_asp3",
-    ) => {
-        mod id;
-        pub use id::Parker;
-    }
-    target_vendor = "win7" => {
-        mod windows7;
-        pub use windows7::Parker;
-    }
-    all(target_vendor = "apple", not(miri)) => {
-        // Doesn't work in Miri, see <https://github.com/rust-lang/miri/issues/2589>.
-        mod darwin;
-        pub use darwin::Parker;
-    }
-    target_os = "xous" => {
-        mod xous;
-        pub use xous::Parker;
-    }
-    target_family = "unix" => {
-        mod pthread;
-        pub use pthread::Parker;
-    }
-    _ => {
-        mod unsupported;
-        pub use unsupported::Parker;
-    }
-}
+// For crucible-mir's benefit, we always use unsupported::Parker, which
+// implements all thread-parking functions as no-ops. This is arguably too
+// simplistic, as this skips calling operations that could trigger a context
+// switch in concurrent programs. Although crux-mir does have some support for
+// modeling this sort of concurrency, it has since bitrotted. (See #238.) If
+// this concurrency support is revived, then we will need to revisit the
+// approach here.
+
+mod unsupported;
+pub use unsupported::Parker;

libs/std/src/sys/thread_local/mod.rs

@@ -82,53 +82,18 @@ pub(crate) mod destructors {
 /// and the [runtime cleanup](crate::rt::thread_cleanup) function. Calling `enable`
 /// should ensure that these functions are called at the right times.
 pub(crate) mod guard {
-    cfg_select! {
-        all(target_thread_local, target_vendor = "apple") => {
-            mod apple;
-            pub(crate) use apple::enable;
-        }
-        target_os = "windows" => {
-            mod windows;
-            pub(crate) use windows::enable;
-        }
-        any(
-            all(target_family = "wasm", not(
-                all(target_os = "wasi", target_env = "p1", target_feature = "atomics")
-            )),
-            target_os = "uefi",
-            target_os = "zkvm",
-            target_os = "trusty",
-        ) => {
-            pub(crate) fn enable() {
-                // FIXME: Right now there is no concept of "thread exit" on
-                // wasm, but this is likely going to show up at some point in
-                // the form of an exported symbol that the wasm runtime is going
-                // to be expected to call. For now we just leak everything, but
-                // if such a function starts to exist it will probably need to
-                // iterate the destructor list with these functions:
-                #[cfg(all(target_family = "wasm", target_feature = "atomics"))]
-                #[allow(unused)]
-                use super::destructors::run;
-                #[allow(unused)]
-                use crate::rt::thread_cleanup;
-            }
-        }
-        any(
-            target_os = "hermit",
-            target_os = "xous",
-        ) => {
-            // `std` is the only runtime, so it just calls the destructor functions
-            // itself when the time comes.
-            pub(crate) fn enable() {}
-        }
-        target_os = "solid_asp3" => {
-            mod solid;
-            pub(crate) use solid::enable;
-        }
-        _ => {
-            mod key;
-            pub(crate) use key::enable;
-        }
+    pub(crate) fn enable() {
+        // FIXME: Right now there is no concept of "thread exit" on
+        // wasm, but this is likely going to show up at some point in
+        // the form of an exported symbol that the wasm runtime is going
+        // to be expected to call. For now we just leak everything, but
+        // if such a function starts to exist it will probably need to
+        // iterate the destructor list with these functions:
+        #[cfg(all(target_family = "wasm", target_feature = "atomics"))]
+        #[allow(unused)]
+        use super::destructors::run;
+        #[allow(unused)]
+        use crate::rt::thread_cleanup;
     }
 }