pthread library intrinsics #582

xeren · 2023-12-01T21:36:14Z

Adds intrinsics for several library functions required for SVCOMP 2024. This includes condition variables, rwlocks and specifics (thread-local storage). Also alters the behavior of pthread mutex intrinsics.

* Ignore inline assembly, but generate nondeterministic return values * Add intrinsics for void* calloc(size_t,size_t), int pthread_mutex_trylock(void*) * Add intrinsics for pthread_cond* * Add empty intrinsics for pthread_mutexattr* * Add intrinsics for pthread_rwlock* * Add intrinsics for strcpy * Intrinsics error message now contains all missing intrinsics * Add intrinsics pthread_getspecific * Add pthread_setspecific * Add pthread_key_create * Add pthread_key_destroy --------- Co-authored-by: René Pascal Maseli <[email protected]>

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

hernanponcedeleon · 2023-12-02T09:39:21Z

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

+        P_THREAD_MUTEXATTR_SET(List.of(
+                "pthread_mutexattr_setprioceiling",
+                "pthread_mutexattr_setprotocol",
+                "pthread_mutexattr_settype",
+                "pthread_mutexattr_setpolicy_np"),
+                true, false, true, true, Intrinsics::inlineAsZero),
+        P_THREAD_MUTEXATTR_GET(List.of(
+                "pthread_mutexattr_getprioceiling",
+                "pthread_mutexattr_getprotocol",
+                "pthread_mutexattr_gettype",
+                "pthread_mutexattr_getpolicy_np"),
+                false, true, true, true, Intrinsics::inlineAsZero),


how faithful are these implementation?

hernanponcedeleon · 2023-12-02T09:39:51Z

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

+        P_THREAD_RWLOCKATTR_SET("pthread_rwlockattr_setpshared", true, false, true, true, Intrinsics::inlineAsZero),
+        P_THREAD_RWLOCKATTR_GET("pthread_rwlockattr_getpshared", true, false, true, true, Intrinsics::inlineAsZero),


how faithful are these implementation?

The implementations fail e.g. this simple test, which should pass on full support:

void test() { int pshared; pthread_rwlockattr_t attr; pthread_rwlockattr_init(&attr); pthread_rwlockattr_setpshared(&attr, PTHREAD_PROCESS_PRIVATE); pthread_rwlockattr_getpshared(&attr, &pshared); assert(pshared == PTHREAD_PROCESS_PRIVATE); }

I don't expect these structures to be used like that in errors we are interested in right now.

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

hernanponcedeleon · 2023-12-02T09:42:31Z

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

+        final Register result = checkValueAndArguments(2, call);
+        final Expression address = call.getArguments().get(0);
+        //final Expression attributes = call.getArguments().get(1);
+        final Expression initializedState = expressions.makeZero(types.getArchType());


is the state of a conditional variable always initialize to zero?

The value was intended to correspond with the number of threads that can be awakened. It does not take spurious wake-ups into account, though. Also, it cannot recognize if the pthread_cond_init is missing. It should rather be 1, pthread_cond_destroy should store 0, and the remaining functions should check this.

hernanponcedeleon · 2023-12-02T09:52:45Z

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

+        return List.of(
+                EventFactory.newLocal(result, expressions.makeGeneralZero(result.getType())));
+    }


I don't fully understand these local storage methods, but since the create access global memory, I looks suspicious the delete does not clean/free/... those

The implementation could treat zero as values of uninitialized objects, instead. Then, destructors can just check non-zero, then store zero. This could be done for the entire pthread library.

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

hernanponcedeleon · 2023-12-02T09:55:46Z

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

+    private List<Event> inlinePthreadMutexTryLock(FunctionCall call) {
+        final Register register = checkValueAndArguments(1, call);
+        checkArgument(register.getType() instanceof IntegerType, "Wrong return type for \"%s\"", call);
+        final var error = new INonDet(constantId++, (IntegerType) register.getType(), true);


Does this mean this method can fail even if the mutex is free?

Yes, this is a bug. I did not want to insert a CAS here, since I did not know if it would have interfered with Lock and Unlock. Instead I could add a new TryLock class or replace the existing lock events with atomics.

Btw. I think if we have like 80% of the pthread library implemented via C11 atomics, we can also go all the way and do so for the standard lock, unlock, and init, that are currently handled by special events.
We are unlikely to do verification w.r.t. to the full C11 model in the near future and that is the only model that talks about these locks as special events. It is also unlikely that the standard implementation via acquire/release deviates much from the ordering implied by the C11 model (so we are unlikely to miss bugs with a concrete implementation).
Lastly, even if we decide to do full C11, we have to introduce a lot of new events anyhow, so adding back in the three we kicked out is not going to be a big deal.

hernanponcedeleon · 2023-12-02T09:58:14Z

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

+        final Register dummy = call.getFunction().newRegister(types.getArchType());
+        final Expression zero = expressions.makeZero(types.getArchType());
+        final Expression one = expressions.makeOne(types.getArchType());
+        final var replacement = new INonDet(constantId++, types.getArchType(), true);


Does this mean the method can spuriously fail, or together with the assume, this gives correct semantics?

This should have given correct semantics. I have replaced it with a CAS now, as suggested by @ThomasHaas.

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

hernanponcedeleon · 2023-12-02T10:30:20Z

These errors suggests problems with some of the intrinsics

./Dartagnan-SVCOMP.sh ../../sv-benchmarks/c/properties/no-overflow.prp ../../sv-benchmarks/c/pthread-divine/tls_basic.i


--------------------------------------------------------------------------------


20:34:09 [INFO ] GitInfo.CreateGitInfo - Git branch: svcomp-2024
20:34:09 [INFO ] GitInfo.CreateGitInfo - Git commit ID: 17eeec33cbc9c310519b08551b317469f878ce8c
20:34:09 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES: false
20:34:09 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_SYMMETRIC_LEARNING: FULL
20:34:09 [INFO ] Dartagnan.main - Program path: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_116fd34f-aaef-4ba0-8813-e386ac403cf8/bin/dartagnan-verify-smqyFgON4Q/output/tls_basic-opt.ll
20:34:09 [INFO ] Dartagnan.main - CAT file path: cat/svcomp.cat
20:34:09 [INFO ] Wmm.configureAll - encoding.wmm.reduceAcyclicityEncodeSets: true
20:34:09 [INFO ] LoopFormVerification.run - Detected 0 loops in the program.
20:34:09 [INFO ] Compilation.run - Program compiled to C11
20:34:09 [INFO ] LoopUnrolling.run - Program unrolled 1 times
20:34:09 [INFO ] DynamicPureLoopCutting.run - Found 0 static spin loops and 0 potential spin loops.
20:34:09 [INFO ] ThreadCreation.run - Number of threads (including main): 2
20:34:09 [ERROR] Dartagnan.main - The types of bv32 r7 and bv64(0) do not match.
java.lang.IllegalArgumentException: The types of bv32 r7 and bv64(0) do not match.
	at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445) ~[guava-32.1.2-jre.jar:?]
	at com.dat3m.dartagnan.expression.IExprBin.<init>(IExprBin.java:20) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.expression.ExpressionFactory.makeBinary(ExpressionFactory.java:220) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.expression.ExpressionFactory.makeADD(ExpressionFactory.java:174) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlinePthreadGetSpecific(Intrinsics.java:514) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.replace(Intrinsics.java:306) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlineLate(Intrinsics.java:1051) ~[dartagnan.jar:?]
	at java.util.ArrayList.forEach(ArrayList.java:1511) ~[?:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlineLate(Intrinsics.java:1041) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.ProcessingManager.lambda$run$0(ProcessingManager.java:142) ~[dartagnan.jar:?]
	at java.util.ArrayList.forEach(ArrayList.java:1511) ~[?:?]
	at com.dat3m.dartagnan.program.processing.ProcessingManager.run(ProcessingManager.java:142) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.ModelChecker.preprocessProgram(ModelChecker.java:71) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.AssumeSolver.run(AssumeSolver.java:46) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.AssumeSolver.run(AssumeSolver.java:36) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:170) [dartagnan.jar:?]
ERROR

./Dartagnan-SVCOMP.sh ../../sv-benchmarks/c/properties/no-overflow.prp ../../sv-benchmarks/c/pthread-divine/tls_destructor_worker.i


--------------------------------------------------------------------------------


20:34:09 [INFO ] GitInfo.CreateGitInfo - Git branch: svcomp-2024
20:34:09 [INFO ] GitInfo.CreateGitInfo - Git commit ID: 17eeec33cbc9c310519b08551b317469f878ce8c
20:34:09 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES: false
20:34:09 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_SYMMETRIC_LEARNING: FULL
20:34:09 [INFO ] Dartagnan.main - Program path: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e861b918-2072-44d4-b99b-c7580ad6f64a/bin/dartagnan-verify-smqyFgON4Q/output/tls_destructor_worker-opt.ll
20:34:09 [INFO ] Dartagnan.main - CAT file path: cat/svcomp.cat
20:34:09 [INFO ] Wmm.configureAll - encoding.wmm.reduceAcyclicityEncodeSets: true
20:34:09 [INFO ] LoopFormVerification.run - Detected 0 loops in the program.
20:34:09 [INFO ] Compilation.run - Program compiled to C11
20:34:09 [INFO ] LoopUnrolling.run - Program unrolled 1 times
20:34:09 [INFO ] DynamicPureLoopCutting.run - Found 0 static spin loops and 0 potential spin loops.
20:34:09 [INFO ] ThreadCreation.run - Number of threads (including main): 2
20:34:09 [ERROR] Dartagnan.main - The types of bv32 r9 and bv64(0) do not match.
java.lang.IllegalArgumentException: The types of bv32 r9 and bv64(0) do not match.
	at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445) ~[guava-32.1.2-jre.jar:?]
	at com.dat3m.dartagnan.expression.IExprBin.<init>(IExprBin.java:20) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.expression.ExpressionFactory.makeBinary(ExpressionFactory.java:220) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.expression.ExpressionFactory.makeADD(ExpressionFactory.java:174) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlinePthreadSetSpecific(Intrinsics.java:525) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.replace(Intrinsics.java:306) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlineLate(Intrinsics.java:1051) ~[dartagnan.jar:?]
	at java.util.ArrayList.forEach(ArrayList.java:1511) ~[?:?]
	at com.dat3m.dartagnan.program.processing.Intrinsics.inlineLate(Intrinsics.java:1041) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.ProcessingManager.lambda$run$0(ProcessingManager.java:142) ~[dartagnan.jar:?]
	at java.util.ArrayList.forEach(ArrayList.java:1511) ~[?:?]
	at com.dat3m.dartagnan.program.processing.ProcessingManager.run(ProcessingManager.java:142) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.ModelChecker.preprocessProgram(ModelChecker.java:71) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.AssumeSolver.run(AssumeSolver.java:46) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.AssumeSolver.run(AssumeSolver.java:36) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:170) [dartagnan.jar:?]
ERROR

Fix pthread_cond_wait and pthread_cond_timedwait aborting if a broadcast guessed the right amount of threads to awake

hernanponcedeleon · 2023-12-05T21:21:36Z

The two benchmarks from above now fail due to this problem

java.lang.IllegalStateException: null
        at com.google.common.base.Preconditions.checkState(Preconditions.java:496) ~[guava-32.1.2-jre.jar:?]
        at com.dat3m.dartagnan.program.memory.MemoryObject.getStaticallyInitializedFields(MemoryObject.java:58) ~[dartagnan.jar:?]
        at com.dat3m.dartagnan.program.processing.RemoveUnusedMemory.run(RemoveUnusedMemory.java:28) ~[dartagnan.jar:?]
        at com.dat3m.dartagnan.program.processing.ProcessingManager.lambda$run$0(ProcessingManager.java:142) ~[dartagnan.jar:?]
        at java.util.ArrayList.forEach(ArrayList.java:1511) ~[?:?]
        at com.dat3m.dartagnan.program.processing.ProcessingManager.run(ProcessingManager.java:142) ~[dartagnan.jar:?]
        at com.dat3m.dartagnan.verification.solving.ModelChecker.preprocessProgram(ModelChecker.java:71) ~[dartagnan.jar:?]
        at com.dat3m.dartagnan.verification.solving.AssumeSolver.run(AssumeSolver.java:46) ~[dartagnan.jar:?]
        at com.dat3m.dartagnan.verification.solving.AssumeSolver.run(AssumeSolver.java:36) ~[dartagnan.jar:?]
        at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:170) [dartagnan.jar:?]
ERROR

…cessing pipeline

hernanponcedeleon · 2023-12-06T14:54:01Z

The exceptions are gone now, but we return the wrong result for tls_destructor_worker.c.

The task is supposed to be unsafe, but I don't understand the comment explaining why this is the case.

ThomasHaas · 2023-12-06T17:15:27Z

The task is unsafe, because the worker thread sets val[key] = 42 but the destructor checks for val[key] != 42.
I think the destructor feature of pthread_create_key is not implemented yet, so that is why we return PASS.

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

ThomasHaas · 2023-12-08T10:31:23Z

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

+    private List<Event> inlinePthreadCondSignal(FunctionCall call) {
+        //see https://linux.die.net/man/3/pthread_cond_signal
+        // Because of spurious wake-ups, there is no need to do anything here.
+        final Register errorRegister = getResultRegisterAndCheckArguments(1, call);
+        //final Expression condAddress = call.getArguments().get(0);
+        return List.of(
+                assignSuccess(errorRegister)
+        );


We could still check that condAddress is initialized and return EINVAL if not. I think we should have a TODO/FIXME for that. or we put a more general FIXME somewhere that says that we assume most/all pthread intrinsics to return success.

The problem is platform-independence: The values of error codes are platform-dependent and not exposed as-is in the LLVM IR. We would need something like int __VERIFIER_EINVAL() {return EINVAL;} in the input program. I will add a TODO.

I see. That makes error code handling annoying.

What about assuming by default they success and having an option to allow failure. If the option is set, we just return a non-det value (we might need to restrict the range)

It's not that much a matter of allowing failure, but that of returning correct values. For cond_signal we can precisely determine when it should succeed and when it should fail, it's just that we do not know what error code to return (it should be EINVAL, but we don't know its value).
We could opt to just always return a non-deterministic, non-zero value as error. No need to have an option for that.

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

ThomasHaas · 2023-12-08T11:35:33Z

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

+                // Try to lock
+                EventFactory.Atomic.newExchange(dummy, lockAddress, replacement, Tag.C11.MO_ACQUIRE),
+                // Store one (write-locked) only if successful, else leave unchanged
+                EventFactory.newAssume(expressions.makeEQ(replacement, properReplacement)),
+                // Deadlock if violation occurs in another thread
+                EventFactory.newAbortIf(locked),
+                assignSuccess(errorRegister)


Wouldn't a CAS-based solution work without any magic? CAS(&lock, 0, 1) will succeed only if the lock is free. In a loop, it will do the correct thing (and deadlock detection will also work). Without the loop, you get the TryWrlock implementation without spurious failures.

Yes, this should work.

ThomasHaas · 2023-12-08T11:53:39Z

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

+                // Increment shared counter only if not locked by writer.
+                EventFactory.Atomic.newFADD(dummy, lockAddress, increment, Tag.C11.MO_ACQUIRE),
+                // Deadlock if a violation occurred in another thread.  In this case, lock value was not changed
+                EventFactory.newAbortIf(expressions.makeEQ(increment, unlocked)),
+                // On success, lock cannot have been write-locked.
+                EventFactory.newAssume(expressions.makeNEQ(dummy, wrLocked)),
+                // On success, incremented by two, if first reader, else one.
+                EventFactory.newAssume(expressions.makeEQ(increment, properIncrement)),
+                assignSuccess(errorRegister)


I'm wondering if a CAS-based solution works here as well and circumvents the spurious store that happens if the locking fails.

expected = non_det(); desired = expected + 2; (oldValue, success) = CAS(&lock, expected, desired) if (oldValue != WrLocked) { assume (success); // CAS succeeds if oldValue was fine. Implies that the guessed expected value matched oldValue. } else { assume (!success); // CAS must fail. } // Could be simplified to assume(ITE(oldValue != WrLocked, success, !success));

Putting this into a loop will give you proper deadlock handling as well.

I agree. You can even simplify it to assume(expected != WrLocked);.

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

Fix type mismatch in pthread_mutex_trylock. Switch implementations of pthread_cond_signal and pthread_cond_broadcast.

Outlined several rwlock-related code.

ThomasHaas · 2023-12-14T10:22:38Z

The exception that is triggered in the CI is because we do not support pthread_create with proper function pointers yet.
Devirtualization runs early and replaces all function pointers by constant (function address) values. This causes pthread_create to observe a constant value instead of a function.
Technically, Devirtualization should treat pthread_create as a virtual call and devirtualize it as well.

ThomasHaas

You should add handling of the nasty "\01" prefix for many pthread calls rather than removing the prefix by hand from the .ll code.
We should be able to run on unmodified .ll code.

[16.12.2023] 11:34:59 [ERROR] Dartagnan.main - Unknown intrinsics 
"\01_pthread_cond_init", "\01_pthread_cond_timedwait", "\01_pthread_cond_wait",
"\01_pthread_mutexattr_destroy", "\01_pthread_rwlock_destroy", 
"\01_pthread_rwlock_init", "\01_pthread_rwlock_rdlock", 
"\01_pthread_rwlock_tryrdlock", "\01_pthread_rwlock_trywrlock", 
"\01_pthread_rwlock_unlock", "\01_pthread_rwlock_wrlock"

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

benchmarks/c/miscellaneous/pthread.c

…brary

hernanponcedeleon · 2023-12-18T18:39:22Z

@xeren can you rebase to see if #591 fixed the CI?

Let's try to get this merged before the weekend so I can finally release version 4.0.0

ThomasHaas · 2023-12-19T09:11:21Z

@xeren can you rebase to see if #591 fixed the CI?

Let's try to get this merged before the weekend so I can finally release version 4.0.0

#591 alone does not fix the CI. As I said in my last post, there is a missing cast and the loop bounds of the test are insufficient (IIRC there are also unannotated loops that need annotatation).

Ignore test for return values of pthread_join Ignore test for destructors of pthread_key_create

hernanponcedeleon · 2023-12-22T09:58:38Z

The exceptions are gone now, but we return the wrong result for tls_destructor_worker.c.

The task is supposed to be unsafe, but I don't understand the comment explaining why this is the case.

We still have this problem

ThomasHaas · 2023-12-22T10:07:08Z

The exceptions are gone now, but we return the wrong result for tls_destructor_worker.c.
The task is supposed to be unsafe, but I don't understand the comment explaining why this is the case.

We still have this problem

This is not a trivial fix because it involves handling of function pointers and instrumenting the exit code of threads.
In other words, this is not something that is doable by pure inlining of the intrinsics.
If you want to have fully correct pthread support in this PR, then you gotta wait until next year :P.

hernanponcedeleon · 2023-12-22T11:07:32Z

I am ok with keeping this as it is (I will open an issue so we don't forget about this one).

@ThomasHaas do you have any further comments about the code or can I merge?

@xeren can you please rebase?

Signed-off-by: Hernan Ponce de Leon <[email protected]>

ThomasHaas · 2023-12-23T11:41:31Z

I am ok with keeping this as it is (I will open an issue so we don't forget about this one).

@ThomasHaas do you have any further comments about the code or can I merge?

I think there are some minor things to fix, but since it is working now, we can merge.

hernanponcedeleon and others added 4 commits December 1, 2023 22:32

Disable strcpy intrinsics

48c9728

pthread_mutex_init initializes unlocked mutexes

5558326

Define return value of pthread_mutex_*

e98d35d

hernanponcedeleon reviewed Dec 2, 2023

View reviewed changes

xeren added 3 commits December 5, 2023 16:30

Refactor and add references

09cb108

Fix pthread_cond_wait and pthread_cond_timedwait aborting if a broadcast guessed the right amount of threads to awake

Add spurious wake-ups to pthread_cond_wait

ee0873d

Add missing load in pthread_getspecific

6938013

Fix pthread_key_create allocating dynamic memory too early in the pro…

fe32a93

…cessing pipeline

ThomasHaas reviewed Dec 6, 2023

View reviewed changes

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java Outdated Show resolved Hide resolved

ThomasHaas reviewed Dec 8, 2023

View reviewed changes

xeren added 10 commits December 11, 2023 17:52

Fix indirection in pthread_getspecific and pthread_setspecific.

1f65e69

Fix type mismatch in pthread_mutex_trylock. Switch implementations of pthread_cond_signal and pthread_cond_broadcast.

Add ExpressionFactory.makeValue(long,IntegerType)

5a7de2f

Fix pthread_rwlock_tryrdlock failing even if read-locked.

c41b522

Outlined several rwlock-related code.

Remove stores from failing pthread_rwlock_try..lock

4517ca4

Refactor Intrinsics, remove strcpy

a09a841

Add pthread_*attr_* intrinsics

cc59176

Add pthread_equal

407dbe5

Add tests

8749470

Remove "\01_" prefix

0b4b8b7

Merge branch 'development' into svcomp-2024-library

9d27083

ThomasHaas reviewed Dec 16, 2023

View reviewed changes

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java Outdated Show resolved Hide resolved

benchmarks/c/miscellaneous/pthread.c Outdated Show resolved Hide resolved

ThomasHaas mentioned this pull request Dec 16, 2023

Devirtualise pthread_create #591

Merged

Merge remote-tracking branch 'origin/development' into svcomp-2024-li…

78724bf

…brary

xeren added 3 commits December 19, 2023 15:07

Fixes

9aabdf9

Add unescaping to VisitorLLVM

260e0eb

Fix pthread_rwlock_rdlock and pthread_rwlock_tryrdlock

3fe3fbd

Ignore test for return values of pthread_join Ignore test for destructors of pthread_key_create

hernan-poncedeleon added 2 commits December 22, 2023 22:31

Merge branch 'development' into svcomp-2024-library

78c801f

Use BV encoding for miscellaneous/pthread test

52fcc92

Signed-off-by: Hernan Ponce de Leon <[email protected]>

hernanponcedeleon merged commit 024bd43 into development Dec 23, 2023
1 check passed

hernanponcedeleon deleted the svcomp-2024-library branch December 23, 2023 12:57

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

pthread library intrinsics #582

pthread library intrinsics #582

xeren commented Dec 1, 2023

hernanponcedeleon Dec 2, 2023

hernanponcedeleon Dec 2, 2023

xeren Dec 11, 2023

hernanponcedeleon Dec 2, 2023

xeren Dec 5, 2023

hernanponcedeleon Dec 2, 2023

xeren Dec 5, 2023

hernanponcedeleon Dec 2, 2023

xeren Dec 4, 2023

ThomasHaas Dec 11, 2023

hernanponcedeleon Dec 2, 2023

xeren Dec 11, 2023

hernanponcedeleon commented Dec 2, 2023 •

edited

Loading

hernanponcedeleon commented Dec 5, 2023

hernanponcedeleon commented Dec 6, 2023

ThomasHaas commented Dec 6, 2023

ThomasHaas Dec 8, 2023 •

edited

Loading

xeren Dec 8, 2023

ThomasHaas Dec 9, 2023

hernanponcedeleon Dec 9, 2023

ThomasHaas Dec 9, 2023

ThomasHaas Dec 8, 2023

xeren Dec 11, 2023

ThomasHaas Dec 8, 2023

xeren Dec 11, 2023

ThomasHaas commented Dec 14, 2023

ThomasHaas left a comment

hernanponcedeleon commented Dec 18, 2023

ThomasHaas commented Dec 19, 2023

hernanponcedeleon commented Dec 22, 2023

ThomasHaas commented Dec 22, 2023

hernanponcedeleon commented Dec 22, 2023

ThomasHaas commented Dec 23, 2023

		P_THREAD_RWLOCKATTR_SET("pthread_rwlockattr_setpshared", true, false, true, true, Intrinsics::inlineAsZero),
		P_THREAD_RWLOCKATTR_GET("pthread_rwlockattr_getpshared", true, false, true, true, Intrinsics::inlineAsZero),

pthread library intrinsics #582

pthread library intrinsics #582

Conversation

xeren commented Dec 1, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hernanponcedeleon commented Dec 2, 2023 • edited Loading

hernanponcedeleon commented Dec 5, 2023

hernanponcedeleon commented Dec 6, 2023

ThomasHaas commented Dec 6, 2023

ThomasHaas Dec 8, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ThomasHaas commented Dec 14, 2023

ThomasHaas left a comment

Choose a reason for hiding this comment

hernanponcedeleon commented Dec 18, 2023

ThomasHaas commented Dec 19, 2023

hernanponcedeleon commented Dec 22, 2023

ThomasHaas commented Dec 22, 2023

hernanponcedeleon commented Dec 22, 2023

ThomasHaas commented Dec 23, 2023

hernanponcedeleon commented Dec 2, 2023 •

edited

Loading

ThomasHaas Dec 8, 2023 •

edited

Loading