Project

General

Profile

Actions

Feature #8646

closed

Optimize total coverage calculation

Added by Evgeny Novikov almost 7 years ago. Updated over 6 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Results processing
Target version:
Start date:
12/26/2017
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

It turned out that calculation of total coverage needs too much memory when a lot of modules are verified against even a single rule specification (several hundreds of MB). For several rule specification it will be a disaster.

I suggest to calculate total coverage independently for each rule specification checked. Moreover it will be great to merge coverage for individual verification tasks step by step rather than to do it at the end of verification. In that way it won't be needed to keep all individual coverages in memory which is obviously absolutely inefficient.

Actions #1

Updated by Evgeny Novikov over 6 years ago

  • Assignee changed from Alexey Polushkin to Ilja Zakharov
  • Target version changed from 2.0 to 1.1

This issue is not strictly bound with purposes of 2.0 that targets verification of C software.

Actions #2

Updated by Ilja Zakharov over 6 years ago

  • Status changed from New to Resolved

Implemented in 8646-optimized-coverage.

Actions #3

Updated by Evgeny Novikov over 6 years ago

  • Status changed from Resolved to Open

Please, merge latest master to that branch - there are non-trivial conflicts.

Actions #4

Updated by Evgeny Novikov over 6 years ago

  • Status changed from Open to Closed

I merged master to the branch and tested it. Our tests don't show noticeable differences in consumed computational resources related with coverage calculation. But for large scale verification one will feel the difference. Indeed, Ilja got rid of linear dependency of computational resources on the number of checked rule specifications. So, now Klever will not fail when checking many rule specifications due to lack of memory at the end of work.

I merged the branch to master in 40fd1a68d.

Actions

Also available in: Atom PDF