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

Worker pool cleanups #3419

Merged
merged 6 commits into from
Nov 29, 2021
Merged

Worker pool cleanups #3419

merged 6 commits into from
Nov 29, 2021

Commits on Nov 26, 2021

  1. Remove unused header file

    NelsonVides committed Nov 26, 2021
    Configuration menu
    Copy the full SHA
    2114824 View commit details
    Browse the repository at this point in the history

Commits on Nov 27, 2021

  1. Configuration menu
    Copy the full SHA
    d8a4a94 View commit details
    Browse the repository at this point in the history
  2. Use stored name instead of regenerating it on every use

    I suspect this might also have somehow better concurrency
    characteristics, as generating the name generates atoms, and therefore
    needs to grab locks on the atom table, which is not optimised for
    writes, even if the write is idempotent as the atom already exists, but
    this one is mostly guessing. Sequential performance is surely much
    better.
    NelsonVides committed Nov 27, 2021
    Configuration menu
    Copy the full SHA
    cbdb5aa View commit details
    Browse the repository at this point in the history

Commits on Nov 28, 2021

  1. Configuration menu
    Copy the full SHA
    970a17a View commit details
    Browse the repository at this point in the history
  2. Remove long-irrelevant comment

    This is invalid since f3ada67 and 7df0bf8
    NelsonVides committed Nov 28, 2021
    Configuration menu
    Copy the full SHA
    ec9d240 View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2021

  1. Configuration menu
    Copy the full SHA
    eee8837 View commit details
    Browse the repository at this point in the history