Klever

Input files for static verifiers are included just if corresponding option is enabled at the job start up page. For the production mode this isn't the case.

To get rid of annoying and large logs I suppose to reduce log levels in the production mode even more - to WARNING. As far as I understand, if log files are absent or empty, Core can report "log": null rather than to create artificial empty files and upload them.

I didn't catch why unknown reports need their parent reports to be uploaded. There are quite a lot of unknown reports, thus the corresponding number of parent reports will be kept as well. If Core has unknown report, the job is Failed rather than Corrupted, but for this something special can be added, e.g. specify this in another table.

Vladimir Gratinskiy wrote:

Evgeny Novikov wrote:

Input files for static verifiers are included just if corresponding option is enabled at the job start up page. For the production mode this isn't the case.

For log's should be the same option.

I guess that it already exists and called the log level. But actually I understand that for lightweight verification results there shouldn't be logs at all because of they won't be available. We should specify the lowest log level (all logs will be most likely empty) or even, better, specify special log levels, say, NONE, meaning that logging isn't required (this will be even a bit more efficient).

To get rid of annoying and large logs I suppose to reduce log levels in the production mode even more - to WARNING. As far as I understand, if log files are absent or empty, Core can report "log": null rather than to create artificial empty files and upload them.

You can have reports with 'log': null and without 'log' at all.

I didn't catch why unknown reports need their parent reports to be uploaded. There are quite a lot of unknown reports, thus the corresponding number of parent reports will be kept as well. If Core has unknown report, the job is Failed rather than Corrupted, but for this something special can be added, e.g. specify this in another table.

For example, the report's page have status of component. If component has unknown as its child then status=Failed and status is link to the corresponding unknown. Several unknowns for component will lead to exception.

This and some other checks can be (already are) missed for lightweight verification results since we rely upon everything is quite good enough..
I still don't see any sense to keep component statutes. Just keep unknown reports with required attributes, including component names, somehow. You can even introduce new fields or even tables especially for lightweight verification results.

Now branch is ready to tests with huge jobs and to merge to master. It contains migration.

Evgeny Novikov wrote:

Vladimir Gratinskiy wrote:

Evgeny Novikov wrote:

Input files for static verifiers are included just if corresponding option is enabled at the job start up page. For the production mode this isn't the case.

For log's should be the same option.

I guess that it already exists and called the log level. But actually I understand that for lightweight verification results there shouldn't be logs at all because of they won't be available. We should specify the lowest log level (all logs will be most likely empty) or even, better, specify special log levels, say, NONE, meaning that logging isn't required (this will be even a bit more efficient).

I created special log level NONE that is now the default one for the production mode. Corresponding logs, logging handlers and files aren't created and uploaded. Since this works even in master, I implemented this there and merge master to the current branch.

When you mentioned resources (just total ones since component reports are thrown away) I realized that information on the total number of safes will be also welcome since it will reflect how many verification tasks were solved. As well it shouldn't be removed when caches are recalculated and when a job archive is downloaded/uploaded.

In addition, I think that Bridge should allow null proofs for safe reports, since most likely we will not upload them at all unless one will ask for this (#6598).

Evgeny Novikov wrote:

After first look I have the following questions and remarks:

1. Since unsafe reports don't have attributes unsafe marks are created too long (there are not fast filters based on attributes matching - just on error trace comparison).

Oh, I forgot about attributes. Will be fixed soon.

1. Core has status Failed even if it finishes successfully - it is enough to finish with unknown for one of its children.

The lightweight job is Failed because the scheduler said it has Failed. Normal jobs can be also failed if Core has unknown as its child.

1. It would be better to move flag lightweight from jobs themselves to the jobs non fast start decision page since it isn't a job property - it is a property of job verification results representation (although one can argue that verification results do differ with and without that flag, but indeed this difference isn't very important from the verification perspective - all unsafes and unknowns are kept).

Will be moved soon.

1. There is "Safe(0)" when, say, some unknown report is uploaded.

Maybe besause there no safes? I'll fix it so there will be Safes(x) if x > 0.

1. I am interested in how collapsing works. As far as I can see, all component reports are actually uploaded to the database and can be even viewed by the user. But then (when?) the most of them disappear. I don't think that reports to be deleted should be shown to users. In addition I am not sure that it is a good idea to remove them with some delay. If I understand properly when we will verify all Linux kernel modules, then actual collapsing will work just when all of them will be verified - too much overhead.

Collapsing or lightweight job verification? I think you mean the second case.
Reports are deleted when you upload finish Core report. Reports tree is needed to collect unsafes attributes (currently it doesn't work but I suggested it). Reports' archives and data are uploaded for Core component and for verification reports, so only parents, resources, cache are filled for reports that will be deleted at the end. It is too difficult to hide reports that will be deleted. Maybe it is easier to upload all needed attributes with unsafe reports?

Vladimir Gratinskiy wrote:

Evgeny Novikov wrote:

After first look I have the following questions and remarks:

1. Core has status Failed even if it finishes successfully - it is enough to finish with unknown for one of its children.

The lightweight job is Failed because the scheduler said it has Failed. Normal jobs can be also failed if Core has unknown as its child.

I think that you didn't understand. Status of the whole job decision is Solved (Core returns 0 and Native Scheduler reports about successful decision). But when I click Solved I see that Core has status Failed although the only unknown report is the child report of the report of the Core component.

1. There is "Safe(0)" when, say, some unknown report is uploaded.

Maybe besause there no safes? I'll fix it so there will be Safes(x) if x > 0.

Definitely this will be better. BTW, non-lightweight verification results also suffer from this in the given branch.

1. I am interested in how collapsing works. As far as I can see, all component reports are actually uploaded to the database and can be even viewed by the user. But then (when?) the most of them disappear. I don't think that reports to be deleted should be shown to users. In addition I am not sure that it is a good idea to remove them with some delay. If I understand properly when we will verify all Linux kernel modules, then actual collapsing will work just when all of them will be verified - too much overhead.

Collapsing or lightweight job verification? I think you mean the second case.

Yes, the second case (collapsing during getting lightweight verification results).

Reports are deleted when you upload finish Core report. Reports tree is needed to collect unsafes attributes (currently it doesn't work but I suggested it). Reports' archives and data are uploaded for Core component and for verification reports, so only parents, resources, cache are filled for reports that will be deleted at the end. It is too difficult to hide reports that will be deleted. Maybe it is easier to upload all needed attributes with unsafe reports?

Okay, let's show them. I don't think that uploading all needed attributes with unsafe reports is enough. Also you need to assume that for each started component an unknown report can be received. The good suggestion is the following. You can remove information on component reports immediately when they terminate, i.e. Bridge receive their finish reports, because of starting from this time such reports couldn't receive any child report which can, say, requires their attributes. I think that this will allow to remove the most of intermediate tree nodes quite quickly.
As well I am interested, do you keep data for all verification reports or just for those ones that can child unsafe reports? Actually for other verification reports it will be unreached.

Evgeny Novikov wrote:

Vladimir Gratinskiy wrote:

Evgeny Novikov wrote:

After first look I have the following questions and remarks:

1. Core has status Failed even if it finishes successfully - it is enough to finish with unknown for one of its children.

The lightweight job is Failed because the scheduler said it has Failed. Normal jobs can be also failed if Core has unknown as its child.

I think that you didn't understand. Status of the whole job decision is Solved (Core returns 0 and Native Scheduler reports about successful decision). But when I click Solved I see that Core has status Failed although the only unknown report is the child report of the report of the Core component.

Can you provide me with such job?

1. There is "Safe(0)" when, say, some unknown report is uploaded.

Maybe besause there no safes? I'll fix it so there will be Safes(x) if x > 0.

Definitely this will be better. BTW, non-lightweight verification results also suffer from this in the given branch.

Non-lightweight verification safes are not shown if number of safes is 0. For lightweight results it is already the same.

Reports are deleted when you upload finish Core report. Reports tree is needed to collect unsafes attributes (currently it doesn't work but I suggested it). Reports' archives and data are uploaded for Core component and for verification reports, so only parents, resources, cache are filled for reports that will be deleted at the end. It is too difficult to hide reports that will be deleted. Maybe it is easier to upload all needed attributes with unsafe reports?

Okay, let's show them. I don't think that uploading all needed attributes with unsafe reports is enough. Also you need to assume that for each started component an unknown report can be received. The good suggestion is the following. You can remove information on component reports immediately when they terminate, i.e. Bridge receive their finish reports, because of starting from this time such reports couldn't receive any child report which can, say, requires their attributes. I think that this will allow to remove the most of intermediate tree nodes quite quickly.

Good idea. Working on this.

As well I am interested, do you keep data for all verification reports or just for those ones that can child unsafe reports? Actually for other verification reports it will be unreached.

For all verification reports as unsafe can be uploaded after verification report is uploaded.

Core began to send "verification finish" reports starting from 611a46e to branch feature_7368.

Done. Job configuration file must include 'lighweightness' option (true/false) now.