key icon indicating copy to clipboard operation
key copied to clipboard

Remove spin lock in waitWhileAutoMode.

Open wadoon opened this issue 2 years ago • 4 comments

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.

wadoon avatar Nov 19 '23 23:11 wadoon

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
@@             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.

codecov[bot] avatar Nov 20 '23 00:11 codecov[bot]

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

unp1 avatar Nov 22 '23 11:11 unp1

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

wadoon avatar Dec 07 '23 02:12 wadoon

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.

FliegendeWurst avatar Jan 03 '24 17:01 FliegendeWurst