KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Remove spin lock in waitWhileAutoMode. #3356

Open wadoon opened 9 months ago

wadoon commented 9 months ago

This PR removes the spin-lock waiting in MediatorProofControl used for waiting on auto-mode finish.

      while (ui.getMediator().isInAutoMode()) { // Wait until auto mode has stopped.
            try {
                Thread.sleep(100);
            } catch (InterruptedException e) {
            }
        }

It uses the Condition class provided by Java5+ concurrent API. Conditions provide a simple interface for waiting and signaling of threads.

We may want to discuss, whether we want one lock in KeYMediator and share it with the threads, or the current solution, the threads have an lock and set the condition in MediatorProofControl.

It is hard to test, but I didn't observe anything by pressing the start/stop button wildly.

codecov[bot] commented 9 months ago

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 37.98%. Comparing base (7254776) to head (5e1b4f6). Report is 38 commits behind head on main.

:exclamation: Current head 5e1b4f6 differs from pull request most recent head 27f04d1. Consider uploading reports for the commit 27f04d1 to get more accurate results

Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3356 +/- ## ============================================ + Coverage 37.86% 37.98% +0.12% + Complexity 17079 17025 -54 ============================================ Files 2092 2059 -33 Lines 127596 126029 -1567 Branches 21478 21282 -196 ============================================ - Hits 48316 47874 -442 + Misses 73355 72272 -1083 + Partials 5925 5883 -42 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

unp1 commented 9 months ago

Hi,

thanks a lot! In the sibling class "DefaultProofControl" there is a similar busy wait, is it possible to apply your solution there as well?

Best regards, Richard

wadoon commented 9 months ago

I removed the spin lock also from DefaultProofControl. It is rather a simple change, I did not try to avoid code duplication.

We have plenty of Thread.sleeps in the test cases. And there is a strange class Watchdog, which says it tries to detect deadlocks, but this makes no sense because Java has a built-in mechanism for deadlock detection.

/cc @FliegendeWurst

FliegendeWurst commented 8 months ago

And there is a strange class Watchdog, which says it tries to detect deadlocks, but this makes no sense because Java has a built-in mechanism for deadlock detection.

The class is supposed to detect when the GUI thread is blocked. That's not automatically handled by Java.