-
Notifications
You must be signed in to change notification settings - Fork 29
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Thread cf & must edges #494
Conversation
Updated control-flow encoding to connect control-flow of ThreadStart with ThreadCreate if possible.
…uivalence. - Updated BranchEquivalence to correctly merge branches of threads that have a creator. Also removed functions related to reachability queries. - Updated ThreadCreation's thread-synchronization code. Also added a missing store for thread ids.
Fixed LogThreadStatistics's detection of init threads (which now have an extra event).
… detection and eliminate redundant casts.
- Needs updating of its documentation - Now always merges branches (cannot be disabled) - Propagation of mutual exclusive branch classes can be improved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
Show resolved
Hide resolved
public ThreadStart(ThreadCreate creator) { | ||
this.creator = creator; | ||
|
||
mayFailSpuriously = (creator != null); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
what happens if I use the CLI option to force thread creation? If that is the case do we call setMayFailSpuriously()
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, ThreadCreation
will spawn threads and set the option based on whether thread creation is forced to succeed.
At some point, I will probably get rid of this flag again and instead let ThreadCreation
generate a non-deterministic choice between success and failure like so:
// compiling "int success = pthread_create(&t, NULL; worker, arg);" to
if (*) {
ThreadCreate(worker, arg);
store (&t, TID);
success = 1;
} else {
// store (&t, -1);
success = 0;
}
Then ThreadCreate/ThreadStart
can always be assumed to succeed if executed.
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java
Show resolved
Hide resolved
LGTM |
* Function passes & Thread creation after unrolling #492 * Thread cf & must edges #494 * Dynamic Pthread join #496 --------- Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Thomas Haas <[email protected]> Co-authored-by: René Pascal Maseli <[email protected]>
This PR adds proper control-flow dependencies between spawned threads and their spawners/creators.
ThreadStart
event that may have aThreadCreate
event as acreator
. Ifcreator == null
, the thread is executed unconditionally (e.g, themain
thread, init threads, and all threads in litmus tests).ThreadStart
only if its associatedcreator
(if any) gets executed.BranchEquivalence
has been reworked to respect this new control-flow and consider the control-flow relationship between a thread and its creator.Minor side changes:
AbortIf (true)
for dead code detectioni64
toi64
casts).Thread.getEntry
andThread.getExit
now returnThreadStart
resp.Label
.