Skip to content
Snippets Groups Projects
Select Git revision
  • de7747349ba4bc926cc96caa3b38cdb9cf7e1eed
  • master default protected
  • btypes-fixes
  • freetypes
  • embedded-codegen
  • rust-support
  • z3solver
7 results

README.md

Blame
    • Fabian Vu's avatar
    Update README.md
    Fabian Vu authored and GitHub committed
    de774734
    History
    Fabian Vu's avatar de774734
    History
    Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    README.md 9.19 KiB

    Benchmarks

    Execution

    Executing benchmarks is done by executing make in each of the directories.

    Technical Data

    • Java: Java HotSpot(TM) 64-Bit Server VM (build 15+36-1562, mixed mode, sharing)
    • C++ Compiler: Apple clang version 13.0.0 (clang-1300.0.29.30) with -O1 and -O2
    • ProB: 1.9.0-nightly (b6d1b600dbf06b7984dd2a1dd7403206cfd9d394)
    • B2Program Commit: 4ba7747d
    • Device: MacBook Air with 8 GB of RAM and a 1.6 GHz Intel i5 processor with two cores

    Results

    Single-threaded

    Machines ProB OP ProB ST TLC Java C++ -O1 C++ -O2
    Counter Runtime 90.06 87.98 8.52 3.24 / 5.16 1.29 / 5.88 1.28 / 5.84
    Speed-up 1 1.02 10.67 27.84 / 17.47 70.08 / 15.33 70.63 / 15.42
    Memory 1151604 1151556 335420 421034 / 654880 217920 / 878754 217940 / 878780
    Cruise Controller Runtime 0.75 1.74 6.89 1.6 / 1.53 0.06 / 0.16 0.06 / 0.15
    Speed-up 1 0.11 0.15 0.47 / 0.49 12.5 / 4.69 12.5 / 5
    Memory 174954 174247 172016 121832 / 113110 2722 / 10912 2788 / 11040
    Landing Gear Runtime 36.85 188.87 25.68 18.23 / 17.22 15.1 / 34.38 14.98 / 33.36
    Speed-up 1 0.2 1.51 2.12 / 2.44 2.56 / 1.12 2.58 / 1.16
    Memory 476783 469995 681308 751508 / 985684 186736 / 1053604 186726 / 1053642
    CAN BUS Runtime 23.13 52.11 11.42 6.23 / 7.21 3.77 / 10.29 3.7 / 9.85
    Speed-up 1 0.44 2.03 3.71 / 3.2 6.14 / 2.25 6.26 / 2.35
    Memory 353338 352125 461096 450596 / 562440 196762 / 677544 196708 / 677734
    Train_6 Runtime 21.92 55.09 19.02 18.96 / 17.13 13.77 / 8.56 13.71 / 8.29
    Speed-up 1 0.4 1.15 1.16 / 1.28 1.59 / 2.56 1.6 / 2.64
    Memory 278126 204090 348272 479204 / 854666 43414 / 108370 43418 / 108410
    Train_10 Runtime 776.81 2564.03 2373.16 1004.45 / 799.37 940.32 / 533.78 924.577 / 520.63
    Speed-up 1 0.3 0.33 0.77 / 0.97 0.83 / 1.46 0.84 / 1.49
    Memory 2995244 1278929 896422 1267960 / 2317640 1228082 / 2995064 1228102 / 2995000
    nota Runtime 29.89 178.82 18.78 21.89 / 20.9 88.51 / 157.8 89.48 / 157.9
    Speed-up 1 0.17 1.59 1.37 / 1.43 0.34 / 0.19 0.33 / 0.19
    Memory 947413 946857 883470 974294 / 1063392 189306 / 993818 189344 / 993864
    sort_1000 Runtime 234.97 359.23 505.1 1365.79 / 146.72 3288.73 / 3468.77 3244.62 / 3473.78
    Speed-up 1 0.65 0.47 0.15 / 1.6 0.07 / 0.07 0.07 / 0.06
    Memory 833697 602163 374906 521224 / 1314720 303293 / 947840 303300 / 947864
    N Queens (N=4) Runtime 0.15 0.19 6.46 61.97 / 61.19 57.05 / 57.02 56.43 / 55.73
    Speed-up 1 0.79 0.02 0.002 / 0.002 0.003 / 0.003 0.003 / 0.003
    Memory 166608 166574 170972 351168 / 349608 48892 / 48886 48998 / 48996
    N Queens (N=8) Runtime 0.46 0.56 278 > 3600 / > 3600 > 3600 / > 3600 > 3600 / > 3600
    Speed-up 1 0.83 0.002 < 0.001 / < 0.001 < 0.001 / < 0.001 < 0.001 / < 0.001
    Memory 166907 166872 255230 - / - - / - - / -

    Multi-threaded (6 Threads)

    Machines TLC Java C++ -O1 C++ -O2
    Counter Runtime 11.79 22.98 / 26.34 17.55 / 24.47 17.62 / 24.47
    Speed-up to TLC 1 0.51 / 0.45 0.67 / 0.48 0.67 / 0.48
    Speed-up to 1 TH 0.73 0.15 / 0.2 0.07 / 0.24 0.07 / 0.24
    Memory 294664 398248 / 728514 218086 / 878910 218078 / 878928
    Cruise Controller Runtime 6.86 1.68 / 1.6 0.06 / 0.15 0.05 / 0.15
    Speed-up to TLC 1 4.1 / 4.3 114.33 / 45.73 137.2 / 45.73
    Speed-up to 1 TH 1 0.96 / 0.96 1 / 1.07 1.2 / 1
    Memory 172032 147498 / 142246 3048 / 10994 3086 / 11150
    Landing Gear Runtime 19.76 14.49 / 14.56 11.54 / 27.29 11.3 / 27.35
    Speed-up to TLC 1 1.36 / 1.36 1.71 / 0.72 1.75 / 0.72
    Speed-up to 1 TH 1.3 1.26 / 1.18 1.31 / 1.26 1.33 / 1.22
    Memory 808976 954956 / 1179980 195566 / 1056952 195590 / 1057498
    CAN BUS Runtime 13.4 6.78 / 7.53 3.61 / 11.03 3.53 / 10.89
    Speed-up to TLC 1 1.98 / 1.78 3.72 / 1.21 3.8 / 1.23
    Speed-up to 1 TH 0.85 0.92 / 0.96 1.04 / 0.93 1.05 / 0.9
    Memory 468646 498644 / 574292 204528 / 687058 204572 / 687424
    Train_6 Runtime 15.33 12.54 / 11.97 8.56 / 5.44 8.42 / 5.4
    Speed-up to TLC 1 1.22 / 1.28 1.79 / 2.82 1.82 / 2.84
    Speed-up to 1 TH 1.24 1.51 / 1.43 1.61 / 1.57 1.63 / 1.54
    Memory 468646 725776 / 1077684 204528 / 687058 204572 / 687424
    Train_10 Runtime 1482.03 459.81 / 421.8 536.21 / 318.4 532.94 / 316.53
    Speed-up to TLC 1 3.22 / 3.51 2.76 / 4.65 2.78 / 4.68
    Speed-up to 1 TH 1.6 2.18 / 1.9 1.75 / 1.68 1.73 / 1.64
    Memory 1077022 1456166 / 2340918 1261254 / 3164336 1261022 / 3164792
    nota Runtime 16.1 16.87 / 19.56 97.37 / 181.08 97 / 179.75
    Speed-up to TLC 1 0.95 / 0.82 0.17 / 0.09 0.17 / 0.09
    Speed-up to 1 TH 1.17 1.3 / 1.07 0.91 / 0.87 0.92 / 0.88
    Memory 898580 1100700 / 1138802 220748 / 1035806 218750 / 1035398
    sort_1000 Runtime 306.13 663.23 / 79.55 1504 / 1613.77 1496.86 / 1580.33
    Speed-up to TLC 1 0.46 / 3.84 0.2 / 0.19 0.2 / 0.19
    Speed-up to 1 TH 1.65 2.06 / 1.85 2.19 / 2.15 2.17 / 2.2
    Memory 503360 520850 / 1894494 304048 / 948392 304058 / 948402
    N Queens (N=4) Runtime 6.44 58.68 / 60.18 56.5 / 56.13 54.99 / 55.14
    Speed-up to TLC 1 0.11 / 0.11 0.11 / 0.11 0.12 / 0.12
    Speed-up to 1 TH 1.0 1.06 / 1.02 1.01 / 1.02 1.03 / 1.01
    Memory 170934 360534 / 350706 49026 / 48920 49012 / 49018
    N Queens (N=8) Runtime 190.72 > 3600 / > 3600 > 3600 / > 3600 > 3600 / > 3600
    Speed-up to TLC 1 < 0.01 / < 0.01 < 0.01 / < 0.01 < 0.01 / < 0.01
    Speed-up to 1 TH 1.46 - / - - / - - / -
    Memory 260730 - / - - / - - / -

    Runtime in Seconds

    Memory Usage in KB

    OP = Operation Reuse

    ST = Standard

    TH = Thread

    Entries as v1/v2 for without/with caching