Using -svcomp option for non-SV-COMP benchmark programs

[Yoel Kim]

Dear CPAchecker,

I applied the -svcomp22 option to a more complex program than the sv-comp benchmark. However, since verifying my target program takes longer than 900 seconds, I wanted to resolve this by removing "limits.time.cpu::required = 900" from the configuration file.

Another issue here was that for each analysis strategy, it only uses a maximum of 90 seconds, and if it doesn't find any counterexamples within this time, the verification process terminates.

Is there a way to apply more than 90 seconds here?
Or there are any recommendable configurations for verifying user-defined properties in embedded software with infinite loops? I used -predicateAnalysis, but it does not work well.

[Philipp Wendler]

Dear Yoel Kim,

Am 22.09.23 um 07:50 schrieb Yoel Kim:

As you have noticed, the -svcomp22 configuration is a complex
configuration that consists of many different analyses combined using
strategy selection, sequential combinations, and parallel combinations.
Due to the sequential combination, a simple extension of the time limit
is not really meaningful, as it would only extend the time available for
the last of these analyses. This is why CPAchecker refuses to run this
configuration with a different time limit than 900s by default.

Of course you are free to create your own configuration for CPAchecker
and you can base this on the existing configs by adapting their time
limits to the values you prefer. But the CPAchecker team has no
experience with running something like -svcomp22 for a longer time, so
we cannot advise on which values would be most appropriate.

In general, a configuration like -svcomp22 is really most suited for use
cases where you want to verify lots of different programs and have only
limited resources. For use cases with a specific kind of program or with
more resources I would recommend to experiment with the individual
analyses on their own. This way you can learn what works well for your
programs.

Besides -predicateAnalysis I can recommend trying out -kInduction, which
is also part of -svcomp22 and the default analysis of CPAchecker for
reachability properties.
-predicateAnalysis-ImpactRefiner-ABEl would also be an option.
If you are only interested in finding bugs and not in proofs,
then -bmc-incremental is a good choice (but it will typically not know
when to terminate and thus run as long as you let it).

Greetings
Philipp

--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

[Yoel Kim]

Thank you for your answer. 

I have one more question about memory usage of CPAchecker. 

Used heap memory:               1343MB (  1280 MiB) max;    714MB (   681 MiB) avg;   1871MB (  1785 MiB) peak
Used non-heap memory:             62MB (    59 MiB) max;     54MB (    52 MiB) avg;     64MB (    61 MiB) peak
Used in G1 Old Gen pool:         843MB (   803 MiB) max;    330MB (   315 MiB) avg;    798MB (   761 MiB) peak
Allocated heap memory:          2151MB (  2052 MiB) max;   1346MB (  1284 MiB) avg
Allocated non-heap memory:        65MB (    62 MiB) max;     58MB (    56 MiB) avg
Total process virtual memory:  16759MB ( 15982 MiB) max;  16247MB ( 15494 MiB) avg

I don't know what the differences are between them, specifically, I'm not sure about the differences between 'used' and 'allocated,' as well as 'max' and 'peak memory.

2023년 9월 22일 금요일 오후 6시 9분 27초 UTC+9에 Philipp Wendler님이 작성:

[Philipp Wendler]

Hi Yoel Kim,

Am 22.09.23 um 11:42 schrieb Yoel Kim:

> I have one more question about memory usage of CPAchecker.
>
> Used heap memory: 1343MB ( 1280 MiB) max; 714MB ( 681
> MiB) avg; 1871MB ( 1785 MiB) peak
> Used non-heap memory: 62MB ( 59 MiB) max; 54MB ( 52
> MiB) avg; 64MB ( 61 MiB) peak
> Used in G1 Old Gen pool: 843MB ( 803 MiB) max; 330MB ( 315
> MiB) avg; 798MB ( 761 MiB) peak
> Allocated heap memory: 2151MB ( 2052 MiB) max; 1346MB ( 1284
> MiB) avg
> Allocated non-heap memory: 65MB ( 62 MiB) max; 58MB ( 56
> MiB) avg
> Total process virtual memory: 16759MB ( 15982 MiB) max; 16247MB ( 15494
> MiB) avg
>
> I don't know what the differences are between them, specifically, I'm not
> sure about the differences between 'used' and 'allocated,' as well as 'max'
> and 'peak memory.

"used" and "allocated" are two numbers that the JVM defines (the latter
is called "committed" by the JVM). The definition of this is in the
table at the top here:
https://docs.oracle.com/en/java/javase/17/docs/api/java.management/java/lang/management/MemoryUsage.html

The "peak" numbers are also provided by the JVM.
"max" however is calculated by CPAchecker: We sample the current memory
consumption of CPAchecker repeatedly and return the maximal value that
we have seen. This is because in the past we didn't have the peak value
provided by the JVM or it was not reliable. Nowadays I would tend to
ignore it and use "peak" instead.
"avg" is also produced by our sampling like "max" and simply the average
of all values over the runtime of CPAchecker.

I hope that helps.