Skip to content

Add support for specifying custom rounds#23

Merged
lim123123123 merged 11 commits intoITMO-PTDC-Team:masterfrom
dmitrii-artuhov:dartiukhov/feature/custom-rounds
Mar 9, 2026
Merged

Add support for specifying custom rounds#23
lim123123123 merged 11 commits intoITMO-PTDC-Team:masterfrom
dmitrii-artuhov:dartiukhov/feature/custom-rounds

Conversation

@dmitrii-artuhov
Copy link
Copy Markdown
Contributor

@dmitrii-artuhov dmitrii-artuhov commented Jan 15, 2026

Features:

  • Separate macros for test with predefined custom rounds
  • Number of threads could be different from --threads flag
  • Minimization also works for custom rounds
  • If predefined custom rounds do not detect error, regular round generation will start

Example:

// data structure implementation
struct Queue {
  non_atomic void Push(int v) { ... }
  non_atomic int Pop() { ... }
  void Reset() { ... }
  // ...
};

LTEST_ENTRYPOINT(
  spec_t,
  { // custom round 1
    { // thread 1
      method_invocation(std::tuple(1), void, Queue, Push, int),
      method_invocation(std::tuple(2), void, Queue, Push, int),
      method_invocation(std::tuple(), int, Queue, Pop),
    },
    { // thread 2
      method_invocation(std::tuple(3), void, Queue, Push, int),
      method_invocation(std::tuple(), int, Queue, Pop)
    }
  },
  { // custom round 2
    ...
  }
);

// regular `target_method`s macros also could be added,
// round generation will be run after all custom scenarios execution
// (and in case if custom rounds do not find an error)

TODO:

  • For some reason after this commit bug detection takes very long and the custom round did not detect an error, but it should. I guess the instrumetation changed in that commit which might lead to less unique thread interleavings
  • Add more tests for custom rounds:
    • for different startegies
    • with regular rounds generation as well

Comment thread verifying/targets/CMakeLists.txt Outdated
Comment on lines +79 to +80
# TODO: test should fail, but for some reason after commit '15f64f0 - feat: add more tests for blocking data structures&refactor blocking support'
# it takes too much time to find bugs, I wasn't able to wait until custom round detects a bug
Copy link
Copy Markdown
Contributor Author

@dmitrii-artuhov dmitrii-artuhov Jan 15, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Пробовал запускать с --exploration_runs 200'000 и с разными стратегиями по несколько раз, но баг не находится. Хотя на моей старой ветке с этой фичой, которая не заребежена на текущий master, баг находится и очень быстро. Также в целом все тесты находят баги гараздо быстрее, чем сейчас на мастере. Надо посмотреть, мб, переключений сильно меньше вставляется сейчас, чем раньше. Пока не исследовал эту теорию

Copy link
Copy Markdown
Collaborator

@lim123123123 lim123123123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Наверное лучше разобраться с тем поч сча твой custom_round тест для очереди не находит баг, дифф с коммитов, который сломал, но кажется, что самое реалистичное - посмотреть куда расставились переключения + прогнаться с ним на одном сиде

Comment thread .github/workflows/run-tests.yaml Outdated
Comment thread runtime/include/random_strategy.h
Comment thread runtime/include/scheduler.h
Comment thread runtime/include/scheduler.h
Comment thread verifying/targets/nonlinear_queue_with_custom_round.cpp
Copy link
Copy Markdown
Collaborator

@lim123123123 lim123123123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@lim123123123 lim123123123 merged commit 650ccfd into ITMO-PTDC-Team:master Mar 9, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants