Additional timings

output/deniability/full/results_20220322.txt

@@ -0,0 +1,44 @@
+==============================================================================
+summary of summaries:
+
+analyzed: deniability/generated_kemtls_sauth_full.spthy
+
+  output:          output/generated_kemtls_sauth_full_analyzed.spthy
+  processing time: 58012.410636656s
+  DiffLemma:  Observational_equivalence : verified (174527 steps)
+
+==============================================================================
+78,169,625,134,768 bytes allocated in the heap
+49,111,990,332,216 bytes copied during GC
+  15,354,482,120 bytes maximum residency (6988 sample(s))
+      37,334,976 bytes maximum slop
+           44655 MiB total memory in use (0 MB lost due to fragmentation)
+
+                                     Tot time (elapsed)  Avg pause  Max pause
+  Gen  0     50660653 colls, 50660653 par   490925.957s  30120.057s     0.0006s    0.0246s
+  Gen  1      6988 colls,  6987 par   60128.583s  4247.110s     0.6078s    4.3875s
+
+  Parallel GC work balance: 44.94% (serial 0%, perfect 100%)
+
+  TASKS: 34 (1 bound, 33 peak workers (33 total), using -N16)
+
+  SPARKS: 224067 (75127 converted, 0 overflowed, 0 dud, 42497 GC'd, 106443 fizzled)
+
+  INIT    time    0.007s  (  0.034s elapsed)
+  MUT     time  62363.158s  (23645.931s elapsed)
+  GC      time  551054.540s  (34367.168s elapsed)
+  EXIT    time    0.665s  (  0.008s elapsed)
+  Total   time  613418.370s  (58013.140s elapsed)
+
+  Alloc rate    1,253,458,423 bytes per MUT second
+
+  Productivity  10.2% of total user, 40.8% of total elapsed
+
+
+real    966m53.939s
+user    4741m41.962s
+sys     5481m57.226s
+Tue 22 Mar 2022 01:53:45 PM CET
+
+
+(note that it yielded same output (byte-for-byte) as generated_kemtls_sauth_full_analyzed_20220112.spthy.gz)

output/kemtls_unified_sauth_20220318.txt

@@ -0,0 +1,13 @@
+
+
+[ 1/52] Proving reachable_KEMTLS_SAUTH_OR_MUTUAL_stage1_accepted1_cwfs1_swfs1     at 21:53:35.949943... Completed in   41 steps in 0:00:48.724332
+[ 2/52] Proving reachable_KEMTLS_SAUTH_stage1_accepted6_cfs_swfs1                 at 21:54:24.676169... Completed in   54 steps in 0:23:11.496669
+[ 3/52] Proving reachable_KEMTLS_SAUTH_OR_MUTUAL_stage2_accepted2_cwfs1_swfs1     at 22:17:36.173504... Completed in   41 steps in 0:00:47.129422
+[ 4/52] Proving reachable_KEMTLS_SAUTH_stage2_accepted6_cfs_swfs1                 at 22:18:23.304822... Completed in   54 steps in 0:23:36.122960
+[ 5/52] Proving reachable_KEMTLS_SAUTH_OR_MUTUAL_stage3_accepted3_cwfs2_swfs1     at 22:41:59.428693... Completed in   55 steps in 0:08:44.503361
+[ 6/52] Proving reachable_KEMTLS_SAUTH_stage3_accepted6_cfs_swfs1                 at 22:50:43.933886... Completed in   62 steps in 0:40:17.095024
+[ 7/52] Proving reachable_KEMTLS_SAUTH_OR_MUTUAL_stage4_accepted4_cwfs2_swfs1     at 23:31:01.029845... Completed in   55 steps in 0:08:41.854795
+[ 8/52] Proving reachable_KEMTLS_SAUTH_stage4_accepted6_cfs_swfs1                 at 23:39:42.886438... Completed in   62 steps in 0:40:07.926894
+[ 9/52] Proving reachable_KEMTLS_SAUTH_stage5_accepted5_cwfs2_swfs1               at 00:19:50.814302... Completed in   48 steps in 0:47:35.237407
+[10/52] Proving reachable_KEMTLS_SAUTH_stage5_accepted6_cfs_swfs1                 at 01:07:26.052595... Completed in   57 steps in 5:01:21.567581
+[11/52] Proving reachable_KEMTLS_SAUTH_stage6_accepted6_cfs_swfs1                 at 06:08:47.621006... Douglas killed it after 45 hours