Add Intrinsics pthread_detach (#905)

Author: xeren

benchmarks/miscellaneous/pthread.c

@@ -38,9 +38,7 @@ void* thread_join(pthread_t id)
 //define PTHREAD_PRIO_NONE 0
 //define PTHREAD_PRIO_INHERIT 1
 //define PTHREAD_PRIO_PROTECT 2
-//define PTHREAD_MUTEX_POLICY_FAIRSHARE_NP 1
-//define PTHREAD_MUTEX_POLICY_FIRSTFIT_NP 3
-void mutex_init(pthread_mutex_t* lock, int type, int protocol, int policy, int prioceiling)
+void mutex_init(pthread_mutex_t* lock, int type, int protocol, int prioceiling)
 {
     int status;
     int value;
@@ -58,11 +56,6 @@ void mutex_init(pthread_mutex_t* lock, int type, int protocol, int policy, int p
     status = pthread_mutexattr_getprotocol(&attributes, &value);
     assert(status == 0);// && value == protocol);
 
-    status = pthread_mutexattr_setpolicy_np(&attributes, policy);
-    assert(status == 0);
-    status = pthread_mutexattr_getpolicy_np(&attributes, &value);
-    assert(status == 0);// && value == policy);
-
     status = pthread_mutexattr_setprioceiling(&attributes, prioceiling);
     assert(status == 0);
     status = pthread_mutexattr_getprioceiling(&attributes, &value);
@@ -104,8 +97,8 @@ void mutex_test()
     pthread_mutex_t mutex0;
     pthread_mutex_t mutex1;
     //TODO Add different behavior based on attributes.
-    mutex_init(&mutex0, PTHREAD_MUTEX_ERRORCHECK, PTHREAD_PRIO_INHERIT, PTHREAD_MUTEX_POLICY_FAIRSHARE_NP, 1);
-    mutex_init(&mutex1, PTHREAD_MUTEX_RECURSIVE, PTHREAD_PRIO_PROTECT, PTHREAD_MUTEX_POLICY_FIRSTFIT_NP, 2);
+    mutex_init(&mutex0, PTHREAD_MUTEX_ERRORCHECK, PTHREAD_PRIO_INHERIT, 1);
+    mutex_init(&mutex1, PTHREAD_MUTEX_RECURSIVE, PTHREAD_PRIO_PROTECT, 2);
 
     {
         mutex_lock(&mutex0);
@@ -229,7 +222,7 @@ void* cond_worker(void* message)
 void cond_test()
 {
     void* message = (void*) 42;
-    mutex_init(&cond_mutex, PTHREAD_MUTEX_NORMAL, PTHREAD_PRIO_NONE, PTHREAD_MUTEX_POLICY_FIRSTFIT_NP, 0);
+    mutex_init(&cond_mutex, PTHREAD_MUTEX_NORMAL, PTHREAD_PRIO_NONE, 0);
     cond_init(&cond);
 
     pthread_t worker = thread_create(cond_worker, message);
@@ -412,10 +405,59 @@ void key_test()
     //assert(pthread_equal(latest_thread, worker));//TODO add support for destructors
 }
 
+// -------- detaching threads
+
+void* detach_test_worker0(void* ignore)
+{
+    return NULL;
+}
+
+void* detach_test_detach(void* ignore)
+{
+    int status;
+    pthread_t w0 = thread_create(detach_test_worker0, NULL);
+    status = pthread_detach(w0);
+    assert(status == 0);
+
+    status = pthread_join(w0, NULL);
+    assert(status != 0);
+    return NULL;
+}
+
+void* detach_test_attr(void* ignore)
+{
+    int status;
+    int detachstate;
+    pthread_t w0;
+    pthread_attr_t w0_attr;
+    status = pthread_attr_init(&w0_attr);
+    assert(status == 0);
+    status = pthread_attr_getdetachstate(&w0_attr, &detachstate);
+    assert(status == 0 && detachstate == PTHREAD_CREATE_JOINABLE);
+    status = pthread_attr_setdetachstate(&w0_attr, PTHREAD_CREATE_DETACHED);
+    assert(status == 0);
+    status = pthread_attr_getdetachstate(&w0_attr, &detachstate);
+    assert(status == 0 && detachstate == PTHREAD_CREATE_DETACHED);
+    status = pthread_create(&w0, &w0_attr, detach_test_worker0, NULL);
+    assert(status == 0);
+    pthread_attr_destroy(&w0_attr);
+
+    status = pthread_join(w0, NULL);
+    assert(status != 0);
+    return NULL;
+}
+
+void detach_test()
+{
+    thread_create(detach_test_detach, NULL);
+    thread_create(detach_test_attr, NULL);
+}
+
 int main()
 {
     mutex_test();
     cond_test();
     rwlock_test();
     key_test();
+    detach_test();
 }

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

@@ -37,6 +37,7 @@
 import com.dat3m.dartagnan.program.event.functions.VoidFunctionCall;
 import com.dat3m.dartagnan.program.event.lang.catomic.*;
 import com.dat3m.dartagnan.program.event.lang.dat3m.DynamicThreadCreate;
+import com.dat3m.dartagnan.program.event.lang.dat3m.DynamicThreadDetach;
 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.*;
@@ -333,6 +334,10 @@ public static DynamicThreadJoin newDynamicThreadJoin(Register resultRegister, Ex
         return new DynamicThreadJoin(resultRegister, tidExpr);
     }
 
+    public static DynamicThreadDetach newDynamicThreadDetach(Register statusReg, Expression tidExpr) {
+        return new DynamicThreadDetach(statusReg, tidExpr);
+    }
+
     public static ThreadCreate newThreadCreate(List<Expression> arguments) {
         return new ThreadCreate(arguments);
     }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/dat3m/DynamicThreadDetach.java

@@ -0,0 +1,63 @@
+package com.dat3m.dartagnan.program.event.lang.dat3m;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.ExpressionVisitor;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.AbstractEvent;
+import com.dat3m.dartagnan.program.event.Event;
+import com.dat3m.dartagnan.program.event.RegReader;
+import com.dat3m.dartagnan.program.event.RegWriter;
+
+import java.util.HashSet;
+import java.util.Set;
+
+public final class DynamicThreadDetach extends AbstractEvent implements RegWriter, RegReader {
+
+    private Register status;
+    private Expression tid;
+
+    public DynamicThreadDetach(Register statusRegister, Expression tidExpression) {
+        this.status = statusRegister;
+        this.tid = tidExpression;
+    }
+
+    private DynamicThreadDetach(DynamicThreadDetach copy) {
+        super(copy);
+        this.status = copy.status;
+        this.tid = copy.tid;
+    }
+
+    public Expression getTid() {
+        return tid;
+    }
+
+    @Override
+    protected String defaultString() {
+        return String.format("%s <- DynamicThreadDetach(%s)", status, tid);
+    }
+
+    @Override
+    public Event getCopy() {
+        return new DynamicThreadDetach(this);
+    }
+
+    @Override
+    public Register getResultRegister() {
+        return status;
+    }
+
+    @Override
+    public void setResultRegister(Register reg) {
+        status = reg;
+    }
+
+    @Override
+    public Set<Register.Read> getRegisterReads() {
+        return Register.collectRegisterReads(tid, Register.UsageType.OTHER, new HashSet<>());
+    }
+
+    @Override
+    public void transformExpressions(ExpressionVisitor<? extends Expression> exprTransformer) {
+        tid = tid.accept(exprTransformer);
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/dat3m/DynamicThreadJoin.java

@@ -29,10 +29,11 @@ The status register shall be large enough to accommodate all error values (bv8 s
 public class DynamicThreadJoin extends AbstractEvent implements RegWriter, RegReader, BlockingEvent {
 
     public enum Status {
-        SUCCESS(0),                // The join was successful
-        INVALID_TID(1),            // The provided tid does not match with a joinable thread
-        INVALID_RETURN_TYPE(2);    // The provided tid is valid, but the return type of that thread does not match
+        SUCCESS(0),                // The join was successful.
+        INVALID_TID(1),            // The provided tid does not match with any of the spawned threads.
+        INVALID_RETURN_TYPE(2),    // The provided tid is valid, but the return type of that thread does not match
                                              // with the expected return type.
+        DETACHED_THREAD(3);        // The provided tid belongs to a non-joinable thread.
 
         final int errorCode;
         public int getErrorCode() { return errorCode; }

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/AssignmentInlining.java

@@ -78,6 +78,7 @@ public Expression visitRegister(Register reg) {
                         // A usage counter may be missing for assignments of the form "r = f(r)"
                         // which do not allow for substituting r for f(r) in later usages.
                         usageCounter.containsKey(lastAssignment)
+                        && preDominatorTree.contains(curEvent)
                         && preDominatorTree.isDominatedBy(curEvent, lastAssignment)
                         && !curEvent.hasTag(Tag.NOOPT)
                         // Inline if the expression is only used once or if it leads to simplifications.