Inlining & Threading (rework) #483
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Pthread_create and join are parsed and calls to them are generated as expected outside of inline mode.
Added new Events for passing parameters across threads, and updated ThreadCreation pass to generate them. Updated CoreCodeVerification to recognize new threading-related events. Updated inlining pass to generate annotations around inlined calls.
Updated Alias analysis to recognize new threading-related events Refactor/renaming
Added new thread events to EventFactory Updated ThreadCreation to not generate Pthread events Fixed issue in ExecutionModel with boolean valued memory accesses.
… with the new ThreadCreation pass, but still fail without, so they are disabled for now.
Added new thread_local.c unit test
Better automatic naming for nameless threads.
Adding logging to ThreadCreation
Adding missing StaticMemoryInitializer pass into ProcessingManager
First cleanup pass of Parser code (removing inline mode).
…aused only warnings, but no semantic errors).
dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/LlvmProcedures.java
Outdated
Show resolved
Hide resolved
...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java
Outdated
Show resolved
Hide resolved
...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java
Show resolved
Hide resolved
Added FIXME for recursion handling
|
LGTM |
hernanponcedeleon
added a commit
that referenced
this pull request
Jul 15, 2023
Add proper functions #470 Generic Registers #471 Rmw base classes #475 Type Safety #478 Parsing & thread creation #479 Unit tests for thread creation #481 Move memory initialization, inlining, and thread creation from the parser to processing passes #483 Inlining of nondet_int #485 Various fixes/cleanup #487 --------- Co-authored-by: Thomas Haas <[email protected]> Co-authored-by: René Pascal Maseli <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Moves inlining of boogie code into a new
ProgramProcessor.EDIT by @ThomasHaas :
This PR moves static memory initialization, inlining, and thread creation from the parser into processing passes.
All thse passes run immediatly after parsing, meaning that the overall behaviour should not have changed.
There is a minor improvement in handling of
pthread_joinallowing us to handle slightly more cases.As a side effect, the 4 pthread events
Create,Start,JoinandEndare also gone now.Work to do in future PRs:
LocalIdin addition toGlobalIdInlineIdnow? More generally, we need to look into metadata tracking with our more intricate program processing. I think tracking oforiginalIdis also broken for now.