On 22/01/2019 23:08, Fabian Immler wrote:
> On 1/22/2019 4:00 PM, Fabian Immler wrote:
>> On 1/22/2019 2:28 PM, Makarius wrote:
>>> On 22/01/2019 20:05, Fabian Immler wrote:
>>>> These numbers look quite extreme:
>>>> The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
>>>> it seems to be the case with polyml-test-0a6ebca445fc).
>>>>
>>>> The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:
>>>>
>>>> ML_PLATFORM="x86-linux"
>>>> ML_OPTIONS="--minheap 2000 --maxheap 4000"
>>>> Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time,
>>>> factor 2.66)
>>>> Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time,
>>>> factor 1.46) > (I am testing HOL-ODE-ARCH-COMP with
>> polyml-test-0a6ebca445fc/x86_64_32-linux right now, but that does take
>> some time...)
> HOL-ODE-ARCH-COMP looked fine (2-3 times slower). But I realized that
> this was the case with your computations, too. Unlike Lorenz_C0:
>
>> x86_64_32-linux -minheap 1500
>> Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44)
>> x86_64-linux --minheap 3000
>> Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52)
> Lorenz_C0 had the most significant slowdown, it has the biggest number
> of parallel computations, so I thought this might be related.
>
> And indeed, if you try the theory at the end:
> Par_List.map (with 6 cores, on Windows) is 12 times slower on _64_32
> whereas the sequential evaluation is only 2 times slower.
>
> All of this reminds me of the discussion we had in November 2017:
> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2017-November/thread.html#7643
Back in Nov-2017, I made the following workaround that is still active:
http://isabelle.in.tum.de/repos/isabelle/rev/5da20135f560
Looking at the profiles of the included Float_Test.thy I now see a lot
of IntInf.divMod, but it is qualitatively similar to former IntInf.pow.
Maybe David can revisit both of these operations, so that we can get
rid of the workarounds.
Note that I have produced the profiles as follows:
isabelle build -o profiling=time ...
with a suitable test session that includes the above test theory, e.g.
see the included ROOT.
Then with "isabelle profiling_report" on the resulting log files, e.g.
isabelle profiling_report
~/.isabelle/heaps/polyml-5.7.1_x86-linux/log/Float_Test.gz
Makarius
theory Float_Test
imports
"HOL-Library.Float"
"HOL-Library.Code_Target_Numeral"
begin
definition "logistic p r x =
normfloat (float_round_down p (float_round_down p (r * x)) * (float_plus_down
p 1 (-x)))"
primrec iter where
"iter p r x 0 = x"
| "iter p r x (Suc n) = iter p r (logistic p r x) n"
definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1))
(nat_of_integer i)"
ML \<open>val logistic_chaos = @{code logistic_chaos}\<close>
ML \<open>Par_List.map logistic_chaos (replicate 10 100000)\<close>
\<comment> \<open>x86_64_32: 24s
x86_64: 2s\<close>
(*
ML \<open>map logistic_chaos (replicate 10 100000)\<close>
\<comment> \<open>x86_64_32: 16s
x86_64: 8s\<close>
*)
endsession Float_Test = "HOL-Library" +
theories
Float_Test
Float_Test:
1 eq-xsymb
1 Term_Ord.typ_ord
1 Raw_Simplifier.extract_rews
1 Output_Primitives.ignore_outputs
1 Code_Symbol.symbol_ord
1 Proofterm.thm_ord
1 Multithreading.sync_wait
1 Graph().merge_trans_acyclic
1 Scan.many
1 Basics.fold_map
1 Basics.fold
1 Pretty.string
1 Type_Infer_Context.prepare_term
1 eq-xprod
1 Term.add_tvarsT
1 Print_Mode.print_mode_value
1 X86ICodeToX86Code().icodeToX86Code
1 ProofRewriteRules.rew
1 String.fields
1 List.foldr
1 Library.insert
1 Type_Infer_Context.unify
1 Term.fold_aterms
1 Term.fastype_of1
1 Raw_Simplifier.bottomc
1 Term_Ord.fast_indexname_ord
1 Term_Subst.map_aterms_same
1 Type_Infer.add_parms
1 Axclass.unoverload
1 CODETREE_REMOVE_REDUNDANT().cleanProc
1 X86ICodeIdentifyReferences().getInstructionState
1 IntSet.minusLists
1 Term_Subst.map_types_same
1 Symbol.explode
1 Graph().add_edge
1 TYPE_TREE().eventual
1 Raw_Simplifier.rewrite_rule_extra_vars
1 Path.check_elem
1 Lazy.force_result
1 Raw_Simplifier.insert_rrule
1 Term.map_types
1 Induct().concl_var
2 Generic_Data().get
2 Logic.list_implies
2 <anon>
2 Table().join
2 IntSet.partition
2 Thm.deriv_rule2
2 X86CodetreeToICode().codeFunctionToX86
2 Thm.transfer
2 Term.fold_term_types
2 IntSet.mergeLists
2 Table().fold_table
2 Term.fold_atyps
2 Ord_List.union
2 Basics.#>
2 Term.argument_type_of
3 Raw_Simplifier.decomp_simp
3 Raw_Simplifier.eq_rrule
3 PolyAddArbitrary
3 Basics.fold_rev
3 Thm.consolidate_theory
3 Proofterm.rewrite_prf
3 PolyMultiplyArbitrary
3 Net.insert
3 Library.eq_list
3 o
4 GARBAGE COLLECTION (minor collection)
4 Sorts.insert
4 GARBAGE COLLECTION (total)
4 List.filter
4 Term.aconv
4 Term.exists_subtype
5 List.mapPartial
6 X86ICodeIdentifyReferences().identifyRegs
7 Table().lookup_key
8 List.map
9 UNKNOWN
10 eq-term
12 Table().lookup
21 Table().defined
23 Table().modify
28 eq-typ
34 PolyQuotRemArbitraryPair
59 Isabelle3896604.Generated_Code.bitlen
234 Isabelle3896604.Generated_Code.divmod_integer
307 Isabelle3896604.Generated_Code.float_plus_down
373 Isabelle3896604.Generated_Code.power
385 Par_List.forked_results
13619 IntInf.divMod
Float_Test:
1 List.mapPartial
1 Term_Ord.typ_ord
1 Raw_Simplifier.extract_rews
1 Code_Symbol.symbol_ord
1 Sorts.coregular
1 ML_Compiler.eval
1 Pretty.blanks
1 X86ICodeIdentifyReferences().identifyRegisters
1 Generic_Data().get
1 Raw_Simplifier.decomp_simp
1 Pretty.make_block
1 Type_Infer_Context.prepare_term
1 Term.could_eta_contract
1 Table().join
1 Defs.match_args
1 Term.add_tvarsT
1 Raw_Simplifier.empty_ss
1 ProofRewriteRules.rew
1 Real.fromDecimal
1 Substring.fields
1 Code_Thingol.ensure_const
1 Raw_Simplifier.bottomc
1 PolyAddArbitrary
1 Item_Net.member
1 Proof_Context.prepare_sorts_env
1 Code_ML.serialize_ml
1 Thm.transfer
1 CODETREE_REMOVE_REDUNDANT().cleanProc
1 Thread_Attributes.uninterruptible
1 CODETREE_SIMPLIFIER().simpBinary
1 X86OUTPUTCODE().expandComplexOperations
1 Table().del
1 X86ICodeIdentifyReferences().getInstructionState
1 Term.aconv
1 IntSet.mergeLists
1 X86PushRegisters().addRegisterPushes
1 Term.maxidx_typ
1 Library.eq_list
1 Library.~~
1 Table().map_table
1 Type_Infer_Context.const_type
1 Type_Infer.add_names
1 X86OUTPUTCODE().generateCode
1 Raw_Simplifier.cond_tracing'
1 Lazy.force_result
1 Proofterm.fulfill_norm_proof
1 Library.I
1 Term.exists_subterm
1 Context.join_certificate
1 ML_Compiler.report_parse_tree
1 Term.argument_type_of
1 List.@
2 Type_Infer.finish
2 <anon>
2 Thm.deriv_rule2
2 List.foldr
2 Type_Infer_Context.unify
2 Term_Ord.fast_indexname_ord
2 Term.fold_term_types
2 Axclass.unoverload
2 IntSet.minusLists
2 Net.insert
2 Raw_Simplifier.rewrite_rule_extra_vars
2 o
3 IntSet.partition
3 List.filter
3 Table().fold_rev_table
3 Term.exists_subtype
3 Raw_Simplifier.insert_rrule
4 Basics.fold
4 List.map
4 Term.fold_atyps
4 X86ICodeIdentifyReferences().identifyRegs
5 PolyMultiplyArbitrary
6 Sorts.insert
6 eq-term
8 Table().fold_table
9 Isabelle3896966.Generated_Code.float_plus_down
10 Table().lookup_key
12 GARBAGE COLLECTION (minor collection)
12 Table().lookup
12 GARBAGE COLLECTION (total)
12 Isabelle3896966.Generated_Code.power
14 Table().defined
24 Par_List.forked_results
26 PolyQuotRemArbitraryPair
26 Table().modify
35 eq-typ
64 Isabelle3896966.Generated_Code.bitlen
210 Isabelle3896966.Generated_Code.divmod_integer
222 IntInf.divMod
11786 UNKNOWN
Float_Test:
1 Code.get_type
1 List.mapPartial
1 Isabelle3896326.Generated_Code.plus_float
1 Code_Thingol.add_constsyms
1 Net.net_skip
1 GARBAGE COLLECTION (minor collection)
1 Code_Symbol.symbol_ord
1 ML_Compiler.eval
1 Type_Infer.finish
1 Ord_List.subtract
1 Scan.repeat
1 Generic_Data().get
1 Logic.list_implies
1 X86OPTIMISE().generateCode
1 GARBAGE COLLECTION (total)
1 IntSet.partition
1 Type_Infer_Context.infer
1 EXPORT_PARSETREE().getExportTree
1 Type.could_match
1 CODETREE_SIMPLIFIER().simpFunctionCall
1 Net.matching
1 Term.add_tvarsT
1 Raw_Simplifier.empty_ss
1 Term_Subst.generalize_same
1 Print_Mode.print_mode_value
1 X86ICodeToX86Code().icodeToX86Code
1 ProofRewriteRules.rew
1 Term_Subst.map_atypsT_same
1 Library.mergesort
1 Axclass.complete_classrels
1 Term.fastype_of1
1 Name_Space.merge
1 X86AllocateRegisters().allocateRegisters
1 Config.declare
1 Table().get_first
1 Axclass.unoverload
1 CODETREE_REMOVE_REDUNDANT().cleanProc
1 Basics.fold_rev
1 Code.cert_of_eqns
1 Graph().reachable
1 X86OUTPUTCODE().fixupLabels
1 IntSet.minusLists
1 Proof_Context.arity_sorts
1 ThreadLib.protect
1 Basics.#>>
1 Library.eq_list
1 Library.~~
1 Basics.try
1 UTILITIES_().splitString
1 Logic.dest_equals
1 Type_Infer.add_names
1 Raw_Simplifier.rewrite_rule_extra_vars
1 Multithreading.synchronized
1 CODETREE().genCode
1 Lazy.force_result
1 X86ICodeIdentifyReferences().identifyRegs
1 Term.exists_subterm
1 Context.join_certificate
1 Basics.#>
1 Defs.merge
1 o
1 Context_Rules.Rules.merge
1 Net.add_key_of_terms
1 List.@
2 Raw_Simplifier.extract_rews
2 Sorts.insert
2 Thm.dest_binop
2 Thm.deriv_rule2
2 List.foldr
2 Term_Ord.fast_indexname_ord
2 Thm.consolidate_theory
2 Type.cert_typ_mode
2 Term.exists_subtype
2 Raw_Simplifier.cond_tracing'
2 Basics.cons
2 Ord_List.union
2 Term.argument_type_of
3 Basics.fold
3 Table().join
3 PolyQuotRemArbitraryPair
3 Isabelle3896326.Generated_Code.float_plus_down
3 Thm.transfer
3 List.filter
3 X86ICodeIdentifyReferences().getInstructionState
3 X86ICodeOptimise().optimiseICode
3 Table().fold_table
4 Raw_Simplifier.decomp_simp
4 Table().fold_rev_table
4 Proofterm.rewrite_prf
4 Net.insert
5 Term.aconv
5 IntSet.mergeLists
6 <anon>
6 Term.fold_atyps
8 eq-term
8 Raw_Simplifier.insert_rrule
10 Table().lookup
11 Isabelle3896326.Generated_Code.power
12 Table().defined
12 List.map
15 Table().lookup_key
15 eq-typ
34 Table().modify
35 Isabelle3896326.Generated_Code.bitlen
59 Par_List.forked_results
143 Isabelle3896326.Generated_Code.divmod_integer
787 IntInf.divMod
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
