Raft tracing - Githubissues

achamayou commented 1 year ago

Moves changes from https://github.com/lemmy/CCF/tree/mku-gh5057 to main, to make progress on #5057. Thank you @lemmy for doing all the work on this!

Introduce a -DCCF_RAFT_TRACING=ON, wired to an ifdef, to make sure there is no impact on release builds. This will require a separate sub-job in the CI at first, probably merged into the Debug build if the performance impact does not lead to timeouts on end to end tests.

Next steps:

[x] Consolidate leadership and membership into state #5203
[x] Emit configurations in addconfiguration and become* functions
[x] Comparison pass with https://github.com/microsoft/CCF/compare/main...lemmy:CCF:mku-gh5057 to confirm all events are covered
[x] Slight tangent to clean up existing states #5207
[x] Adjust field names in trace spec as necessary
[x] CI should update traces every time

ccf-bot commented 1 year ago

raft_tracing@69517 aka 20230426.16 vs main ewma over 20 builds from 68997 to 69502

Click to see table

main | build_id | build_number | Commit latency factor | tpcc_virtual_cft^ | tpcc_sgx_cft^ | tpcc_sgx_cft_mem | ls_virtual_cft^ | pi_ls_virtual_cft^ | ls_jwt_virtual_cft^ | pi_ls_jwt_virtual_cft^ | ls_sgx_cft^ | ls_sgx_cft_mem | pi_ls_sgx_cft^ | pi_ls_sgx_cft_mem | ls_js_virtual_cft^ | ls_jwt_sgx_cft^ | ls_jwt_sgx_cft_mem | ls_full_js_virtual_cft^ | pi_ls_jwt_sgx_cft^ | pi_ls_jwt_sgx_cft_mem | ls_js_jwt_virtual_cft^ | ls_js_sgx_cft^ | ls_js_sgx_cft_mem | hist_sgx_cft^ | ls_full_js_sgx_cft^ | ls_full_js_sgx_cft_mem | ls_js_jwt_sgx_cft^ | ls_js_jwt_sgx_cft_mem | RB put (/s)^ | CHAMP put (/s)^ | RB get (/s)^ | CHAMP get (/s)^ | |-----------:|:---------------|------------------------:|--------------------:|----------------:|-------------------:|------------------:|---------------------:|----------------------:|-------------------------:|--------------:|-----------------:|-----------------:|--------------------:|---------------------:|------------------:|---------------------:|--------------------------:|---------------------:|------------------------:|-------------------------:|-----------------:|--------------------:|----------------:|----------------------:|-------------------------:|---------------------:|------------------------:|---------------:|------------------:|---------------:|------------------:| | 68997 | 20230420.14 | 0.792012 | 17137.2 | 7302.33 | 8.59996e+07 | 45655.5 | 48700.7 | 12387.9 | 13035.6 | 19997.4 | 1.88908e+07 | 20123.4 | 1.25993e+07 | 4426.75 | 6401.15 | 1.67936e+07 | 3722.53 | 6467.4 | 6.30784e+06 | 3274.58 | 1709.34 | 1.05021e+07 | 45595.4 | 1485.23 | 1.05021e+07 | 1403.14 | 1.05021e+07 | 800374 | 1.17785e+06 | 8.15261e+06 | 3.07785e+07 | | 69009 | 20230420.17 | 0.790821 | 17425.2 | 7310.58 | 8.59996e+07 | 45832 | 48743.9 | 12420.5 | 12895.6 | 20055.5 | 1.88908e+07 | 20194 | 1.25993e+07 | 4451.21 | 6347.31 | 1.67936e+07 | 3736.96 | 6493.7 | 6.30784e+06 | 3246.12 | 1709.53 | 1.05021e+07 | 45249.2 | 1500.66 | 1.05021e+07 | 1395.68 | 1.05021e+07 | 833060 | 1.17626e+06 | 8.15115e+06 | 3.07891e+07 | | 69017 | 20230420.19 | 0.799441 | 17436.4 | 7283.31 | 8.59996e+07 | 45580.1 | 42499 | 12425.3 | 13071.1 | 19982.9 | 1.88908e+07 | 20219.1 | 1.05021e+07 | 4444.03 | 6314.25 | 1.67936e+07 | 3745.16 | 6479.2 | 6.30784e+06 | 3250.18 | 1703.89 | 1.05021e+07 | 50727.6 | 1501.96 | 1.05021e+07 | 1396.86 | 1.05021e+07 | 832303 | 1.17936e+06 | 8.15329e+06 | 3.08123e+07 | | 69035 | 20230420.26 | 0.806502 | 17310.8 | 7305.62 | 8.59996e+07 | 45514.6 | 48604.3 | 12414.3 | 12963.1 | 20046.5 | 1.88908e+07 | 20312.6 | 1.25993e+07 | 4447.81 | 6670.29 | 1.67936e+07 | 3758.04 | 6504.1 | 6.30784e+06 | 3349.17 | 1717 | 1.05021e+07 | 50978.6 | 1507.4 | 1.05021e+07 | 1402.82 | 1.05021e+07 | 832273 | 1.17067e+06 | 8.15598e+06 | 3.07549e+07 | | 69046 | 20230421.3 | 0.808997 | 17343.1 | 7334.05 | 8.59996e+07 | 45857 | 48755.7 | 12415.9 | 12909.2 | 20037 | 1.88908e+07 | 20258.7 | 1.25993e+07 | 4444.69 | 6675.63 | 1.67936e+07 | 3764.34 | 6500.1 | 6.30784e+06 | 3343.89 | 1710.3 | 1.05021e+07 | 47196.3 | 1508.63 | 1.05021e+07 | 1420.93 | 1.05021e+07 | 833669 | 1.18037e+06 | 8.16314e+06 | 3.03596e+07 | | 69139 | 20230421.25 | 0.78317 | 17287.6 | 7348.46 | 8.59996e+07 | 45595.2 | 48950.5 | 12425.8 | 13176.8 | 20000.3 | 1.88908e+07 | 20253.3 | 1.25993e+07 | 4465.41 | 6353.38 | 1.67936e+07 | 3756.29 | 6496.3 | 6.30784e+06 | 3362.34 | 1717.15 | 1.05021e+07 | 51217.1 | 1494.63 | 1.05021e+07 | 1406.31 | 1.05021e+07 | 833686 | 1.1848e+06 | 8.15475e+06 | 3.08132e+07 | | 69154 | 20230421.29 | 0.802427 | 17131.1 | 7269.41 | 8.59996e+07 | 45648.7 | 48788.1 | 12343.2 | 12999.8 | 20104.7 | 1.88908e+07 | 20383.3 | 1.05021e+07 | 4450.33 | 6386.47 | 1.67936e+07 | 3738.58 | 6463.5 | 6.30784e+06 | 3375.52 | 1701.96 | 1.05021e+07 | 46933.3 | 1485.2 | 1.05021e+07 | 1393.66 | 1.05021e+07 | 832759 | 1.17809e+06 | 8.1529e+06 | 3.07766e+07 | | 69170 | 20230421.35 | 0.802505 | 17510.3 | 7357.12 | 8.59996e+07 | 45912.7 | 48691.7 | 12428.3 | 12846.2 | 19957 | 1.88908e+07 | 20287.5 | 1.25993e+07 | 4466.23 | 6368.78 | 1.67936e+07 | 3740.62 | 6564.1 | 6.30784e+06 | 3275.97 | 1717.62 | 1.05021e+07 | 50791 | 1493.29 | 1.05021e+07 | 1405.73 | 1.05021e+07 | 830300 | 1.17624e+06 | 8.13874e+06 | 3.05663e+07 | | 69177 | 20230421.37 | 0.770609 | 17321.4 | 7284.78 | 8.39025e+07 | 47653.4 | 48592.8 | 12422.4 | 13005.4 | 19977.3 | 1.88908e+07 | 20249.6 | 1.25993e+07 | 4406.13 | 6332.71 | 1.67936e+07 | 3759.82 | 6507.5 | 6.30784e+06 | 3268.74 | 1716.13 | 1.05021e+07 | 49258 | 1494.02 | 1.05021e+07 | 1404.73 | 1.05021e+07 | 835942 | 1.18082e+06 | 8.15176e+06 | 3.07905e+07 | | 69216 | 20230424.3 | 0.793444 | 17407.1 | 7330.33 | 8.59996e+07 | 45684.2 | 48998.7 | 12444.4 | 12962.6 | 20101.5 | 1.88908e+07 | 20236 | 1.25993e+07 | 4420.6 | 6362.08 | 1.67936e+07 | 3748.1 | 6514.6 | 6.30784e+06 | 3360.91 | 1733.53 | 1.05021e+07 | 48968.5 | 1494.11 | 1.05021e+07 | 1398.69 | 1.05021e+07 | 833367 | 1.18008e+06 | 8.15524e+06 | 3.13337e+07 | | 69218 | 20230424.4 | 0.821944 | 17648.7 | 7241.23 | 8.59996e+07 | 45880.5 | 49149.9 | 12477.3 | 12300.7 | 19761.4 | 1.88908e+07 | 20108.4 | 1.25993e+07 | 4307.96 | 6369.46 | 1.67936e+07 | 3729.97 | 6376.7 | 6.30784e+06 | 3261.57 | 1688.89 | 1.05021e+07 | 47626.4 | 1473.32 | 1.05021e+07 | 1385.57 | 1.05021e+07 | 839242 | 1.17259e+06 | 8.15602e+06 | 3.08127e+07 | | 69298 | 20230424.24 | 0.795807 | 17333.1 | 7272.07 | 8.59996e+07 | 46008.8 | 47982.6 | 12481 | 12914.9 | 20014.4 | 1.88908e+07 | 20317.6 | 1.25993e+07 | 4416.53 | 6385.7 | 1.67936e+07 | 3726.29 | 6508 | 6.30784e+06 | 3283.25 | 1710.58 | 1.05021e+07 | 46954.2 | 1492.63 | 1.05021e+07 | 1406.54 | 1.05021e+07 | 830162 | 1.17161e+06 | 8.15511e+06 | 3.07609e+07 | | 69306 | 20230424.26 | 0.780244 | 17327.1 | 7245.16 | 8.59996e+07 | 45550.8 | 48243.2 | 12551.8 | 12942 | 19908.9 | 1.88908e+07 | 20170.4 | 1.25993e+07 | 4395.81 | 6342.31 | 1.67936e+07 | 3729.08 | 6374.4 | 6.30784e+06 | 3375.66 | 1686.75 | 1.05021e+07 | 50172.8 | 1470.73 | 1.05021e+07 | 1390.98 | 1.05021e+07 | 820794 | 1.18045e+06 | 8.15407e+06 | 3.04989e+07 | | 69346 | 20230425.3 | 0.794321 | 17460.3 | 7327.19 | 8.59996e+07 | 45808 | 47678.7 | 12399.4 | 13163.4 | 20054 | 1.88908e+07 | 20355.1 | 1.25993e+07 | 4454.15 | 6331.12 | 1.67936e+07 | 3739.58 | 6501.1 | 6.30784e+06 | 3278.42 | 1712.05 | 1.05021e+07 | 51117.9 | 1490.52 | 1.05021e+07 | 1409.17 | 1.05021e+07 | 827591 | 1.17402e+06 | 8.17245e+06 | 3.08151e+07 | | 69378 | 20230425.13 | 0.76443 | 17374.6 | 7273.57 | 8.59996e+07 | 45662.3 | 48586.3 | 12547.5 | 12873.5 | 20210.9 | 1.88908e+07 | 20290.5 | 1.25993e+07 | 4442.27 | 6334.03 | 1.67936e+07 | 3738.52 | 6507.2 | 6.30784e+06 | 3252.24 | 1726.86 | 1.05021e+07 | 49594.9 | 1504.02 | 1.05021e+07 | 1417.86 | 1.05021e+07 | 838031 | 1.18088e+06 | 8.14933e+06 | 3.09773e+07 | | 69394 | 20230425.17 | 0.778737 | 17698 | 7293.32 | 8.59996e+07 | 45996.3 | 48943.6 | 12609.2 | 13178.4 | 20085.4 | 1.88908e+07 | 20276.3 | 1.25993e+07 | 4457.65 | 6378.77 | 1.67936e+07 | 3758.17 | 6470.7 | 6.30784e+06 | 3279.52 | 1710.94 | 1.05021e+07 | 46568.4 | 1505.48 | 1.05021e+07 | 1415.56 | 1.05021e+07 | 832304 | 1.18022e+06 | 8.16704e+06 | 3.02252e+07 | | 69411 | 20230425.24 | 0.781021 | 17424 | 7300.28 | 8.39025e+07 | 45536.8 | 47962.6 | 12584.4 | 13014.4 | 20073.9 | 1.88908e+07 | 20292.6 | 1.25993e+07 | 4456.87 | 6677.37 | 1.67936e+07 | 3737.94 | 6508.5 | 6.30784e+06 | 3273.81 | 1709.79 | 1.05021e+07 | 48534.4 | 1504.84 | 1.05021e+07 | 1396.68 | 1.05021e+07 | 824293 | 1.18376e+06 | 8.15111e+06 | 3.08387e+07 | | 69477 | 20230426.6 | 0.798463 | 17160.5 | 7356.01 | 8.59996e+07 | 45858.9 | 47629.3 | 12493.1 | 13180.9 | 20011 | 1.88908e+07 | 20305.1 | 1.25993e+07 | 4390.06 | 6418.03 | 1.67936e+07 | 3725.08 | 6556.4 | 6.30784e+06 | 3362.2 | 1730.48 | 1.05021e+07 | 46080.9 | 1492.55 | 1.05021e+07 | 1420.5 | 1.05021e+07 | 833610 | 1.17569e+06 | 8.07307e+06 | 3.07378e+07 | | 69482 | 20230426.8 | 0.773344 | 17411.1 | 7329.38 | 8.39025e+07 | 45585 | 47906.2 | 12463.9 | 12815.9 | 20114.3 | 1.88908e+07 | 20318.1 | 1.25993e+07 | 4473.52 | 6723.21 | 1.67936e+07 | 3753.63 | 6560 | 6.30784e+06 | 3232.9 | 1713.04 | 1.05021e+07 | 43933.3 | 1506.26 | 1.05021e+07 | 1403.46 | 1.05021e+07 | 831077 | 1.17801e+06 | 8.15335e+06 | 3.08109e+07 | | 69502 | 20230426.13 | 0.787383 | 17406.3 | 7201.22 | 8.59996e+07 | 45787.2 | 48282.6 | 12726.1 | 13293.8 | 19853 | 1.88908e+07 | 20160.4 | 1.25993e+07 | 4444.7 | 6339.72 | 1.67936e+07 | 3725.19 | 5812.1 | 6.30784e+06 | 3355.15 | 1702.87 | 1.05021e+07 | 45788.7 | 1471.65 | 1.05021e+07 | 1378.02 | 1.05021e+07 | 833835 | 1.17237e+06 | 8.04083e+06 | 3.10378e+07 | raft_tracing | build_id | build_number | Commit latency factor | tpcc_virtual_cft^ | tpcc_sgx_cft^ | tpcc_sgx_cft_mem | ls_virtual_cft^ | pi_ls_virtual_cft^ | ls_jwt_virtual_cft^ | pi_ls_jwt_virtual_cft^ | ls_sgx_cft^ | ls_sgx_cft_mem | ls_js_virtual_cft^ | pi_ls_sgx_cft^ | pi_ls_sgx_cft_mem | ls_jwt_sgx_cft^ | ls_jwt_sgx_cft_mem | ls_full_js_virtual_cft^ | pi_ls_jwt_sgx_cft^ | pi_ls_jwt_sgx_cft_mem | ls_js_jwt_virtual_cft^ | ls_js_sgx_cft^ | ls_js_sgx_cft_mem | hist_sgx_cft^ | ls_full_js_sgx_cft^ | ls_full_js_sgx_cft_mem | ls_js_jwt_sgx_cft^ | ls_js_jwt_sgx_cft_mem | RB put (/s)^ | CHAMP put (/s)^ | RB get (/s)^ | CHAMP get (/s)^ | |-----------:|:---------------|------------------------:|--------------------:|----------------:|-------------------:|------------------:|---------------------:|----------------------:|-------------------------:|--------------:|-----------------:|---------------------:|-----------------:|--------------------:|------------------:|---------------------:|--------------------------:|---------------------:|------------------------:|-------------------------:|-----------------:|--------------------:|----------------:|----------------------:|-------------------------:|---------------------:|------------------------:|---------------:|------------------:|---------------:|------------------:| | 69462 | 20230426.2 | 0.777822 | 17190.2 | 7367.72 | 8.59996e+07 | 45667.9 | 47354.7 | 12541.1 | 13172.8 | 20161 | 1.88908e+07 | 4436.21 | 20268.6 | 1.25993e+07 | 6362.56 | 1.67936e+07 | 3721.51 | 6428.6 | 6.30784e+06 | 3360.75 | 1712.19 | 1.05021e+07 | 46274.9 | 1500.87 | 1.05021e+07 | 1402.46 | 1.05021e+07 | 827902 | 1.18261e+06 | 8.15416e+06 | 3.08383e+07 | | 69467 | 20230426.3 | 0.762417 | 17363.1 | 7266.81 | 8.59996e+07 | 45500.1 | 47758.7 | 12460.3 | 12734 | 19849.7 | 1.88908e+07 | 4443.71 | 20085 | 1.25993e+07 | 6336.82 | 1.67936e+07 | 3735.78 | 6341.6 | 6.30784e+06 | 3256.33 | 1685.16 | 1.05021e+07 | 47878.1 | 1480.79 | 1.05021e+07 | 1393.05 | 1.05021e+07 | 833099 | 1.17755e+06 | 8.15556e+06 | 3.14752e+07 | | 69495 | 20230426.10 | 0.817491 | 17315 | 7305.71 | 8.39025e+07 | 45726.9 | 47512.7 | 12733.5 | 13217.6 | 20061.3 | 1.88908e+07 | 4428.72 | 20264.5 | 1.25993e+07 | 6681.74 | 1.67936e+07 | 3737.74 | 6507.6 | 6.30784e+06 | 3340.22 | 1716.8 | 1.05021e+07 | 51346 | 1506.33 | 1.05021e+07 | 1404.87 | 1.05021e+07 | 830617 | 1.1843e+06 | 8.15455e+06 | 3.06757e+07 | | 69508 | 20230426.14 | 0.773002 | 17382.5 | 7304.73 | 8.59996e+07 | 45565.9 | 47127.1 | 12358.6 | 13101.5 | 19984.8 | 1.88908e+07 | 4415.23 | 20167.1 | 1.25993e+07 | 6328.77 | 1.67936e+07 | 3721.71 | 6455.1 | 6.30784e+06 | 3261.21 | 1706.48 | 1.05021e+07 | 51193 | 1491.75 | 1.05021e+07 | 1404.04 | 1.05021e+07 | 831903 | 1.1822e+06 | 8.14794e+06 | 3.08448e+07 | | 69517 | 20230426.16 | 0.792253 | 17341.5 | 7335.48 | 8.39025e+07 | 45926.7 | 47739.3 | 12412.6 | 12991.6 | 20035.9 | 1.88908e+07 | 4219.83 | 20304.1 | 1.25993e+07 | 6385.8 | 1.67936e+07 | 3759.81 | 6555.5 | 6.30784e+06 | 3286.8 | 1717.72 | 1.05021e+07 | 50441.4 | 1509.95 | 1.05021e+07 | 1403.99 | 1.05021e+07 | 821884 | 1.18273e+06 | 8.15365e+06 | 3.07924e+07 |

images

lemmy commented 1 year ago

https://github.com/microsoft/CCF/pull/5200 https://github.com/microsoft/CCF/commit/382a7c7aff0453bd99116fb5ccd5ce17cec21604 https://github.com/microsoft/CCF/commit/db8343c798515d3f036d3a656db85912c196118d

lemmy commented 1 year ago

I'd prefer not to deal with null in the trace spec. As a matter of fact, the JSON module doesn't even handle null.

On April 25, 2023 12:51:41 AM PDT, Amaury Chamayou @.***> wrote:

@achamayou commented on this pull request.

@@ -178,4 +176,15 @@ namespace aft std::optional leadership_state = std::nullopt; kv::MembershipState membership_state = kv::MembershipState::Active; };

DECLARE_JSON_TYPE(State);

DECLARE_JSON_REQUIRED_FIELDS(

State,

node_id,

current_view,

last_idx,

commit_idx,

watermark_idx,

new_view_idx,

leadership_state,

This is because of the switch to our standard JSON serialisation macros, and away from the custom leadership_state_string() which had been used on https://github.com/microsoft/CCF/compare/main...lemmy:CCF:mku-gh5057/.

There are three options:

Write a custom serialiser for State just for this. Distinctly unappealing.

Stay with null and update the trace spec. Not sure how annoying this is.

Add a None state to the LeadershipState enum, and remove the optional. I think that's what I would prefer, optional initial state feels strange, and we have very little of it (I think this may be the only bit).

achamayou commented 1 year ago

I'd prefer not to deal with null in the trace spec. As a matter of fact, the JSON module doesn't even handle null.

Ok, option 3 it is.

achamayou commented 1 year ago

@lemmy I am a bit puzzled. Despite producing output seemingly equivalent to the existing trace job using static files, all my runs (local or on CI) end up with a return code of 151, for example:

amchamay@amchamay:~/CCF/tla$ JSON=../build/reconnect_node.ndjson java -XX:+UseParallelGC -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -tool Traceccfraft.tla 2>&1
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.18 of Day Month 20?? (rev: a5053a0)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 5 and seed -2153380224744086050 with 1 worker on 8 cores with 14293MB heap and 64MB offheap memory [pid: 59520] (Linux 5.15.0-1034-azure amd64, Ubuntu 11.0.18 x86_64, MSBDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/amchamay/CCF/tla/Traceccfraft.tla
Parsing file /home/amchamay/CCF/tla/ccfraft.tla
Parsing file /tmp/tlc-4098931758969786108/Json.tla (jar:file:/home/amchamay/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Json.tla)
Parsing file /tmp/tlc-4098931758969786108/IOUtils.tla (jar:file:/home/amchamay/CCF/tla/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /tmp/tlc-4098931758969786108/Sequences.tla (jar:file:/home/amchamay/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-4098931758969786108/Naturals.tla (jar:file:/home/amchamay/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-4098931758969786108/FiniteSets.tla (jar:file:/home/amchamay/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-4098931758969786108/TLC.tla (jar:file:/home/amchamay/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-4098931758969786108/FiniteSetsExt.tla (jar:file:/home/amchamay/CCF/tla/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /tmp/tlc-4098931758969786108/SequencesExt.tla (jar:file:/home/amchamay/CCF/tla/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /tmp/tlc-4098931758969786108/Functions.tla (jar:file:/home/amchamay/CCF/tla/CommunityModules-deps.jar!/Functions.tla)
Parsing file /tmp/tlc-4098931758969786108/Folds.tla (jar:file:/home/amchamay/CCF/tla/CommunityModules-deps.jar!/Folds.tla)
Parsing file /tmp/tlc-4098931758969786108/Integers.tla (jar:file:/home/amchamay/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module ccfraft
Semantic processing of module Json
Semantic processing of module Integers
Semantic processing of module IOUtils
Semantic processing of module Traceccfraft
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2023-04-25 22:59:30)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2281:1 @!@!@
The configuration file substitutes constant Servers with non-constant TraceServers
@!@!@ENDMSG 2281 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 458ms at (2023-04-25 22:59:30)
@!@!@ENDMSG 2186 @!@!@
amchamay@amchamay:~/CCF/tla$ echo $?
151

What am I missing?

achamayou commented 1 year ago

amchamay@amchamay:~/CCF/tla$ ls -al traces2/replicate.ndjson
-rw-rw-r-- 1 amchamay amchamay 27522 Apr 25 19:51 traces2/replicate.ndjson
amchamay@amchamay:~/CCF/tla$ ls -al ../build/replicate.ndjson
-rw-rw-r-- 1 amchamay amchamay 27522 Apr 25 23:07 ../build/replicate.ndjson
amchamay@amchamay:~/CCF/tla$ diff ../build/replicate.ndjson traces2/replicate.ndjson
amchamay@amchamay:~/CCF/tla$

and yet:

amchamay@amchamay:~/CCF/tla$ JSON=../build/replicate.ndjson java -XX:+UseParallelGC -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -tool Traceccfraft.tla 1>/dev/null; echo $?
151
amchamay@amchamay:~/CCF/tla$ JSON=traces2/replicate.ndjson java -XX:+UseParallelGC -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -tool Traceccfraft.tla 1>/dev/null; echo $?
0

achamayou commented 1 year ago

The error was caused by the lack of .nodes files, that must contain the maximum number of nodes used in the trace, and are expected with the same name in the same directory as the trace files:

JsonServers ==
    atoi(Deserialize(JsonFile \o ".nodes", [format |-> "TXT", charset |-> "UTF-8"]).stdout)
ASSUME JsonServers \in Nat \ {0}

I've not yet figured out, but there is probably a way to give a better error message when that happens.

achamayou commented 1 year ago

I think this is good to go now, we generate the traces every build, and run the validation against them. Next up #5208, #5212 and #5213.

lemmy commented 1 year ago

The error was caused by the lack of .nodes files, that must contain the maximum number of nodes used in the trace, and are expected with the same name in the same directory as the trace files:
JsonServers ==
    atoi(Deserialize(JsonFile \o ".nodes", [format |-> "TXT", charset |-> "UTF-8"]).stdout)
ASSUME JsonServers \in Nat \ {0}
I've not yet figured out, but there is probably a way to give a better error message when that happens.

I can look into the error handling of the involved operators. However, we might as well pass the number of nodes as an environment variable now, given that the .ndjson files are no longer part of the repo.

achamayou commented 1 year ago

I can look into the error handling of the involved operators. However, we might as well pass the number of nodes as an environment variable now, given that the .ndjson files are no longer part of the repo.

Ah that's a good idea. We'll need a small wrapper for the call to tlc (but maybe that's fine, it's fairly long) to extract the max number of nodes from the trace (this is done by the trace generation now, but can be moved).

achamayou commented 1 year ago

The SNP job failure is unrelated, and caused by a bug in our CI files, fixed separately in #5214

microsoft / CCF

Raft tracing #5201