Project

General

Profile

Actions

Feature #10852

closed

Support parallel execution of Weaver

Added by Evgeny Novikov 8 months ago. Updated 7 months ago.

Status:
Closed
Priority:
High
Category:
Tasks generation
Target version:
Start date:
06/10/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Weaver instruments original source files and models sequentially that is pretty well for the production mode and when there are many verification tasks that are generated and solved in parallel. In the development mode or when there is the only verification task this is very inefficient. Indeed, Weaver can consume most of wall time at least for generation of verification tasks. It would be great to support parallel execution of Weaver and to have a separate option that will allow to specify the number of parallel workers for Weaver when starting a verification job decision.

Actions #1

Updated by Evgeny Novikov 7 months ago

  • Target version changed from 3.3 to 3.2
  • Status changed from New to Resolved

I did this in branch parallel-weaver. Let's see on CI results since it is a quite crucial improvement.

Actions #2

Updated by Evgeny Novikov 7 months ago

CI helped to reveal data races that I fixed in the same branch. Let's wait for new results.

Actions #3

Updated by Evgeny Novikov 7 months ago

  • Status changed from Resolved to Closed

Tests passed, so, I merged the branch to master in e280b0df5. Existing configurations for job decisions will not work unless you will specify the number of parallel workers for "Weaving". By default in the development mode there are will be quite many Weaver workers (0.5, i.e. a half of CPU cores).

Actions #4

Updated by Evgeny Novikov 7 months ago

  • Status changed from Closed to Open

CI reported a data race one more time. It turned out that I fixed it incorrectly last time. Unlike another data race, this one happens extremely seldom, but nevertheless it is crucial.

Actions #5

Updated by Evgeny Novikov 7 months ago

  • Status changed from Open to Resolved

I fixed the data race in branch fix-data-race-weaver. Let's wait for CI results.

Actions #6

Updated by Evgeny Novikov 7 months ago

  • Status changed from Resolved to Closed

Tests passed, so, I merged the branch to master in 9178752a8.

Actions

Also available in: Atom PDF