User Tools

Site Tools


sv-comp_2015_arrays

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sv-comp_2015_arrays [2015/01/14 10:21]
mictau
sv-comp_2015_arrays [2015/01/14 15:10] (current)
mbrain
Line 1: Line 1:
-<​code>​ +====== General Observations ====== 
-# For Arrays, BitVectors, ControlFlowInteger/​loop-acceleration:​ + 
-time cbmc --verbosity 10 with increasing unwinding bounds to figure out +All benchmarks are too large to unwind fully. ​ Often contain looks that generate assertions. ​ Thus all true answers are due to the strategy of the script and not anything in the core of CBMC.  No-one gave a valid counter-example for any of these. ​ Almost all loops look acceleratable. 
-whether memory or CPU time is the main limiting factor; then use gprof (CPU + 
-time) or valgrind/​massif (memory) to identify the key bits requiring +====== Michael'​s Analysis ====== 
-improvement+ 
 +time cbmc --verbosity 10 with increasing unwinding bounds to figure out 
 +whether memory or CPU time is the main limiting factor; then use gprof (CPU 
 +time) or valgrind/​massif (memory) to identify the key bits requiring 
 +improvement 
 + 
 +==== Too few unwindings (>100000 required) ==== 
 + 
 +Arrays/​array-examples/​data_structures_set_multi_proc_false-unreach-call_ground.i
  
-# Too few unwindings (>100000 required) 
 Arrays/​array-examples/​sorting_bubblesort_false-unreach-call2_ground.i Arrays/​array-examples/​sorting_bubblesort_false-unreach-call2_ground.i
 +
 Arrays/​array-examples/​sorting_bubblesort_false-unreach-call_ground.i Arrays/​array-examples/​sorting_bubblesort_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​sorting_selectionsort_false-unreach-call2_ground.i Arrays/​array-examples/​sorting_selectionsort_false-unreach-call2_ground.i
 +
 +Arrays/​array-examples/​standard_allDiff2_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_copy1_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy1_false-unreach-call_ground.i
-Arrays/​array-examples/​data_structures_set_multi_proc_false-unreach-call_ground.i+
 Arrays/​array-examples/​standard_copy2_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy2_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_copy3_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy3_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_copy4_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy4_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_copy5_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy5_false-unreach-call_ground.i
-Arrays/​array-examples/​standard_allDiff2_false-unreach-call_ground.i+
 Arrays/​array-examples/​standard_copy6_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy6_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_copy7_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy7_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_copy8_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy8_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_copy9_false-unreach-call_ground.i Arrays/​array-examples/​standard_copy9_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_copyInitSum2_false-unreach-call_ground.i Arrays/​array-examples/​standard_copyInitSum2_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_init1_false-unreach-call_ground.i Arrays/​array-examples/​standard_init1_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_init2_false-unreach-call_ground.i Arrays/​array-examples/​standard_init2_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_init3_false-unreach-call_ground.i Arrays/​array-examples/​standard_init3_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_init4_false-unreach-call_ground.i Arrays/​array-examples/​standard_init4_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_init5_false-unreach-call_ground.i Arrays/​array-examples/​standard_init5_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_init6_false-unreach-call_ground.i Arrays/​array-examples/​standard_init6_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_init7_false-unreach-call_ground.i Arrays/​array-examples/​standard_init7_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_init8_false-unreach-call_ground.i Arrays/​array-examples/​standard_init8_false-unreach-call_ground.i
-Arrays/​array-examples/​standard_minInArray_false-unreach-call_ground.i+
 Arrays/​array-examples/​standard_init9_false-unreach-call_ground.i Arrays/​array-examples/​standard_init9_false-unreach-call_ground.i
 +
 +Arrays/​array-examples/​standard_minInArray_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_partition_false-unreach-call_ground.i Arrays/​array-examples/​standard_partition_false-unreach-call_ground.i
 +
 Arrays/​array-examples/​standard_running_false-unreach-call.i Arrays/​array-examples/​standard_running_false-unreach-call.i
-SAT solver takes forever!? (Even --unwind 2)+ 
 + 
 +==== SAT solver takes forever!? (Even --unwind 2) ==== 
 Arrays/​array-examples/​standard_sentinel_true-unreach-call.i Arrays/​array-examples/​standard_sentinel_true-unreach-call.i
-</​code>​+ 
 +Seems to have finished at least one iteration within the competition time. 
 + 
 + 
 + 
 +====== Performance Regressions ====== 
 + 
 + 
 +Times are an order of magnitude or two greater than ESBMC, probably due to a better (non-eagerly instantiating) array theory. 
 + 
 +The following two manage at least one unwinding but not all of them: 
 + 
 +data_structures_set_multi_proc_true-unreach-call_ground.i 
 + 
 +standard_sentinel_true-unreach-call.i 
 + 
 +====== Non-Green Benchmarks from SV-COMP 2015 ====== 
 + 
 +All of the ones Michael diagnosed plus the following, all of which list out-of-memory:​ 
 + 
 +sorting_bubblesort_true-unreach-call_ground.i 
 + 
 +standard_copy7_true-unreach-call_ground.i 
 + 
 +standard_copy8_true-unreach-call_ground.i 
 + 
 +standard_copy9_true-unreach-call_ground.i 
 + 
 +standard_init8_true-unreach-call_ground.i 
 + 
 +standard_init9_true-unreach-call_ground.i 
 + 
sv-comp_2015_arrays.txt · Last modified: 2015/01/14 15:10 by mbrain