VST upgrade 2.6 -> 2.8: 80% slowdown in compilation time #514
Comments
|
Can you provide more information about the funspec of the function Within g, just at the forward_call to function f, there are then 12 lvars and 12 (Of course, perhaps it goes fast on my machine because I have a core i7 processor...) |
|
More measurements, shown here demonstrate that having 20 lvars, with the associated 20 data_at conjuncts, and functions with between 0 and 20 pointer parameters (with the corresponding 0 to 20 data_at conjuncts in the precondition), does not lead to exponential slowdown. So, this issue report illustrates some performance problem in VST, but it's not simply the number of variables, or the number of function parameters, or the number of SEP conjuncts. |
Related: [vst-user] mailing list thread, VST performance thread on Coq discoruse.
After upgrading our relatively large (43KLOC) C verification project from VST version 2.6 to 2.8 (along with ocaml and some others), we've encountered a major increase in compilation time: from 3.2 to 5.7 hours on single thread.
Following are the benchmarks of the same project before and after VST upgrade (with only minor fixes made).
VST 2.6
Opam switch
Using coq-config.
NOTE: despite it being included in the base compiler, Coq was built without flambda support.
Slowest lines
Based on
coq_makefile'sTIMING=1.Time+Memory per file
Based on
coq_makefile'spretty-timed.VST 2.8
Opam switch
Using coq-config.
Slowest lines
Based on
coq_makefile'sTIMING=1.Time+Memory per file
Based on
coq_makefile'spretty-timed.Sure, our code is not well optimzed, but the exact same tactic invocations are taking up to 4 times as long after the upgrade.
Furethermore, peak memory consumption of 15GiB is achieved in the same tactic invocation under both versions. Here are some details:
Peak memory tactic
Runninng
for goal corresponding to this line in C:
Espec : OracleKind opt_codec_ctx_p, td_p : val td : TYPE_descriptor tags_p : val b : block i : ptrofs ptr : list int res_p : val size : Z last_length_p : val max_stack_size : Z Delta_specs := abbreviate : PTree.t funspec Delta := abbreviate : tycontext v_tlv_tag, v_tlv_len, v_rval, v_rval__1, v_rval__2, v_rval__3, v_rval__4, v_rval__5, v_rval__6, v_rval__7, v_rval__8, v_rval__9, v_rval__10, v_rval__11, v_rval__12 : val i0, i1 : int Heqp : Exec.ber_fetch_tags ptr size = (i0, i1) H : (Znth (Int.signed i0) ptr & Int.repr 128)%int = 0 /\ 0 < len ptr - Int.signed i0 H2 : 0 < len ptr <= Int.max_signed H3 : (Znth 0 ptr & Int.repr 32)%int = 0 H6 : 1 = len (tags td) H7 : 0 <= Ptrofs.unsigned i + len ptr <= Ptrofs.max_unsigned H8 : Forall (fun x : int => 0 <= Int.signed x <= Byte.max_signed) ptr H9 : 0 <= size <= 32 /\ size = len ptr A : -1 <= ASN__STACK_OVERFLOW_CHECK 0 max_stack_size <= 0 H0 : opt_codec_ctx_p <> nullval H1 : ASN__STACK_OVERFLOW_CHECK 0 max_stack_size = 0 i2, i3 : int Heqp0 : Exec.ber_fetch_len (sublist (Int.signed i0) (len ptr) ptr) 0 0 (Int.repr size - i0)%int (Int.repr (sizeof tuint)) (Int.repr Int.max_signed) = (i2, i3) ptr' : list val Heqptr' : ptr' = map Vint ptr POSTCONDITION := abbreviate : ret_assert z : Z Heqb0 : z = 0 H4 : 0 <= z <= 1 H5 : z < len (tags td) LLL : size < Int.max_signed PPP : size = len ptr H10 : ((i0 == Int.repr (-1)) || (i0 == 0))%bool = false H11 : Vptr b i = field_address (tarray tuchar (len ptr)) (SUB 0) (Vptr b i) H12 : i1 = Int.repr (Znth z (tags td)) MORE_COMMANDS := abbreviate : statement G : 0 <= size <= 32 U : size = len ptr B : i0 = fst (i0, i1) -> ((i0 == 0) || (i0 == Int.repr (-1)))%bool = false -> 0 <= Int.signed i0 II : 0 < Int.signed i0 H13 : (Znth (Int.signed i0) ptr & Int.repr 128)%int = 0 H14 : 0 < len ptr - Int.signed i0 D : data_at Tsh (tarray tuchar (len ptr)) (map Vint ptr) (Vptr b i) = (data_at Tsh (tarray tuchar (Int.signed i0)) (map Vint (sublist 0 (Int.signed i0) ptr)) (Vptr b i) * data_at Tsh (tarray tuchar (len (sublist (Int.signed i0) (len ptr) ptr))) (map Vint (sublist (Int.signed i0) (len ptr) ptr)) (Vptr b (i + Ptrofs.repr (Int.signed i0))%ptrofs))%logic ============================ semax Delta (PROP (True) LOCAL (temp _t'35 (Vint (Int.repr (len (tags td)))); temp _t'16 Vzero; temp _tlv_constr (Vint 0); temp _t'14 Vzero; temp _t'39 (Znth 0 (map Vint ptr)); temp _t'13 (if i0 == Int.repr (-1) then Vint 1 else Val.of_bool (i0 == Int.repr 0)); temp _tag_len (Vint i0); temp _t'40 (Vint (Int.repr (len (tags td)))); temp _tagno (Vint (Int.repr z)); temp _step (Vint (Int.repr z)); temp _expect_00_terminators (Vint (Int.repr 0)); temp _limit_len (Vint (Int.repr (-1))); temp _consumed_myself (Vint 0); lvar _rval__12 (Tstruct _asn_dec_rval_s noattr) v_rval__12; lvar _rval__11 (Tstruct _asn_dec_rval_s noattr) v_rval__11; lvar _rval__10 (Tstruct _asn_dec_rval_s noattr) v_rval__10; lvar _rval__9 (Tstruct _asn_dec_rval_s noattr) v_rval__9; lvar _rval__8 (Tstruct _asn_dec_rval_s noattr) v_rval__8; lvar _rval__7 (Tstruct _asn_dec_rval_s noattr) v_rval__7; lvar _rval__6 (Tstruct _asn_dec_rval_s noattr) v_rval__6; lvar _rval__5 (Tstruct _asn_dec_rval_s noattr) v_rval__5; lvar _rval__4 (Tstruct _asn_dec_rval_s noattr) v_rval__4; lvar _rval__3 (Tstruct _asn_dec_rval_s noattr) v_rval__3; lvar _rval__2 (Tstruct _asn_dec_rval_s noattr) v_rval__2; lvar _rval__1 (Tstruct _asn_dec_rval_s noattr) v_rval__1; lvar _rval (Tstruct _asn_dec_rval_s noattr) v_rval; lvar _tlv_len tint v_tlv_len; lvar _tlv_tag tuint v_tlv_tag; temp __res res_p; temp _opt_codec_ctx opt_codec_ctx_p; temp _td td_p; temp _opt_ctx nullval; temp _ptr (Vptr b i); temp _size (Vint (Int.repr size)); temp _tag_mode (Vint (Int.repr 0)); temp _last_tag_form (Vint (Int.repr 0)); temp _last_length last_length_p; temp _opt_tlv_form nullval) SEP (data_at Tsh (tarray tuchar (Int.signed i0)) (map Vint (sublist 0 (Int.signed i0) ptr)) (Vptr b i) * data_at Tsh (tarray tuchar (len (sublist (Int.signed i0) (len ptr) ptr))) (map Vint (sublist (Int.signed i0) (len ptr) ptr)) (Vptr b (i + Ptrofs.repr (Int.signed i0))%ptrofs); if ((i0 == Int.repr (-1)) || (i0 == 0))%bool then data_at_ Tsh tuint v_tlv_tag else data_at Tsh tuint (Vint i1) v_tlv_tag; data_at Tsh (Tstruct _asn_codec_ctx_s noattr) (Vint (Int.repr max_stack_size)) opt_codec_ctx_p; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__12; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__11; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__10; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__9; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__8; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__7; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__6; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__5; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__4; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__3; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__2; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__1; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval; data_at_ Tsh tint v_tlv_len; field_at Tsh (Tstruct _asn_TYPE_descriptor_s noattr) (DOT _tags) tags_p td_p; field_at Tsh (Tstruct _asn_TYPE_descriptor_s noattr) (DOT _tags_count) (Vint (Int.repr (len (tags td)))) td_p; data_at Tsh (tarray tuint (len (tags td))) (map Vint (map Int.repr (tags td))) tags_p; data_at_ Tsh asn_dec_rval_s res_p; data_at_ Tsh tint last_length_p)) ((_t'20 = _ber_fetch_length (_tlv_constr, ((tptr tschar) _ptr + _tag_len), (_size - _tag_len), &_tlv_len); _len_len = _t'20;) MORE_COMMANDS) POSTCONDITIONThe text was updated successfully, but these errors were encountered: