TLA – Random IT Utensils https://blog.adamfurmanek.pl IT, operating systems, maths, and more. Sat, 01 Jan 2022 09:20:55 +0000 en-US hourly 1 https://wordpress.org/?v=6.5.2 TLA+ Part 2 — TLA+ to ILP Part 2 — Performance check https://blog.adamfurmanek.pl/2022/01/01/tla-part-2/ https://blog.adamfurmanek.pl/2022/01/01/tla-part-2/#comments Sat, 01 Jan 2022 09:00:14 +0000 https://blog.adamfurmanek.pl/?p=4320 Continue reading TLA+ Part 2 — TLA+ to ILP Part 2 — Performance check]]>

This is the second part of the TLA+ series. For your convenience you can find other parts in the table of contents in Part 1 — TLA+ to ILP Part 1 — Reducing problem

Let’s now carry on with adding more invariants. Tutorial says to reorder the operations, so let’s first update the db and then send the message. Now we get the following output:

Infeasibility row 'c4673':  0  = 1.
Presolve time = 0.00 sec. (2.08 ticks)

Root node processing (before b&c):
  Real time             =    0.02 sec. (3.10 ticks)
Parallel b&c, 8 threads:
  Real time             =    0.00 sec. (0.00 ticks)
  Sync time (average)   =    0.00 sec.
  Wait time (average)   =    0.00 sec.
                          ------------
Total (root+branch&cut) =    0.02 sec. (3.10 ticks)
ILOG.CPLEX.CpxException: CPLEX Error  1217: No solution exists.

   at ILOG.CPLEX.CplexI.CALL(Int32 status)
   at ILOG.CPLEX.CplexI.GetXcache()
   at ILOG.CPLEX.Cplex.GetValue(INumExpr expr)
   at CplexMilpManager.Implementation.CplexMilpSolver.GetValue(IVariable variable) in C:\Users\afish\Desktop\milpmanager\CplexMilpSolver\Implementation\CplexMilpSolver.cs:line 160
   at IlpPlayground.Program415798633.Start()
   at IlpPlayground.Env415798633.Start()

Great, it took 0.02 second to show that the invariant holds. Let’s now do it for 3 messages and at most 3 processing attempts:

Tried aggregator 4 times.
MIP Presolve eliminated 54625 rows and 31499 columns.
MIP Presolve modified 181700 coefficients.
Aggregator did 45594 substitutions.
Reduced MIP has 93725 rows, 47083 columns, and 249598 nonzeros.
Reduced MIP has 46912 binaries, 171 generals, 0 SOSs, and 0 indicators.
Presolve time = 1.23 sec. (600.55 ticks)
Probing fixed 14146 vars, tightened 199 bounds.
Probing changed sense of 57 constraints.
Probing time = 17.13 sec. (1432.87 ticks)
Cover probing fixed 0 vars, tightened 2535 bounds.
Tried aggregator 3 times.
MIP Presolve eliminated 70194 rows and 34054 columns.
MIP Presolve modified 3224 coefficients.
Aggregator did 2272 substitutions.
Reduced MIP has 21259 rows, 10757 columns, and 63444 nonzeros.
Reduced MIP has 10620 binaries, 137 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.59 sec. (231.37 ticks)
Probing fixed 24 vars, tightened 0 bounds.
Probing time = 0.22 sec. (45.46 ticks)
Cover probing fixed 0 vars, tightened 1 bounds.
Tried aggregator 2 times.
MIP Presolve eliminated 155 rows and 76 columns.
MIP Presolve modified 142 coefficients.
Aggregator did 5 substitutions.
Reduced MIP has 21099 rows, 10676 columns, and 62945 nonzeros.
Reduced MIP has 10540 binaries, 136 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.23 sec. (95.63 ticks)
Probing time = 0.08 sec. (13.65 ticks)
Cover probing fixed 0 vars, tightened 1 bounds.
Clique table members: 45984.
Tightened 1 constraints.
MIP emphasis: balance optimality and feasibility.
MIP search method: dynamic search.
Parallel mode: deterministic, using up to 8 threads.
Root relaxation solution time = 1.11 sec. (961.52 ticks)

        Nodes                                         Cuts/
   Node  Left     Objective  IInf  Best Integer    Best Bound    ItCnt     Gap

      0     0        0.0000  5881                      0.0000     1352
      0     0        0.0000  3727                  Cuts: 5374     6451
      0     0        0.0000  4197                  Cuts: 5035    11423
      0     0        0.0000  4325                  Cuts: 1023    13349
      0     2        0.0000  4253                      0.0000    13356
Elapsed time = 114.24 sec. (21523.30 ticks, tree = 0.01 MB, solutions = 0)
      1     3        0.0000  2780                      0.0000    16381
      2     4        0.0000  2843                      0.0000    17428
      3     5        0.0000  3457                      0.0000    18627
      5     7        0.0000  2934                      0.0000    21893
      6     8        0.0000  2319                      0.0000    23101
      7     9        0.0000  3013                      0.0000    25401
      9    11        0.0000  2989                      0.0000    28566
     13    15        0.0000  2920                      0.0000    31356
     14    16        0.0000  2617                      0.0000    37043
     15    17        0.0000  2912                      0.0000    46732
Elapsed time = 151.31 sec. (32512.06 ticks, tree = 0.62 MB, solutions = 0)
     20    22        0.0000  3517                      0.0000    81581
     24    26        0.0000  2902                      0.0000    88579
     26    28        0.0000  3059                      0.0000    93950
     33    35        0.0000  3015                      0.0000   103587
     40    42        0.0000  3063                      0.0000   114475
     58    60        0.0000  2399                      0.0000   125358
    114   116        0.0000  3082                      0.0000   152685
    116   118        0.0000  3189                      0.0000   161093
    226   228        0.0000  3024                      0.0000   240262
    233   235        0.0000  3373                      0.0000   254295
Elapsed time = 237.67 sec. (47212.18 ticks, tree = 2.07 MB, solutions = 0)
    241   243        0.0000  3360                      0.0000   270376
    264   266        0.0000  3985                      0.0000   296067
    333   335        0.0000  4311                      0.0000   330386
    350   352        0.0000  3411                      0.0000   338396
    388   390        0.0000  4369                      0.0000   352083
    429   427        0.0000  3566                      0.0000   364863
    500   488        0.0000  3588                      0.0000   388167
    582   533        0.0000  2617                      0.0000   420887
    609   560        0.0000  3532                      0.0000   445335
    617   568        0.0000  3525                      0.0000   452259
Elapsed time = 324.52 sec. (60798.93 ticks, tree = 52.37 MB, solutions = 0)
    625   576        0.0000  3681                      0.0000   459968
    719   639        0.0000  3013                      0.0000   502774
    760   643    infeasible                            0.0000   523214
    767   640    infeasible                            0.0000   537231
    779   644        0.0000  2605                      0.0000   554928
    801   658    infeasible                            0.0000   569934
    808   661    infeasible                            0.0000   579213
    809   660    infeasible                            0.0000   583339
    835   676    infeasible                            0.0000   628043
    843   676        0.0000  3136                      0.0000   638649
Elapsed time = 444.45 sec. (76815.67 ticks, tree = 85.60 MB, solutions = 0)
    867   682        0.0000  3764                      0.0000   669511
    901   704        0.0000  3766                      0.0000   709631
    903   704    infeasible                            0.0000   715957
    915   710        0.0000  3162                      0.0000   740255
    917   708    infeasible                            0.0000   749940
    923   712        0.0000  3709                      0.0000   761042
    943   724        0.0000  3539                      0.0000   783652
    959   728        0.0000  3137                      0.0000   798467
    967   732        0.0000  3823                      0.0000   804908
    975   738        0.0000  4172                      0.0000   815605
Elapsed time = 567.24 sec. (93862.15 ticks, tree = 93.52 MB, solutions = 0)
    983   742    infeasible                            0.0000   823977
    999   746        0.0000  3371                      0.0000   839661
   1087   780        0.0000  2492                      0.0000   902650
   1119   797        0.0000  2777                      0.0000   910464
   1199   828        0.0000  4473                      0.0000   925206
   1247   837        0.0000  4138                      0.0000   936822
   1259   841        0.0000  1225                      0.0000   940666
   1315   850        0.0000  3219                      0.0000   954899
   1351   864        0.0000  4491                      0.0000   966487
   2173   937    infeasible                            0.0000  1112720
Elapsed time = 673.52 sec. (108488.76 ticks, tree = 110.30 MB, solutions = 0)
   2189   925        0.0000  1676                      0.0000  1120865
   2209   911        0.0000   579                      0.0000  1136585
   2245   885        0.0000  1784                      0.0000  1160077
   2253   885        0.0000  1849                      0.0000  1168468
   2261   883        0.0000  1390                      0.0000  1173587
   2297   859        0.0000  2847                      0.0000  1202406
   2318   862        0.0000  3319                      0.0000  1230963
   2338   868        0.0000  3796                      0.0000  1247768
   2354   884        0.0000  4336                      0.0000  1255653
   2370   898        0.0000  3772                      0.0000  1263712
Elapsed time = 765.36 sec. (121444.90 ticks, tree = 90.82 MB, solutions = 0)
   2458   937        0.0000  3417                      0.0000  1291990
   2465   938        0.0000  3515                      0.0000  1292597
   2497   947        0.0000  3714                      0.0000  1301926
   2529   961        0.0000  4121                      0.0000  1310923
   2728   998        0.0000  4528                      0.0000  1359838
   2947  1042    infeasible                            0.0000  1421286
   2955  1040        0.0000  2800                      0.0000  1428789
   2971  1040    infeasible                            0.0000  1441818
   2996  1055        0.0000  2774                      0.0000  1461750
   3011  1062        0.0000   663                      0.0000  1471650
Elapsed time = 861.75 sec. (134254.97 ticks, tree = 121.30 MB, solutions = 0)
   3032  1061        0.0000  4411                      0.0000  1480281
   3056  1063        0.0000   634                      0.0000  1493358
   3092  1077        0.0000  2755                      0.0000  1508073
   3143  1082        0.0000  2846                      0.0000  1525295
   3370  1085        0.0000  3626                      0.0000  1603979
   3386  1097        0.0000  3260                      0.0000  1612883
   3394  1103        0.0000  4976                      0.0000  1617681
   3402  1109        0.0000  4590                      0.0000  1625703
   3434  1127        0.0000  4192                      0.0000  1642722
   3458  1135        0.0000  3135                      0.0000  1651700
Elapsed time = 955.80 sec. (147901.18 ticks, tree = 119.13 MB, solutions = 0)
   3482  1145        0.0000  4132                      0.0000  1666318
   3490  1149    infeasible                            0.0000  1671301
   3522  1162        0.0000  3943                      0.0000  1687495
   3557  1157        0.0000  3739                      0.0000  1698383
   3878  1217    infeasible                            0.0000  1793730
   3879  1218        0.0000  4304                      0.0000  1797563
   3887  1214        0.0000  4112                      0.0000  1810387
   3895  1212        0.0000  3086                      0.0000  1817630
   3911  1214    infeasible                            0.0000  1843753
   3951  1230    infeasible                            0.0000  1894774
Elapsed time = 1086.38 sec. (164678.85 ticks, tree = 138.75 MB, solutions = 0)
   3984  1239        0.0000  3560                      0.0000  1936581
   4012  1243        0.0000  4185                      0.0000  1978109
   4036  1249    infeasible                            0.0000  2008723
   4084  1273        0.0000  2249                      0.0000  2058914
   4291  1339        0.0000  3954                      0.0000  2160985
   4451  1382        0.0000  1876                      0.0000  2221480
   4523  1399        0.0000  3779                      0.0000  2243829
   4643  1402        0.0000  3522                      0.0000  2279823
   5128  1475    infeasible                            0.0000  2447189
   5160  1457        0.0000  3772                      0.0000  2483614
Elapsed time = 1361.44 sec. (209060.48 ticks, tree = 168.45 MB, solutions = 0)
   5196  1459        0.0000  1136                      0.0000  2517097
   5227  1448    infeasible                            0.0000  2548302
   5275  1434        0.0000  4369                      0.0000  2595818
   5334  1457        0.0000  3442                      0.0000  2654614
   5374  1481        0.0000  4063                      0.0000  2677172
   5438  1504        0.0000  3184                      0.0000  2715195
   5630  1540        0.0000  2624                      0.0000  2782860
   5810  1580        0.0000  3521                      0.0000  2877911
   5976  1617        0.0000  4363                      0.0000  2950026
   6000  1635        0.0000  3808                      0.0000  2981426
Elapsed time = 1643.06 sec. (254703.32 ticks, tree = 178.88 MB, solutions = 0)
   6017  1646        0.0000  3429                      0.0000  2998492
   6041  1657        0.0000  3951                      0.0000  3013795
   6105  1681        0.0000  4355                      0.0000  3044837
   6472  1723    infeasible                            0.0000  3284304
   6501  1716        0.0000  3153                      0.0000  3323608
   6510  1723        0.0000  4787                      0.0000  3346200
   6533  1732        0.0000  4333                      0.0000  3392812
   6581  1762        0.0000  1784                      0.0000  3452511
   6627  1758    infeasible                            0.0000  3508445
   6655  1758        0.0000  4502                      0.0000  3556108
Elapsed time = 1934.77 sec. (300419.53 ticks, tree = 185.01 MB, solutions = 0)
   6673  1760        0.0000  3929                      0.0000  3576293
   6716  1777        0.0000  4649                      0.0000  3622724
   6738  1775        0.0000  4594                      0.0000  3664192
   6756  1777        0.0000  3895                      0.0000  3707356
   6780  1781        0.0000  4029                      0.0000  3741195
   6820  1779    infeasible                            0.0000  3788602
   6925  1802        0.0000  3864                      0.0000  3921387
   6986  1846        0.0000  5462                      0.0000  3959989
   7042  1862        0.0000  4057                      0.0000  4000839
   7122  1900        0.0000  3414                      0.0000  4050704
Elapsed time = 2272.58 sec. (349766.51 ticks, tree = 196.05 MB, solutions = 0)
   7178  1934        0.0000  3980                      0.0000  4094289
   7210  1950        0.0000  4365                      0.0000  4118547
   7367  2016        0.0000  4163                      0.0000  4209261
   7545  2086        0.0000  1570                     -0.0000  4328399
   7549  2089        0.0000   930                     -0.0000  4335294
   7564  2097        0.0000  2319                     -0.0000  4368329
   7594  2116        0.0000  1753                     -0.0000  4428410
   7603  2120        0.0000  1992                     -0.0000  4499536
   7639  2113        0.0000  2665                     -0.0000  4567231
   7760  1876        0.0000  3345                     -0.0000  4650533
Elapsed time = 2584.36 sec. (418550.38 ticks, tree = 503.71 MB, solutions = 0)
   7787  1778    infeasible                           -0.0000  4683492
   7842  1626        0.0000  1482                     -0.0000  4751846
   7892  1516        0.0000  3149                     -0.0000  4796067
   7908  1479        0.0000  1445                     -0.0000  4815710
   7973  1275        0.0000  2715                     -0.0000  4894447
   8009  1199        0.0000  1522                     -0.0000  4933489
   8031  1145        0.0000  3088                     -0.0000  4970651
   8070  1081        0.0000  3651                     -0.0000  5020954
   8105   994    infeasible                           -0.0000  5064629
   8121   957    infeasible                           -0.0000  5090673
Elapsed time = 2814.31 sec. (465587.14 ticks, tree = 218.87 MB, solutions = 0)
   8150   917        0.0000  1817                     -0.0000  5144677
   8171   914        0.0000  2797                     -0.0000  5173548
   8203   863    infeasible                           -0.0000  5220060
   8222   828    infeasible                           -0.0000  5252533
   8255   774        0.0000  3762                     -0.0000  5302317
   8286   760    infeasible                           -0.0000  5336306
   8315   722        0.0000  2793                     -0.0000  5391932
   8348   677        0.0000  3488                     -0.0000  5441044
   8377   647        0.0000  2029                     -0.0000  5483059
   8407   624        0.0000  2980                     -0.0000  5519130
Elapsed time = 3060.86 sec. (512468.98 ticks, tree = 109.89 MB, solutions = 0)
   8433   621        0.0000  3164                     -0.0000  5562393
   8456   594    infeasible                           -0.0000  5591068
   8486   570    infeasible                           -0.0000  5637889
   8513   555        0.0000  2542                     -0.0000  5672283
   8532   541        0.0000  2665                     -0.0000  5700080
   8564   509        0.0000  2708                     -0.0000  5744187
   8612   476    infeasible                           -0.0000  5812616
   8629   460    infeasible                           -0.0000  5842067
   8658   443    infeasible                           -0.0000  5897253
   8674   431    infeasible                           -0.0000  5928058
Elapsed time = 3293.72 sec. (556670.87 ticks, tree = 50.01 MB, solutions = 0)
   8690   417        0.0000  3761                     -0.0000  5972047
   8709   401    infeasible                           -0.0000  6025153
   8726   385        0.0000  2293                     -0.0000  6058443
   8749   373        0.0000  2586                     -0.0000  6084516
   8795   341        0.0000  3357                     -0.0000  6152100
   8815   332        0.0000  3504                     -0.0000  6181099
   8839   314    infeasible                           -0.0000  6214294
   8855   287    infeasible                           -0.0000  6239941
   8888   275        0.0000  2871                     -0.0000  6305306
   8919   276        0.0000  2899                     -0.0000  6345940
Elapsed time = 3544.33 sec. (603579.54 ticks, tree = 7.73 MB, solutions = 0)
   8940   273        0.0000  3927                     -0.0000  6382370
   8963   270        0.0000  3880                     -0.0000  6426954
   8979   262        0.0000  3622                     -0.0000  6457588
   9002   259    infeasible                           -0.0000  6510739
   9038   261        0.0000  3811                     -0.0000  6575786
   9054   267        0.0000  3360                     -0.0000  6602310
   9078   261        0.0000  3308                     -0.0000  6640545
   9100   257        0.0000  4100                     -0.0000  6680438
   9136   255        0.0000  4015                     -0.0000  6733972
   9160   253        0.0000  5122                     -0.0000  6768716
Elapsed time = 3833.42 sec. (654232.38 ticks, tree = 7.51 MB, solutions = 0)
   9196   241    infeasible                           -0.0000  6830570
   9212   247        0.0000  3278                     -0.0000  6868366
   9237   252    infeasible                           -0.0000  6905455
   9267   248        0.0000  3337                     -0.0000  6949754
   9285   244    infeasible                           -0.0000  6982328
   9299   240    infeasible                           -0.0000  7007355
   9339   246        0.0000  3457                     -0.0000  7077818
   9366   237        0.0000  3578                     -0.0000  7131351
   9379   240        0.0000  3621                     -0.0000  7153049
   9411   236        0.0000  3911                     -0.0000  7197569
Elapsed time = 4127.74 sec. (697815.97 ticks, tree = 6.99 MB, solutions = 0)
   9443   232    infeasible                           -0.0000  7255603
   9459   222    infeasible                           -0.0000  7280744
   9483   222    infeasible                           -0.0000  7320997
   9507   222    infeasible                           -0.0000  7354601
   9539   224        0.0000  3142                     -0.0000  7395162
   9575   232        0.0000  3356                     -0.0000  7442675
   9603   228        0.0000  3102                     -0.0000  7484229
   9633   224        0.0000  2556                     -0.0000  7521632
   9655   216        0.0000  3543                     -0.0000  7558645
   9681   204        0.0000  2819                     -0.0000  7601679
Elapsed time = 4396.64 sec. (745122.95 ticks, tree = 6.22 MB, solutions = 0)
   9709   200        0.0000  2874                     -0.0000  7658008
   9726   199    infeasible                           -0.0000  7683572
   9743   192        0.0000  3106                     -0.0000  7712638
   9767   184    infeasible                           -0.0000  7748852
   9799   180    infeasible                           -0.0000  7789378
   9845   174        0.0000  3479                     -0.0000  7857047
   9868   169    infeasible                           -0.0000  7887777
   9887   162    infeasible                           -0.0000  7914802
   9908   155        0.0000  2762                     -0.0000  7952261
   9925   154    infeasible                           -0.0000  7978558
Elapsed time = 4668.92 sec. (789344.83 ticks, tree = 3.98 MB, solutions = 0)
   9959   146        0.0000  3402                     -0.0000  8022705
   9999   136        0.0000  3421                     -0.0000  8095320
  10020   125    infeasible                           -0.0000  8132497
  10036   115    infeasible                           -0.0000  8167324
  10068   103        0.0000  4263                     -0.0000  8215880
  10092    97    infeasible                           -0.0000  8250282
  10151    78    infeasible                           -0.0000  8327404
  10167    78    infeasible                           -0.0000  8357192
  10191    68    infeasible                           -0.0000  8387293
  10215    52    infeasible                           -0.0000  8421111
Elapsed time = 4933.30 sec. (836114.41 ticks, tree = 0.30 MB, solutions = 0)
  10240    41    infeasible                           -0.0000  8461178
  10261    28        0.0000  3434                     -0.0000  8492217
  10285    24        0.0000  3244                     -0.0000  8522078
  10322     7    infeasible                           -0.0000  8557419

GUB cover cuts applied:  46
Clique cuts applied:  94
Cover cuts applied:  2012
Implied bound cuts applied:  2216
Flow cuts applied:  1
Mixed integer rounding cuts applied:  269
Zero-half cuts applied:  215
Gomory fractional cuts applied:  4

Root node processing (before b&c):
  Real time             =  113.80 sec. (21386.31 ticks)
Parallel b&c, 8 threads:
  Real time             = 4895.06 sec. (834168.80 ticks)
  Sync time (average)   =  312.55 sec.
  Wait time (average)   =    0.01 sec.
                          ------------
Total (root+branch&cut) = 5008.86 sec. (855555.11 ticks)
ILOG.CPLEX.CpxException: CPLEX Error  1217: No solution exists.

   at ILOG.CPLEX.CplexI.CALL(Int32 status)
   at ILOG.CPLEX.CplexI.GetXcache()
   at ILOG.CPLEX.Cplex.GetValue(INumExpr expr)
   at CplexMilpManager.Implementation.CplexMilpSolver.GetValue(IVariable variable) in C:\Users\afish\Desktop\milpmanager\CplexMilpSolver\Implementation\CplexMilpSolver.cs:line 160
   at IlpPlayground.Program1159526820.Start()
   at IlpPlayground.Env1159526820.Start()

5000 seconds, that’s almost 85 minutes to prove that the invariant holds. The same takes around 2 seconds for TLA+.

]]> https://blog.adamfurmanek.pl/2022/01/01/tla-part-2/feed/ 1 TLA+ Part 1 — TLA+ to ILP Part 1 — Reducing problem https://blog.adamfurmanek.pl/2021/12/25/tla-part-1/ https://blog.adamfurmanek.pl/2021/12/25/tla-part-1/#respond Sat, 25 Dec 2021 09:00:06 +0000 https://blog.adamfurmanek.pl/?p=4313 Continue reading TLA+ Part 1 — TLA+ to ILP Part 1 — Reducing problem]]>

This is the first part of the TLA+ series. For your convenience you can find other parts using the links below:
Part 1 — TLA+ to ILP Part 1 — Reducing problem
Part 2 — TLA+ to ILP Part 2 — Performance check

Today we are going to reduce some TLA+ algorithm to ILP and see if it works. Let’s begin.

We take the Model Checking example by Tomasz Masternak from Exactly Once. It’s a short code presenting possible race conditions and issues with distributed transaction consisting of sending a message to the out queue and updating the message in a database. See the code first and understand what’s going on there as I won’t be covering it here.

Now, what we want to do is to model the same problem in ILP and see if we can get correct results. Let’s decompose the TLA+ model:

  • We have an input queue with some messages
  • We have an output queue with sent messages and their transaction id
  • We have a database storing some transaction id
  • Each message may be processed multiple times in case of failures
  • Business transaction is represented as incrementing a transaction counter
  • Message is marked as processed

We need to represent the model in ILP. We are going to store an array of bits holding messages. I’ll present this in the rough and dirty way without too much of an abstraction but in a production code you would probably encapsulate all the nasty stuff.

The code:

var integerWidth = 10;
var epsilon = 0.1;
var storeDebugExpressions = false;
var cacheConstants = false;
var storeDebugConstraints = false;

var solver = new CplexMilpSolver(new CplexMilpSolverSettings
{
	IntegerWidth = integerWidth,
	Epsilon = epsilon,
	StoreDebugExpressions = storeDebugExpressions,
	CacheConstants = cacheConstants,
	StoreDebugConstraints = storeDebugConstraints
});

var messagesCount = 1;
var retriesCount = 2;
var totalSteps = messagesCount * retriesCount;

Func<int, int> getBitsCount = maximumValue => 1 + (int)(Math.Log(maximumValue) / Math.Log(2));

var retriesBitsLength = getBitsCount(retriesCount);
var transactionBitsLength = getBitsCount(totalSteps);
var recordSize = 
	// is in queue in
	1 + 
	// is in processed
	1 + 
	// is in queue out
	1 + 
	// is in db
	1 + 
	// failures count
	retriesBitsLength + 
	// transaction id in queue
	transactionBitsLength +
	// transaction id in db
	transactionBitsLength;
	
Func<IVariable[]> createRecord = () => Enumerable.Range(0, recordSize)
	.Select(v => solver.FromConstant(0))
	.ToArray();

var bitFlags = Enumerable.Range(0, messagesCount)
	.SelectMany(step => {
		var record = createRecord();
		record[0] = solver.FromConstant(1);
		return record;
	})
	.ToArray();

Func<IVariable[], IVariable> recordToIVariable = bits => {
	int power = 1;
	IVariable result = solver.FromConstant(0);
	for(int i=bits.Length - 1;i>=0;--i){
		result = result.Operation<Addition>(bits[i].Operation<Multiplication>(solver.FromConstant(power)));
		power *= 2;
	}
	return result;
};

Func<IVariable[], int, int, IVariable> bitsToIVariable = (record, offset, length) => recordToIVariable(Enumerable.Range(offset, length)
	.Select(i => record[i]).ToArray());

Func<int, int, IVariable[]> integerToBits = (value, bitsCount) => {
	List<IVariable> result = new List<IVariable>();
	for(int i=0;i<bitsCount;++i){
		result.Add(solver.FromConstant(value % 2 == 1 ? 1 : 0));
		value /= 2;
	}
	
	result.Reverse();
	return result.ToArray();
};

Func<IVariable, int, IVariable[]> ivariableToBits = (value, bitsCount) => {
	List<IVariable> result = new List<IVariable>();
	for(int i=0;i<bitsCount;++i){
		result.Add(value.Operation<IsGreaterOrEqual>(solver.FromConstant(1)));
		value = value.Operation<Division>(solver.FromConstant(2));
	}
	
	result.Reverse();
	return result.ToArray();
};




// Just for easier debugging for development
List<IVariable> debug = new List<IVariable>();




Action<IVariable[], IVariable> failMessage = (record, hasFailed) => {
	var failuresCount = bitsToIVariable(record, 4, retriesBitsLength);
	var tooManyFailures = failuresCount
		.Operation<IsGreaterOrEqual>(solver.FromConstant(retriesCount - 1))
		.Operation<Conjunction>(hasFailed);
	
	// Remove from queue in
	record[0] = solver.Operation<Condition>(tooManyFailures, solver.FromConstant(0), record[0]);
	// Mark as processed
	record[1] = solver.Operation<Condition>(tooManyFailures, solver.FromConstant(1), record[1]);
	
	
	var newFailuresCount = solver.Operation<Condition>(tooManyFailures, failuresCount, failuresCount.Operation<Addition>(solver.FromConstant(1)));
	var newFailuresCountBits = ivariableToBits(newFailuresCount, retriesBitsLength);
	for(int i=0;i<retriesBitsLength;++i){
		record[4 + i] = solver.Operation<Condition>(hasFailed, newFailuresCountBits[i], record[4 + i]);
	}
};

List<IVariable> history = new List<IVariable>();

for(int step=0;step < totalSteps;++step){
	// Fail macro can go to the next iteration so we need to have a variable representing if we carry on with the loop
	var isStillProcessing = solver.FromConstant(1);
	
	// Receive
		// First, select some message from queue in if possible
		Func<int, IVariable> isInQueueIn = id => bitFlags[id * recordSize];
		var howManyInQueueIn = solver.Operation<Addition>(
			Enumerable.Range(0, messagesCount).Select(id => isInQueueIn(id)).ToArray()
		);
		// We know if there was any message selected thanks to "hadAnyMessageInQueueIn
		var hadAnyMessageInQueueIn = howManyInQueueIn.Operation<IsGreaterThan>(solver.FromConstant(0));
		isStillProcessing = hadAnyMessageInQueueIn;
		history.Add(isStillProcessing);
		
		var selectedMessage = solver
			.CreateAnonymous(Domain.PositiveOrZeroInteger)
			.Set<LessOrEqual>(solver.FromConstant(messagesCount - 1));
		history.Add(selectedMessage);
		
		// Now, extract bits of the message
		var selectionStartIndex = selectedMessage.Operation<Multiplication>(solver.FromConstant(recordSize));
		var currentRecord = Enumerable.Range(0, recordSize)
			.Select(i => selectionStartIndex.Operation<Addition>(solver.FromConstant(i)))
			.Select(i => solver.CompositeOperation<ArrayGet>(new ArrayGetParameters
				{
					Index = i
				}, bitFlags).ToArray().First())
			.ToArray();
		
		// Make sure that selected message is in queue (so if we're still processing then in queue must be true)
		solver.Set<Equal>(
			solver.FromConstant(1), 
			solver.Operation<MaterialImplication>(isStillProcessing, currentRecord[0])
		);
		
	
	// Process
		// This isn't exactly equivalent to the code in TLA+ as we don't keep this variable in the model
		// We'll handle this later on
		var transactionId = step + 1;
	
	// SendOutgoingMsg
		// Either fail message
		var failedInSendOutgoingMsg = solver.CreateAnonymous(Domain.BinaryInteger).Operation<Conjunction>(isStillProcessing);
		history.Add(failedInSendOutgoingMsg);
		failMessage(currentRecord, failedInSendOutgoingMsg);
		isStillProcessing = solver.Operation<Conjunction>(isStillProcessing, failedInSendOutgoingMsg.Operation<BinaryNegation>());
		
		// Or put it in queue out and set the transaction counter
		currentRecord[2] = solver.Operation<Condition>(isStillProcessing, solver.FromConstant(1), currentRecord[2]);
		var queueTransactionCounter = integerToBits(transactionId, transactionBitsLength);
		for(int i=0;i<transactionBitsLength;++i){
			currentRecord[4 + retriesBitsLength + i] = solver.Operation<Condition>(isStillProcessing, queueTransactionCounter[i], currentRecord[4 + retriesBitsLength + i]);
		}
	
	// UpdateDb
		// Either fail message
		var failInUpdateDb = solver.CreateAnonymous(Domain.BinaryInteger).Operation<Conjunction>(isStillProcessing);
		history.Add(failInUpdateDb);
		failMessage(currentRecord, failInUpdateDb);
		isStillProcessing = solver.Operation<Conjunction>(isStillProcessing, failInUpdateDb.Operation<BinaryNegation>());
		
		// Update database and set the transaction counter
		currentRecord[3] = solver.Operation<Condition>(isStillProcessing, solver.FromConstant(1), currentRecord[3]);
		var dbTransactionCounter = integerToBits(transactionId, transactionBitsLength);
		for(int i=0;i<transactionBitsLength;++i){
			currentRecord[4 + retriesBitsLength + transactionBitsLength + i] = solver.Operation<Condition>(isStillProcessing, dbTransactionCounter[i], currentRecord[4 + retriesBitsLength + transactionBitsLength + i]);
		}
	
	// AckInMsg
		// Either fail message
		var failInAck = solver.CreateAnonymous(Domain.BinaryInteger).Operation<Conjunction>(isStillProcessing);
		history.Add(failInAck);
		failMessage(currentRecord, failInAck);
		isStillProcessing = solver.Operation<Conjunction>(isStillProcessing, failInAck.Operation<BinaryNegation>());
		
		// Remove message from the in queue and mark as processed
		currentRecord[0] = solver.Operation<Condition>(isStillProcessing, solver.FromConstant(0), currentRecord[0]);
		currentRecord[1] = solver.Operation<Condition>(isStillProcessing, solver.FromConstant(1), currentRecord[1]);
	
	
	// We modified record in place and created new array elements, let's rewrite them back
	for(int i=0;i<recordSize;++i){
		solver.CompositeOperation<ArraySet>(new ArraySetParameters
			{
				Index = selectionStartIndex.Operation<Addition>(solver.FromConstant(i)),
				Value = currentRecord[i]
			}, bitFlags);
	}
}


// Now, let's now try generating ghost message
// We iterate through messages, check if any of them is ghost and make sure it's true

var isGhost = solver.FromConstant(0);
for(int i = 0; i < messagesCount; ++i){
	isGhost = isGhost.Operation<Disjunction>(solver.Operation<Conjunction>(
		// In out queue
		bitFlags[i * recordSize + 2],
		// Not in db
		bitFlags[i * recordSize + 3].Operation<BinaryNegation>()
	));
}
isGhost.Set<Equal>(solver.FromConstant(1));

solver.AddGoal("g", solver.FromConstant(0));
solver.Solve();


Func<int, int, int, double> getValue = (id, offset, length) => {
	double result = 0;
	for(int i=0; i < length; ++ i){
		result *= 2;
		var value = Math.Round(solver.GetValue(bitFlags[id * recordSize + offset + i]));
		result += value;
	}
	
	return result;
};

// This is just for easier debugging during development
foreach(var v in debug){
	Console.WriteLine(Math.Round(solver.GetValue(v)));
}

for(int i=0;i<totalSteps;++i){
	var processingInStep = Math.Round(solver.GetValue(history[i * 5])) > 0;
	Console.WriteLine("Step {0} {1} processing", i + 1, processingInStep ? "was" : "wasn't");
	Console.WriteLine("\tSelected message {0}", Math.Round(solver.GetValue(history[i * 5 + 1]) + 1));
	Console.WriteLine("\tFailure in outgoing queue {0}", Math.Round(solver.GetValue(history[i * 5 + 2])));
	Console.WriteLine("\tFailure in db {0}", Math.Round(solver.GetValue(history[i * 5 + 3])));
	Console.WriteLine("\tFailure in ack {0}", Math.Round(solver.GetValue(history[i * 5 + 4])));
}

for(int i=0;i<messagesCount;++i){
	Console.WriteLine("Message {0}", i + 1);
	Console.WriteLine("\tIn queue in: {0}", getValue(i, 0, 1));
	Console.WriteLine("\tIs processed: {0}", getValue(i, 1, 1));
	Console.WriteLine("\tIn queue out: {0}", getValue(i, 2, 1));
	Console.WriteLine("\tIn db: {0}", getValue(i, 3, 1));
	Console.WriteLine("\tFailures count: {0}", getValue(i, 4, retriesBitsLength));
	Console.WriteLine("\tTransaction id in queue: {0}", getValue(i, 4 + retriesBitsLength, transactionBitsLength));
	Console.WriteLine("\tTransaction id in database: {0}", getValue(i, 4 + retriesBitsLength + transactionBitsLength, transactionBitsLength));
}

A lot in here so let’s go line by line.

First, we initialize the solver in 1-13. Just a regular CPLEX.

Next, we store some hyperparameters: how many messages (line 15) and how many times each message can be processed (two times, line 16). We then calculate the number of all steps which solver should emulate and this is exactly number of messages times how many times we try processing a single message.

Next, we’re going to store things as bit flags so let’s define some helper function which calculates how many bits we need to store some bounded integer (line 19). It’s just a logarithm, nothing fancy (I’m running this in old .NET version so I don’t have Math.Log2 method yet…). We then calculate how many bits we need to store retries counter and transaction counter (lines 21-22).

Now, each record is going to hold the following:

  • Whether it is currently in the input queue
  • Wheter it was processed
  • Whether it’s stored in the output queue
  • Whether it’s in database
  • Retries counter
  • Transaction counter stored in the output queue
  • Transaction counter stored in the database

This is in lines 21-37.

Lovely, now an actual bit mask in lines 40-50. We initialize flags so that initially all messages are in the input queue, everything else is zeroed-out.

Next, we define some helper methods to convert bits to integer, integer to bits etc. This is in lines 52-85. We also define some collection for debug variables to be able to fix issues easier (line 91) – this doesn’t affect the model checking at all.

Okay, let’s now begin with an actual calculation. Let’s ignore failmessage for now and move on to line 117. We iterate through steps and start by defining a variable indicating whether we did a break in the loop – it’s this line in TILA+. The variable will be used in all operations. In ILP we can’t just break the iteration – we need to update all variables because we don’t know the values yet, so we use this flag to effectively do nothing.

First, we implement the Receive part. We first calculate how many messages are there in the queue (lines 123-126) and if we have a message to process (lines 128-130). Next, we define a free variable indicating which message from the queue we start processing (lines 132-135). This is an important part as we don’t process messages in any order, we are free to model race conditions, caches, network delays, or whatever else. We just get a message from the queue.

Now, we get the bits of the message to a helper array to keep things easier and faster. We use Array.Get operation which is slow (squared time complexity). We do it just once in lines 138-145.

However, since we don’t actually know how many messages there are, it may be that we select a message which was already processed. We make sure that if we selected the message then that message must have been in the queue (lines 148-151). However, if there are no more messages to process then we’ll need to emulate a no-op instructions later on.

Okay, now we move on to the business processing part. It’s trivial as it’s just a counter calculation at this point (line 157). However, later on we’ll need to emulate an assignment which in TLA+ copies values so we’ll need to copy them as well.

It’s a high time for some actual processing. We start with sending the message to the output queue in line 161. We first start by optionally failing the process. We create a free variable in line 161 which can be set only if we’re still processing (which is true at this point as nothing have failed yet). Then, we move on to the failing procedure (we call it in line 163).

The failing procedure starts by extracting the failure counter (line 97) and then checks if this message failed too many times already (lines 98-100). It’s true if and only if it was processed exactly once and it failed this time. Now we need to start performing conditional operations.
If the message failed too many times then we need to remove it from the input queue (line 103) but otherwise we don’t touch the bit at all (we rewrite its value). We do similar for processing flag – if the message failed too many times then we mark it as processed, otherwise we don’t touch the flag.

Now, we calculate the new failures count and convert it to bits (lines 108-109). We then store these bits in the record (lines 110-112).

We now carry on with processing. We update the flag indicating whether we failed and stopped the iteration (line 164). Next, we try putting the message in the output queue (line 167) and we use conditionals again – we send the message if and only if we’re still processing the loop (meaning that the message hasn’t failed too many times and hasn’t failed now). We also update the transaction counter in the same manner (lines 168-171). Notice here that we calculate the transaction counter and create new variables for it – that’s because this line effectively copies the value so we need to create a copy as well.

Next, we perform similar processing for updating the database (lines 174-185).

Finally, we acknowledge the message. We again check the failure (lines 189-192) and then update flags – remove the message from the input queue and mark it as processed.

Since we modified variables in place, we need to store them in the bitset. We do that in lines 200-206. And we’re done.

That’s it for representing the code. Now we need to model the invariant. We start with NoGhost invariant which says that either the message is not in the output queue or it’s stored in the database. So we get each message one by one and check whether it’s in the input queue (line 217) and it’s not in the database (line 219) – in that case the message is ghost We finally add the constraint that this must be true so there must be some ghost message (line 222). If ILP solver finds an evaluation and shows a solution then it means that the invariant was broken and that the business code is wrong. If ILP fails to find a solution – it means that the invariant holds.

Now, we need some code to actually retrieve the history in a friendly manner (lines 228-262). And we’re done. Output:

Tried aggregator 5 times.
MIP Presolve eliminated 7077 rows and 4313 columns.
MIP Presolve modified 2809 coefficients.
Aggregator did 722 substitutions.
Reduced MIP has 122 rows, 70 columns, and 365 nonzeros.
Reduced MIP has 57 binaries, 13 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.02 sec. (12.70 ticks)
Found incumbent of value 0.000000 after 0.02 sec. (14.35 ticks)

Root node processing (before b&c):
  Real time             =    0.02 sec. (14.53 ticks)
Parallel b&c, 8 threads:
  Real time             =    0.00 sec. (0.00 ticks)
  Sync time (average)   =    0.00 sec.
  Wait time (average)   =    0.00 sec.
                          ------------
Total (root+branch&cut) =    0.02 sec. (14.53 ticks)
Step 1 was processing
        Selected message 1
        Failure in outgoing queue 1
        Failure in db 0
        Failure in ack 0
Step 2 was processing
        Selected message 1
        Failure in outgoing queue 0
        Failure in db 1
        Failure in ack 0
Message 1
        In queue in: 0
        Is processed: 1
        In queue out: 1
        In db: 0
        Failures count: 1
        Transaction id in queue: 2
        Transaction id in database: 0

How do we read that? First, it took 0.02 second to find that the invariant is broken. We can see that in the first loop iteration was processing a message (so there was still something in the input queue), chose first message from the queue, and then failed when putting it in the output queue. Step 2 tried doing the same and succeeded, but later failed when updating the message in the database. Finally, we can see that the message is not in the input queue, was processed, is in the output queue but not in the database. We can also see the failures count set to one and that the transaction id was stored correctly in the output queue.

Next time we’re going to experiment with other invariants, and later on we’ll run some performance tests.

]]> https://blog.adamfurmanek.pl/2021/12/25/tla-part-1/feed/ 0