Add minimal functionality for using GenMC mode

genmc-sys/build.rs

@@ -26,7 +26,7 @@ mod downloading {
     use super::GENMC_DOWNLOAD_PATH;
 
     /// The GenMC repository the we get our commit from.
-    pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/Patrick-6/genmc.git";
+    pub(crate) const GENMC_GITHUB_URL: &str = "https://gitlab.inf.ethz.ch/public-plf/genmc.git";
     /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
     pub(crate) const GENMC_COMMIT: &str = "af9cc9ccd5d412b16defc35dbf36571c63a19c76";
 

genmc-sys/cpp/src/MiriInterface/Setup.cpp

@@ -153,12 +153,22 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
         // FIXME(genmc,error reporting): Once a proper a proper API for passing such information is
         // implemented in GenMC, Miri should use it to improve the produced error messages.
         /* getStaticName: */ [](SAddr addr) { return "[UNKNOWN STATIC]"; },
-        // FIXME(genmc): Add proper support for initial values.
-        // This function is called to get the initial value of globals.
-        // Ideally, the function signature (on the GenMC side) would be changed to return an
-        // `std::optional<SVal>`, since the given `AAccess` may not point to a valid and initialized
-        // allocation.
-        /* initValGetter: */ [](const AAccess& a) { return SVal(0xff); },
+        // This function is called to get the initial value memory from the interpreter.
+        //
+        // This value should never be visible to the interpreted program.
+        // GenMC does not understand uninitialized memory the same way Miri does, which may cause
+        // this function to be called. The returned value can be visible to Miri or the user:
+        // - Printing the execution graph may contain this value in place of uninitialized values.
+        //   FIXME(genmc): NOTE: printing the execution graph is not yet implemented.
+        // - Non-atomic loads may return this value, but Miri ignores values of non-atomic loads.
+        // - Atomic loads will *not* see this value once mixed atomic-non-atomic support is added.
+        //   Currently, atomic loads can see this value, unless initialized by an *atomic* store.
+        //   FIXME(genmc): update this comment once mixed atomic-non-atomic support is added.
+        //
+        // FIXME(genmc): implement proper support for uninitialized memory in GenMC. Ideally, the
+        // initial value getter would return an `optional<SVal>`, since the memory location may be
+        // uninitialized.
+        /* initValGetter: */ [](const AAccess& a) { return SVal(0xDEAD); },
         // Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in
         // that case. This should no longer be required with proper mixed-size access support.
         /* skipUninitLoadChecks: */ [](MemOrdering ord) { return ord == MemOrdering::NotAtomic; },

tests/genmc/pass/litmus/IRIW-acq-sc.rs

@@ -1,12 +1,14 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
 
+// Translated from GenMC's "IRIW-acq-sc" test.
+
 #![no_main]
 
 #[path = "../../../utils/genmc.rs"]
 mod genmc;
 
-use std::ffi::c_void;
-use std::sync::atomic::{AtomicU64, Ordering};
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
 
 use crate::genmc::*;
 
@@ -15,30 +17,48 @@ static Y: AtomicU64 = AtomicU64::new(0);
 
 #[unsafe(no_mangle)]
 fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
-    let thread_order = [thread_1, thread_2, thread_3, thread_4];
-    let _ids = unsafe { create_pthreads_no_params(thread_order) };
-
-    0
-}
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
 
-pub extern "C" fn thread_1(_value: *mut c_void) -> *mut c_void {
-    X.store(1, Ordering::SeqCst);
-    std::ptr::null_mut()
-}
+    unsafe {
+        let mut a = 1234;
+        let mut b = 1234;
+        let mut c = 1234;
+        let ids = [
+            spawn_pthread_closure(|| {
+                X.store(1, SeqCst);
+            }),
+            spawn_pthread_closure(|| {
+                a = X.load(Acquire);
+                Y.load(SeqCst);
+            }),
+            spawn_pthread_closure(|| {
+                b = Y.load(Acquire);
+                c = X.load(SeqCst);
+            }),
+            spawn_pthread_closure(|| {
+                Y.store(1, SeqCst);
+            }),
+        ];
+        // Join so we can read the final values.
+        join_pthreads(ids);
 
-pub extern "C" fn thread_2(_value: *mut c_void) -> *mut c_void {
-    X.load(Ordering::Acquire);
-    Y.load(Ordering::SeqCst);
-    std::ptr::null_mut()
-}
-
-pub extern "C" fn thread_3(_value: *mut c_void) -> *mut c_void {
-    Y.load(Ordering::Acquire);
-    X.load(Ordering::SeqCst);
-    std::ptr::null_mut()
-}
+        // Check that we don't get any unexpected values:
+        if !matches!(
+            (a, b, c),
+            (0, 0, 0)
+                | (0, 0, 1)
+                | (0, 1, 0)
+                | (0, 1, 1)
+                | (1, 0, 0)
+                | (1, 0, 1)
+                | (1, 1, 0)
+                | (1, 1, 1)
+        ) {
+            std::process::abort();
+        }
 
-pub extern "C" fn thread_4(_value: *mut c_void) -> *mut c_void {
-    Y.store(1, Ordering::SeqCst);
-    std::ptr::null_mut()
+        0
+    }
 }

tests/genmc/pass/litmus/LB.rs

@@ -1,33 +1,47 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
 
+// Translated from GenMC's "litmus/LB" test.
+
 #![no_main]
 
 #[path = "../../../utils/genmc.rs"]
 mod genmc;
 
-use std::ffi::c_void;
-use std::sync::atomic::{AtomicU64, Ordering};
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
 
 static X: AtomicU64 = AtomicU64::new(0);
 static Y: AtomicU64 = AtomicU64::new(0);
 
-use crate::genmc::*;
-
 #[unsafe(no_mangle)]
 fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
-    let _ids = unsafe { create_pthreads_no_params([thread_1, thread_2]) };
-
-    0
-}
-
-extern "C" fn thread_1(_value: *mut c_void) -> *mut c_void {
-    Y.load(Ordering::Acquire);
-    X.store(2, Ordering::Release);
-    std::ptr::null_mut()
-}
-
-extern "C" fn thread_2(_value: *mut c_void) -> *mut c_void {
-    X.load(Ordering::Acquire);
-    Y.store(1, Ordering::Release);
-    std::ptr::null_mut()
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+
+    unsafe {
+        let mut a = 1234;
+        let mut b = 1234;
+        let ids = [
+            spawn_pthread_closure(|| {
+                a = Y.load(Acquire);
+                X.store(2, Release);
+            }),
+            spawn_pthread_closure(|| {
+                b = X.load(Acquire);
+                Y.store(1, Release);
+            }),
+        ];
+        // Join so we can read the final values.
+        join_pthreads(ids);
+
+        // Check that we don't get any unexpected values:
+        if !matches!((a, b), (0, 0) | (0, 2) | (1, 0)) {
+            std::process::abort();
+        }
+
+        0
+    }
 }

tests/genmc/pass/litmus/MP.rs

@@ -1,33 +1,47 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
 
+// Translated from GenMC's "litmus/MP" test.
+
 #![no_main]
 
 #[path = "../../../utils/genmc.rs"]
 mod genmc;
 
-use std::ffi::c_void;
-use std::sync::atomic::{AtomicU64, Ordering};
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
 
 static X: AtomicU64 = AtomicU64::new(0);
 static Y: AtomicU64 = AtomicU64::new(0);
 
-use crate::genmc::*;
-
 #[unsafe(no_mangle)]
 fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
-    let _ids = unsafe { create_pthreads_no_params([thread_1, thread_2]) };
-
-    0
-}
-
-extern "C" fn thread_1(_value: *mut c_void) -> *mut c_void {
-    X.store(1, Ordering::Release);
-    Y.store(1, Ordering::Release);
-    std::ptr::null_mut()
-}
-
-extern "C" fn thread_2(_value: *mut c_void) -> *mut c_void {
-    Y.load(Ordering::Acquire);
-    X.load(Ordering::Acquire);
-    std::ptr::null_mut()
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+
+    unsafe {
+        let mut a = 1234;
+        let mut b = 1234;
+        let ids = [
+            spawn_pthread_closure(|| {
+                X.store(1, Release);
+                Y.store(1, Release);
+            }),
+            spawn_pthread_closure(|| {
+                a = Y.load(Acquire);
+                b = X.load(Acquire);
+            }),
+        ];
+        // Join so we can read the final values.
+        join_pthreads(ids);
+
+        // Check that we don't get any unexpected values:
+        if !matches!((a, b), (0, 0) | (0, 1) | (1, 1)) {
+            std::process::abort();
+        }
+
+        0
+    }
 }

tests/genmc/pass/litmus/SB.rs

@@ -1,33 +1,47 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
 
+// Translated from GenMC's "litmus/SB" test.
+
 #![no_main]
 
 #[path = "../../../utils/genmc.rs"]
 mod genmc;
 
-use std::ffi::c_void;
-use std::sync::atomic::{AtomicU64, Ordering};
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
+
+use crate::genmc::*;
 
 static X: AtomicU64 = AtomicU64::new(0);
 static Y: AtomicU64 = AtomicU64::new(0);
 
-use crate::genmc::*;
-
 #[unsafe(no_mangle)]
 fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
-    let _ids = unsafe { create_pthreads_no_params([thread_1, thread_2]) };
-
-    0
-}
-
-extern "C" fn thread_1(_value: *mut c_void) -> *mut c_void {
-    X.store(1, Ordering::Release);
-    Y.load(Ordering::Acquire);
-    std::ptr::null_mut()
-}
-
-extern "C" fn thread_2(_value: *mut c_void) -> *mut c_void {
-    Y.store(1, Ordering::Release);
-    X.load(Ordering::Acquire);
-    std::ptr::null_mut()
+    // FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+    Y.store(0, Relaxed);
+
+    unsafe {
+        let mut a = 1234;
+        let mut b = 1234;
+        let ids = [
+            spawn_pthread_closure(|| {
+                X.store(1, Release);
+                a = Y.load(Acquire);
+            }),
+            spawn_pthread_closure(|| {
+                Y.store(1, Release);
+                b = X.load(Acquire);
+            }),
+        ];
+        // Join so we can read the final values.
+        join_pthreads(ids);
+
+        // Check that we don't get any unexpected values:
+        if !matches!((a, b), (0, 0) | (0, 1) | (1, 0) | (1, 1)) {
+            std::process::abort();
+        }
+
+        0
+    }
 }

tests/genmc/pass/litmus/default.rs

@@ -1,36 +1,47 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
 
+// Translated from GenMC's "litmus/default" test.
+
 #![no_main]
 
 #[path = "../../../utils/genmc.rs"]
 mod genmc;
 
-use std::ffi::c_void;
-use std::sync::atomic::{AtomicU64, Ordering};
+use std::sync::atomic::AtomicU64;
+use std::sync::atomic::Ordering::*;
 
 use crate::genmc::*;
 
 static X: AtomicU64 = AtomicU64::new(0);
 
 #[unsafe(no_mangle)]
 fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
-    let _ids = unsafe { create_pthreads_no_params([thread_1, thread_2, thread_3]) };
-
-    0
-}
-
-extern "C" fn thread_1(_value: *mut c_void) -> *mut c_void {
-    X.load(Ordering::Acquire);
-    X.load(Ordering::Acquire);
-    std::ptr::null_mut()
-}
-
-extern "C" fn thread_2(_value: *mut c_void) -> *mut c_void {
-    X.store(1, Ordering::Release);
-    std::ptr::null_mut()
-}
-
-extern "C" fn thread_3(_value: *mut c_void) -> *mut c_void {
-    X.store(2, Ordering::Release);
-    std::ptr::null_mut()
+    // FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
+    X.store(0, Relaxed);
+
+    unsafe {
+        let mut a = 1234;
+        let mut b = 1234;
+        let ids = [
+            spawn_pthread_closure(|| {
+                a = X.load(Acquire);
+                b = X.load(Acquire);
+            }),
+            spawn_pthread_closure(|| {
+                X.store(1, Release);
+            }),
+            spawn_pthread_closure(|| {
+                X.store(2, Release);
+            }),
+        ];
+        // Join so we can read the final values.
+        join_pthreads(ids);
+
+        // Check that we don't get any unexpected values:
+        if !matches!((a, b), (0, 0) | (0, 1) | (0, 2) | (1, 1) | (1, 2) | (2, 1) | (2, 2)) {
+            std::process::abort();
+        }
+
+        0
+    }
 }

tests/genmc/pass/litmus/detour.no_join.stderr

@@ -0,0 +1,2 @@
+(GenMC) Verification complete. No errors were detected.
+Number of complete executions explored: 9