Clean up mutex_simple test

Author: Patrick-6

tests/genmc/pass/shims/mutex_simple.rs

@@ -5,11 +5,12 @@
 // Miri running with GenMC intercepts the Mutex functions `lock`, `try_lock` and `unlock`, instead of running their actual implementation.
 // This interception should not break any functionality.
 //
+// FIXME(genmc): Once GenMC supports mixed size accesses, add stack/heap allocated Mutexes to the test.
 // FIXME(genmc): Once the actual implementation of mutexes can be used in GenMC mode and there is a setting to disable Mutex interception: Add test revision without interception.
 //
 // Miri provides annotations to GenMC for the condition required to unblock a thread blocked on a Mutex lock call.
 // This massively reduces the number of blocked executions we need to explore (in this test we require zero blocked execution).
-// We use verbose output to test that there are no blocked executions introduces by future changes, only completed executions.
+// We use verbose output to check that this test always explores zero blocked executions.
 
 #![no_main]
 #![feature(abort_unwind)]
@@ -23,7 +24,8 @@ use crate::genmc::*;
 
 const REPS: u64 = 3;
 
-static LOCK: Mutex<[u64; 32]> = Mutex::new([1234; 32]);
+static LOCK: Mutex<u64> = Mutex::new(0);
+static OTHER_LOCK: Mutex<u64> = Mutex::new(1234);
 
 #[unsafe(no_mangle)]
 fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
@@ -32,44 +34,35 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
 }
 
 fn main_() {
-    // FIXME(genmc): Try using stack/heap allocated Mutexes once GenMC has mixed-size access support.
+    // Two mutexes should not interfere, holding this guard does not affect the other mutex.
+    let other_guard = OTHER_LOCK.lock().unwrap();
 
-    let mut guard = LOCK.lock().unwrap();
-    for &v in guard.iter() {
-        assert!(v == 1234); // Check that mutex values are initialized correctly
-    }
-    guard[0] = 0;
-    guard[1] = 10;
-    assert!(guard[0] == 0 && guard[1] == 10); // Check if changes are accepted
-
-    // Trying to lock should fail if the lock is already held
+    let guard = LOCK.lock().unwrap();
+    // Trying to lock should fail if the mutex is already held.
     assert!(LOCK.try_lock().is_err());
-
     // Dropping the guard should unlock the mutex correctly.
     drop(guard);
-    {
-        // Trying to lock now should succeed since the lock is unlocked.
-        assert!(LOCK.try_lock().is_ok());
-    }
+    // Trying to lock now should succeed.
+    assert!(LOCK.try_lock().is_ok());
 
     // Spawn multiple threads interacting with the same mutex.
     unsafe {
         let ids = [
             spawn_pthread_closure(|| {
                 for _ in 0..REPS {
-                    let mut guard = LOCK.lock().unwrap();
-                    guard[0] += 2;
+                    *LOCK.lock().unwrap() += 2;
                 }
             }),
             spawn_pthread_closure(|| {
                 for _ in 0..REPS {
-                    let mut guard = LOCK.lock().unwrap();
-                    guard[0] += 4;
+                    *LOCK.lock().unwrap() += 4;
                 }
             }),
         ];
         join_pthreads(ids);
     }
-    // Due to locking, all increments should be visible in every execution GenMC explores.
-    assert!(LOCK.lock().unwrap()[0] == REPS * 6);
+    // Due to the Mutex, all increments should be visible in every explored execution.
+    assert!(*LOCK.lock().unwrap() == REPS * 6);
+
+    drop(other_guard);
 }