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

Improve condvar signaling #323

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Improve condvar signaling #323

wants to merge 1 commit into from

Conversation

krtab
Copy link
Collaborator

@krtab krtab commented Jun 18, 2024

No description provided.

@krtab krtab mentioned this pull request Jun 18, 2024
Closed
@zapashcanon
Copy link
Member

I'm going to bench this on Test-Comp first

@zapashcanon
Copy link
Member

Main: Nothing: 75 Reached: 613 Timeout: 527 Other: 1 Killed: 0
This PR: Nothing: 75 Reached: 609 Timeout: 531 Other: 1 Killed: 0

Also:

on      commonly  reached tasks, tool 1 took 1575.201145 sec. (mean 2.586537) and tool 2 took 1614.162636 sec. (mean 2.650513)

(tool1 is main, tool2 is this PR)

@zapashcanon
Copy link
Member

zapashcanon commented Jul 3, 2024 •
edited
Loading

@krtab, what should we do with this one ?

(also could you rebase so I can restart the CI ?)

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
no changelog
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@krtab @zapashcanon