Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Improved liveness detection for store exclusives #722

Merged
merged 29 commits into from
Sep 3, 2024
Merged

Improved liveness detection for store exclusives #722

merged 29 commits into from
Sep 3, 2024

Conversation

ThomasHaas
Copy link
Collaborator

This PR addresses issue #719 while also refactoring some code related to that.

xeren and others added 29 commits May 27, 2024 21:53
@xeren
Split 'addInto' stats into graph and cycle detection counters (#683)
92d82b1
@ThomasHaas
UI update (#684)
016aaf4 
* Updated witness generation functions to return the generated File.

* Improved UI:
- can select property to check for (only one property at a time)
- can generate and render the violation witness in the UI
- UI can be scaled with 'ctrl' + '+/-'
- Added simple zoom option to displayed witnesses

* Added ability to pass configuration options via the UI.

* UI programs now get a unified name.
Fixed witness generation for programs without names or without file suffix.
@hernanponcedeleon @hernan-poncedeleon
Add support for memcpy_s (#686)
184fab4 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
@ThomasHaas
- Added Event.getLocalId/Event.setLocalId() (#688)
28885e2 
- Function-based analysis and passes now rely on local ids (e.g., for loop detection) for the most part.
- Fixed problems in NormalizeLoops.java
@hernanponcedeleon
Add support for cttz (count trailing zeros) intrinsic (#689)
929b15b 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
@ThomasHaas
Fix addresses in witnesses (#692)
1afd208 
* Added memory layout information to ExecutionModel.

* Fixed ExecutionGraphVisualizer printing odd addresses sometimes.

* Fix address string computation. 

* Added better out-of-bounds tagging.

* Fixed RefinementSolver.analyzeInconclusiveness.
@ThomasHaas
Fix size and offset computations of types (#691)
6c8baa3
@xeren
Fix inclusion updates in IBPA (#694)
94f90c7
@ThomasHaas
Easier handling of nondet choices (#693)
8b8389a
@hernanponcedeleon @hernan-poncedeleon
Fix cttz bug (#696)
2688e01 
* Fix copy paste error

* Add unit tests

---------

Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
@ThomasHaas
Better mem2reg (#697)
075f03f 
* Added RemoveDeadNullChecks pass

* Added TypeFactory.decomposeIntoPrimitives
Improved MemToReg to also work on complex allocations.

* Avoid Mem2Reg on allocations that are used in RMWs.

* Added loop check to avoid unsoundness
@hernanponcedeleon @hernan-poncedeleon
Model locks as spinloops to avoid wrong liveness bugs (#695)
3291aa0 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
@xeren
Assertion expressions (#690)
489f608
@ThomasHaas
Added TagSet, used in AbstractEvent to store tags of events. (#698)
d917401
@hernanponcedeleon @hernan-poncedeleon
Avoid exception in SyntacticContextAnalysis (#699)
fa5a226 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
@hernanponcedeleon @hernan-poncedeleon @ThomasHaas
Add loop bound annotation (#687)
3771432 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Thomas Haas <[email protected]>
@hernanponcedeleon @hernan-poncedeleon
Automatically cancel previous CI when new commits are pushed (#700)
6356656 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
@hernanponcedeleon
Update JavaSMT version (#701)
9f44db5
@DIvanov503
Refactor relation analysis interface (#702)
e87cb88 
Co-authored-by: Dmitry Ivanov <[email protected]>
@DIvanov503
Fix an incorrect term pattern in SyncWith (#706)
eb15f40 
Co-authored-by: Dmitry Ivanov <[email protected]>
@hernanponcedeleon @hernan-poncedeleon @ThomasHaas
Extend loop normalization (#705)
6582d4a 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Thomas Haas <[email protected]>
@natgavrilenko @hernan-poncedeleon
@tonghaining @ThomasHaas
Spir-V frontend (#703)
030b16b 
Co-authored-by: Natalia Gavrilenko <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: haining <[email protected]>
Co-authored-by: Thomas Haas <[email protected]>
@natgavrilenko
Add memory effects to LLVM grammar and better error message (#710)
cdc0689 
Co-authored-by: Natalia Gavrilenko <[email protected]>
@natgavrilenko
Fix printer OutOfBoundsException (#713)
618c3f7 
Co-authored-by: Natalia Gavrilenko <[email protected]>
@DIvanov503
Compute missing tuples in transitive closure (#718)
f6d10e2 
Co-authored-by: Dmitry Ivanov <[email protected]>
@ThomasHaas
Merge branch 'refs/heads/development' into spinloop_excl_store
a81b5fd
@ThomasHaas
Improved DynamicSpinLoopDetection to handle RMWStoreExclusive correctly
053afd6
@ThomasHaas
Refactored PropertyEncoder.LivenessEncoder and added fairness conditi…
dc34e7e 
…ons for RMWStoreExclusive when checking for liveness issues
@ThomasHaas
Split Tag.EARLYTERMINATION into EXCEPTITONAL_TERMINATION and NONTERMI…
b682775 
…NATION
@ThomasHaas
Copy link
Collaborator Author

Does anybody know why commits from over 3 months ago are shown in this PR?

@ThomasHaas ThomasHaas mentioned this pull request Aug 30, 2024
Closed
@hernanponcedeleon
Copy link
Owner

hernanponcedeleon commented Aug 30, 2024 •
edited
Loading

Probably you created you branch before I forced pushed to development a few days ago (I had the same issue when I opened the smtlib PR, which was based on a local copy of depelopment that was in turns based rebased on top of master that had one extra commit, thus the forced pushed).

The diff just shows what we care about and I'll eventually squash once this is reviewed (I'll check the code once I'm back on Wednesday), so don't worry about the extra commits.

@db7
Copy link

db7 commented Sep 2, 2024

It would be nice to have this branch or arm-asm branch merged, because rebasing one on another always creates conflicts.

@hernanponcedeleon hernanponcedeleon merged commit 6326445 into development Sep 3, 2024
1 check passed
@hernanponcedeleon hernanponcedeleon deleted the improvedLivenessDetection branch September 3, 2024 19:12
hernanponcedeleon pushed a commit that referenced this pull request Sep 16, 2024
@ThomasHaas @hernan-poncedeleon
Improved liveness detection for store exclusives (#722)
38a2844
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@ThomasHaas @hernanponcedeleon @db7 @xeren @DIvanov503 @natgavrilenko