Remove obsolete pthread mutex events. (#921)

Type of pthread mutex is u1 instead of u32.
Remove intrinsics for pthread_mutexattr_setpolicy_np.

Author: xeren

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

@@ -41,9 +41,6 @@
 import com.dat3m.dartagnan.program.event.lang.dat3m.DynamicThreadJoin;
 import com.dat3m.dartagnan.program.event.lang.linux.*;
 import com.dat3m.dartagnan.program.event.lang.llvm.*;
-import com.dat3m.dartagnan.program.event.lang.pthread.InitLock;
-import com.dat3m.dartagnan.program.event.lang.pthread.Lock;
-import com.dat3m.dartagnan.program.event.lang.pthread.Unlock;
 import com.dat3m.dartagnan.program.event.lang.spirv.*;
 import com.dat3m.dartagnan.program.event.lang.svcomp.*;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
@@ -388,28 +385,6 @@ public static Xchg newXchg(Register register, Expression address, Expression sto
         }
     }
 
-    // =============================================================================================
-    // ========================================== Pthread ==========================================
-    // =============================================================================================
-
-    public static class Pthread {
-        private Pthread() {
-        }
-
-        public static InitLock newInitLock(String name, Expression address, Expression ignoreAttributes) {
-            //TODO store attributes inside mutex object
-            return new InitLock(name, address, expressions.makeZero(types.getArchType()));
-        }
-
-        public static Lock newLock(String name, Expression address) {
-            return new Lock(name, address);
-        }
-
-        public static Unlock newUnlock(String name, Expression address) {
-            return new Unlock(name, address);
-        }
-    }
-
     // =============================================================================================
     // ========================================== Atomics ==========================================
     // =============================================================================================

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java

@@ -17,9 +17,6 @@
 import com.dat3m.dartagnan.program.event.lang.catomic.*;
 import com.dat3m.dartagnan.program.event.lang.linux.*;
 import com.dat3m.dartagnan.program.event.lang.llvm.*;
-import com.dat3m.dartagnan.program.event.lang.pthread.InitLock;
-import com.dat3m.dartagnan.program.event.lang.pthread.Lock;
-import com.dat3m.dartagnan.program.event.lang.pthread.Unlock;
 import com.dat3m.dartagnan.program.event.lang.spirv.*;
 import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic;
 import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic;
@@ -56,11 +53,6 @@ public interface EventVisitor<T> {
 
     // ============================== Language-level events ==============================
 
-    // ------------------ Pthread Events ------------------
-    default T visitInitLock(InitLock e) { return visitMemEvent(e); }
-    default T visitLock(Lock e) { return visitMemEvent(e); }
-    default T visitUnlock(Unlock e) { return visitMemEvent(e); }
-
     // ------------------ Common Events ------------------
     default T visitStoreExclusive(StoreExclusive e) { return visitMemEvent(e); }
     default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); };

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/InitLock.java

@@ -659,13 +659,15 @@ private List<Event> inlinePthreadCondWait(FunctionCall call) {
         final Register errorRegister = getResultRegisterAndCheckArguments(2, call);
         //final Expression condAddress = call.getArguments().get(0);
         final Expression lockAddress = call.getArguments().get(1);
-        // TODO: implement this without lock/unlock events and get rid of them
-        return List.of(
+        final IntegerType type = getPthreadMutexType();
+        final Register oldValueRegister = call.getFunction().newUniqueRegister("__pthread_cond_wait", type);
+        final Register successRegister = call.getFunction().newUniqueRegister("__pthread_cond_wait", types.getBooleanType());
+        return eventSequence(
                 // Allow other threads to access the condition variable.
-                EventFactory.Pthread.newUnlock(lockAddress.toString(), lockAddress),
+                newPthreadUnlock(oldValueRegister, lockAddress),
                 // This thread would sleep here.  Explicit or spurious signals may wake it.
                 // Re-lock.
-                EventFactory.Pthread.newLock(lockAddress.toString(), lockAddress),
+                newPthreadLock(oldValueRegister, successRegister, lockAddress),
                 assignSuccess(errorRegister)
         );
     }
@@ -677,12 +679,15 @@ private List<Event> inlinePthreadCondTimedwait(FunctionCall call) {
         //final Expression condAddress = call.getArguments().get(0);
         final Expression lockAddress = call.getArguments().get(1);
         //final Expression timespec = call.getArguments().get(2);
-        return List.of(
+        final IntegerType type = getPthreadMutexType();
+        final Register oldValueRegister = call.getFunction().newUniqueRegister("__pthread_cond_timedwait", type);
+        final Register successRegister = call.getFunction().newUniqueRegister("__pthread_cond_timedwait", types.getBooleanType());
+        return eventSequence(
                 // Allow other threads to access the condition variable.
-                EventFactory.Pthread.newUnlock(lockAddress.toString(), lockAddress),
+                newPthreadUnlock(oldValueRegister, lockAddress),
                 // This thread would sleep here.  Explicit or spurious signals may wake it.
                 // Re-lock.
-                EventFactory.Pthread.newLock(lockAddress.toString(), lockAddress),
+                newPthreadLock(oldValueRegister, successRegister, lockAddress),
                 newLocal(errorRegister, expressions.makeValue(PosixErrorCode.ETIMEDOUT.getValue(), errorType))
         );
     }
@@ -758,17 +763,15 @@ private List<Event> inlinePthreadSetSpecific(FunctionCall call) {
     private static final List<String> P_THREAD_MUTEXATTR = List.of(
             "prioceiling",
             "protocol",
-            "type",
-            "policy_np"
+            "type"
     );
 
     private List<Event> inlinePthreadMutexInit(FunctionCall call) {
         //see https://linux.die.net/man/3/pthread_mutex_init
         //TODO use attributes
         final Register errorRegister = getResultRegisterAndCheckArguments(2, call);
         final Expression lockAddress = call.getArguments().get(0);
-        // FIXME: We currently use bv32 in InitLock, Lock and Unlock.
-        final IntegerType type = types.getIntegerType(32);
+        final IntegerType type = getPthreadMutexType();
         final Expression unlocked = expressions.makeZero(type);
         return List.of(
                 EventFactory.Llvm.newStore(lockAddress, unlocked, Tag.C11.MO_RELEASE),
@@ -789,58 +792,39 @@ private List<Event> inlinePthreadMutexLock(FunctionCall call) {
         //see https://linux.die.net/man/3/pthread_mutex_lock
         final Register errorRegister = getResultRegisterAndCheckArguments(1, call);
         checkArgument(errorRegister.getType() instanceof IntegerType, "Wrong return type for \"%s\"", call);
-        // FIXME: We currently use bv32 in InitLock, Lock and Unlock.
-        final IntegerType type = types.getIntegerType(32);
-        final Register oldValueRegister = call.getFunction().newRegister(type);
-        final Register successRegister = call.getFunction().newRegister(types.getBooleanType());
+        final IntegerType type = getPthreadMutexType();
+        final Register oldValueRegister = call.getFunction().newUniqueRegister("__pthread_mutex_lock", type);
+        final Register successRegister = call.getFunction().newUniqueRegister("__pthread_mutex_lock", types.getBooleanType());
         final Expression lockAddress = call.getArguments().get(0);
-        final Expression locked = expressions.makeOne(type);
-        final Expression unlocked = expressions.makeZero(type);
-        final Expression fail = expressions.makeNot(successRegister);
-        final Label spinLoopHead = EventFactory.newLabel("__spinloop_head");
-        final Label spinLoopEnd = EventFactory.newLabel("__spinloop_end");
-        // We implement this as a caslocks
-        return List.of(
-                spinLoopHead,
-                EventFactory.Llvm.newCompareExchange(oldValueRegister, successRegister, lockAddress, unlocked, locked, Tag.C11.MO_ACQUIRE, true),
-                EventFactory.newJump(successRegister, spinLoopEnd),
-                EventFactory.newGoto(spinLoopHead),
-                spinLoopEnd,
-                EventFactory.newLocal(errorRegister, expressions.makeCast(fail, errorRegister.getType()))
+        return eventSequence(
+                newPthreadLock(oldValueRegister, successRegister, lockAddress),
+                assignSuccess(errorRegister)
         );
     }
 
     private List<Event> inlinePthreadMutexTryLock(FunctionCall call) {
         //see https://linux.die.net/man/3/pthread_mutex_trylock
         final Register errorRegister = getResultRegisterAndCheckArguments(1, call);
         checkArgument(errorRegister.getType() instanceof IntegerType, "Wrong return type for \"%s\"", call);
-        // FIXME: We currently use bv32 in InitLock, Lock and Unlock.
-        final IntegerType type = types.getIntegerType(32);
-        final Register oldValueRegister = call.getFunction().newRegister(type);
-        final Register successRegister = call.getFunction().newRegister(types.getBooleanType());
+        final IntegerType type = getPthreadMutexType();
+        final Register oldValueRegister = call.getFunction().newUniqueRegister("__pthread_mutex_try_lock", type);
+        final Register successRegister = call.getFunction().newUniqueRegister("__pthread_mutex_try_lock", types.getBooleanType());
         final Expression lockAddress = call.getArguments().get(0);
-        final Expression locked = expressions.makeOne(type);
-        final Expression unlocked = expressions.makeZero(type);
         final Expression fail = expressions.makeNot(successRegister);
         return List.of(
-                EventFactory.Llvm.newCompareExchange(oldValueRegister, successRegister, lockAddress, unlocked, locked, Tag.C11.MO_ACQUIRE),
+                newPthreadTryLock(oldValueRegister, successRegister, lockAddress, false),
                 EventFactory.newLocal(errorRegister, expressions.makeCast(fail, errorRegister.getType()))
         );
     }
 
     private List<Event> inlinePthreadMutexUnlock(FunctionCall call) {
         //see https://linux.die.net/man/3/pthread_mutex_unlock
         final Register errorRegister = getResultRegisterAndCheckArguments(1, call);
-        // FIXME: We currently use bv32 in InitLock, Lock and Unlock.
-        final IntegerType type = types.getIntegerType(32);
-        final Register oldValueRegister = call.getFunction().newRegister(type);
+        final IntegerType type = getPthreadMutexType();
+        final Register oldValueRegister = call.getFunction().newUniqueRegister("__pthread_mutex_unlock", type);
         final Expression lockAddress = call.getArguments().get(0);
-        final Expression locked = expressions.makeOne(type);
-        final Expression unlocked = expressions.makeZero(type);
         return eventSequence(
-                EventFactory.Llvm.newLoad(oldValueRegister, lockAddress, Tag.C11.MO_RELAXED),
-                notToInline.contains(AssertionType.USER) ? null : EventFactory.newAssert(expressions.makeEQ(oldValueRegister, locked), "Unlocking an already unlocked mutex"),
-                EventFactory.Llvm.newStore(lockAddress, unlocked, Tag.C11.MO_RELEASE),
+                newPthreadUnlock(oldValueRegister, lockAddress),
                 assignSuccess(errorRegister)
         );
     }
@@ -869,6 +853,39 @@ private List<Event> inlinePthreadMutexAttr(FunctionCall call) {
         );
     }
 
+    private List<Event> newPthreadUnlock(Register oldValueRegister, Expression address) {
+        final Expression unlocked = expressions.makeGeneralZero(oldValueRegister.getType());
+        final boolean skipCheck = notToInline.contains(AssertionType.USER);
+        final Event load = skipCheck ? null : EventFactory.Llvm.newLoad(oldValueRegister, address, Tag.C11.MO_RELAXED);
+        final Expression isLocked = skipCheck ? null : expressions.makeNEQ(oldValueRegister, unlocked);
+        final Event check = skipCheck ? null : EventFactory.newAssert(isLocked, "Unlocking an already unlocked mutex");
+        final Event store = EventFactory.Llvm.newStore(address, unlocked, Tag.C11.MO_RELEASE);
+        return Arrays.asList(load, check, store);
+    }
+
+    private Event newPthreadTryLock(Register oldValueRegister, Register successRegister, Expression address, boolean strong) {
+        final Expression unlocked = expressions.makeGeneralZero(oldValueRegister.getType());
+        final Expression locked = expressions.makeOne((IntegerType) oldValueRegister.getType());
+        return EventFactory.Llvm.newCompareExchange(oldValueRegister, successRegister, address, unlocked, locked, Tag.C11.MO_ACQUIRE, strong);
+    }
+
+    private List<Event> newPthreadLock(Register oldValueRegister, Register successRegister, Expression address) {
+        // We implement this as a CAS-spinlock
+        final Label spinLoopHead = EventFactory.newLabel("__spinloop_head");
+        final Label spinLoopEnd = EventFactory.newLabel("__spinloop_end");
+        return List.of(
+                spinLoopHead,
+                newPthreadTryLock(oldValueRegister, successRegister, address, true),
+                EventFactory.newJump(successRegister, spinLoopEnd),
+                EventFactory.newGoto(spinLoopHead),
+                spinLoopEnd
+        );
+    }
+
+    private IntegerType getPthreadMutexType() {
+        return types.getIntegerType(1);
+    }
+
     private static final List<String> P_THREAD_RWLOCK_ATTR = List.of(
             "pshared"
     );