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.

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

Remove spin lock in waitWhileAutoMode. #3356

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Remove spin lock in waitWhileAutoMode. #3356

wants to merge 3 commits into from

Conversation

wadoon
Copy link
Member

@wadoon wadoon commented Nov 19, 2023

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.

Copy link

codecov bot commented Nov 20, 2023

Codecov Report

All modified and coverable lines are covered by tests ✅

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

❗ 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     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@unp1 unp1 self-requested a review November 20, 2023 07:39
@unp1
Copy link
Member

unp1 commented Nov 22, 2023

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 wadoon changed the title remove spin lock Remove spin lock in waitWhileAutoMode. Nov 24, 2023
@wadoon wadoon marked this pull request as ready for review November 24, 2023 12:29
@wadoon wadoon added GUI 🛠 Maintenance Code quality and related things w/o functional changes labels Nov 24, 2023
@wadoon wadoon self-assigned this Nov 24, 2023
@wadoon
Copy link
Member Author

wadoon commented Dec 7, 2023

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
Copy link
Member

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.

@wadoon wadoon force-pushed the weigl/spinlock branch from 0373d7c to 27f04d1 Compare May 2, 2024 09:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
GUI 🛠 Maintenance Code quality and related things w/o functional changes
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants