Skip to content

Conversation

@michael-schwarz
Copy link
Member

@michael-schwarz michael-schwarz commented May 14, 2025

current_node is a bit problematic as it is global mutable state. For the concurrent solvers, it would be nice to get rid of such things: DLS is only a solution where one Domain maps to one uninterrupted task.

Also, in general, it's ugly to have such mutable global state.

In many cases the usage was actually not truly needed. In some cases it is a bit more complicated, these remain to be done here.

@michael-schwarz michael-schwarz added the cleanup Refactoring, clean-up label May 14, 2025
@michael-schwarz michael-schwarz marked this pull request as ready for review May 14, 2025 11:25
@michael-schwarz michael-schwarz requested review from arkocal and sim642 May 14, 2025 11:25
@michael-schwarz
Copy link
Member Author

Related #1730.

@michael-schwarz michael-schwarz changed the title Remove (some) usages of MyCFG.current_node Remove some usages of MyCFG.current_node May 14, 2025
@sim642 sim642 added this to the v2.6.0 milestone May 15, 2025
@sim642 sim642 added the parallel Parallel Goblint label May 15, 2025
@arkocal
Copy link
Contributor

arkocal commented May 15, 2025

Thanks for beginning the effort! We should solve the issue in precisionUtil and messages as well, but I am not opening issues yet, since the topics are on next weeks GobCon agenda.

@arkocal arkocal merged commit 8b9b045 into master May 15, 2025
21 checks passed
@arkocal arkocal deleted the remove_current_node_usages branch May 15, 2025 09:48
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 5, 2025
CHANGES:

* Add division by zero analysis (goblint/analyzer#1764).
* Add bitfield domain (goblint/analyzer#1623).
* Add weakly-relational C-2PO pointer analysis (goblint/analyzer#1485).
* Add widening delay (goblint/analyzer#1358, goblint/analyzer#1442, goblint/analyzer#1483).
* Add narrowing of globals to top-down solver (goblint/analyzer#1636).
* Add weak dependencies to top-down solver (goblint/analyzer#1746, goblint/analyzer#1747).
* Add YAML ghost witness generation (goblint/analyzer#1394).
* Remove GraphML witness generation (goblint/analyzer#1732, goblint/analyzer#1733, goblint/analyzer#1738).
* Use C standard option for preprocessing (goblint/analyzer#1807).
* Add bash completion for array options (goblint/analyzer#1670, goblint/analyzer#1705, goblint/analyzer#1750).
* Make `malloc(0)` semantics configurable (goblint/analyzer#1418, goblint/analyzer#1777).
* Update path-sensitive analyses (goblint/analyzer#1785, goblint/analyzer#1791, goblint/analyzer#1792).
* Fix evaluation of library function arguments (goblint/analyzer#1758, goblint/analyzer#1761).
* Optimize affine equalities analysis using sparse matrices (goblint/analyzer#1459, goblint/analyzer#1625).
* Prepare for parallelism (goblint/analyzer#1708, goblint/analyzer#1744, goblint/analyzer#1748, goblint/analyzer#1781, goblint/analyzer#1790).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up parallel Parallel Goblint

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants