Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add TLAi linter. #6098

Merged
merged 4 commits into from
Mar 27, 2024
Merged

Add TLAi linter. #6098

merged 4 commits into from
Mar 27, 2024

Conversation

lemmy
Copy link
Contributor

@lemmy lemmy commented Mar 26, 2024

I'm not 100% certain that this automation will have always access to the env secrets. Unfortunately, I don't know how to check it without deploying it.

@lemmy lemmy added the tla TLA+ specifications label Mar 26, 2024
@ghost
Copy link

ghost commented Mar 26, 2024

mku-tlai@83226 aka 20240326.30 vs main ewma over 20 builds from 82798 to 83199

Click to see table

main

build_id build_number pi_basic_mt_virtual_cft^ Commit latency factor pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem tpcc_sgx_cft^ tpcc_sgx_cft_mem tpcc_virtual_cft^ ls_sgx_cft^ ls_sgx_cft_mem pi_ls_sgx_cft^ pi_ls_sgx_cft_mem pi_basic_sgx_cft^ pi_basic_sgx_cft_mem ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ pi_basic_js_virtual_cft^ ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem ls_js_virtual_cft^ ls_full_js_virtual_cft^ ls_jwt_sgx_cft^ ls_jwt_sgx_cft_mem 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 ls_full_js_sgx_cft^ ls_full_js_sgx_cft_mem ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem hist_sgx_cft^ KV ser (/s)^ KV deser (/s)^ KV snap ser (/s)^ KV snap deser (/s)^ RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^ tlc_sim_traces tlc_sim_levelmean
82798 20240318.25 97670.4 0.816977 27980.6 2.30851e+07 5577.76 8.59996e+07 17215.3 13942.6 1.88908e+07 14002.4 1.05021e+07 15379.8 1.46964e+07 53023.5 55469 62158.1 4443.2 20725 22098 1370 1.25993e+07 17491.2 17205.9 6801.93 1.88908e+07 6928.8 6.30784e+06 11605.5 5799.78 1.67936e+07 5480.57 1.67936e+07 3982.34 1.67936e+07 42771 1.05009e+06 1.14116e+06 7963.99 1404.73 827431 1.18304e+06 8.15472e+06 3.07581e+07 32280 384
82808 20240318.28 70163.6 0.805582 27678.5 2.51822e+07 5626.63 8.59996e+07 17152.8 13970.8 1.88908e+07 14039 1.05021e+07 15521.4 1.46964e+07 53231.6 55482.5 61663.6 4405.7 20568.4 21548.5 1373.9 1.25993e+07 17531.8 17515.4 6868.02 1.88908e+07 6931.4 6.30784e+06 11563.2 5803.98 1.67936e+07 5442.74 1.67936e+07 3990.95 1.67936e+07 45393.1 1.04646e+06 1.16809e+06 7919.02 1398.65 832135 1.17718e+06 8.09813e+06 3.14226e+07 31220 382
82814 20240319.1 70706.4 0.835128 28079.1 2.30851e+07 5601.4 8.59996e+07 17277.2 13946.2 1.88908e+07 14017.3 1.05021e+07 15577.4 1.46964e+07 52833.5 57165.7 62292 4430.8 21262.1 21811.2 1359.8 1.25993e+07 17511.8 17293.3 6850.25 1.88908e+07 7140.2 6.30784e+06 11732.8 5754.81 1.67936e+07 5447.98 1.67936e+07 3989.09 1.67936e+07 48561.4 1.03413e+06 1.14025e+06 7801.37 1405.27 830705 1.17741e+06 8.14402e+06 3.1109e+07 32462 369
82835 20240319.8 69590.2 0.837813 28062.1 2.51822e+07 5510.28 8.59996e+07 17227.7 13804.3 1.88908e+07 13908.2 1.05021e+07 15320.3 1.46964e+07 53576 56250.9 62196 4431.4 20786.7 21712.2 1348.4 1.25993e+07 17538.6 17544 6848.14 1.88908e+07 6889.5 6.30784e+06 11613.7 5778.13 1.67936e+07 5474.58 1.67936e+07 3957.99 1.67936e+07 44852.3 1.03907e+06 1.16741e+06 8028.68 1384.91 801178 1.18205e+06 8.1315e+06 3.11322e+07 31218 366
82842 20240320.1 82750.6 0.795937 28088.6 2.30851e+07 5578.48 8.59996e+07 17161.1 13967.6 1.88908e+07 13984.1 1.05021e+07 15560.5 1.25993e+07 50737.4 55481.9 61410.4 4408.2 20721.6 20939.8 1370.3 1.05021e+07 17393.6 16990.9 6805.41 1.88908e+07 7042.4 6.30784e+06 11706.9 5775.41 1.67936e+07 5467.65 1.67936e+07 3879.66 1.67936e+07 47065.1 1.05186e+06 1.16104e+06 8151.56 1404.1 839027 1.17528e+06 8.15056e+06 3.06587e+07 30174 382
82864 20240320.9 84734.7 0.821651 27810.6 2.30851e+07 5512.38 8.59996e+07 17219.5 13879.7 1.88908e+07 14042 1.05021e+07 15479.2 1.46964e+07 53302.2 55326.6 62207 4407.7 17196.8 21736.3 1359.2 1.25993e+07 17512.2 17459.7 6849.78 1.67936e+07 7018.8 6.30784e+06 11693.7 5765.35 1.67936e+07 5480.38 1.67936e+07 3990.49 1.67936e+07 41778.3 1.04701e+06 1.13109e+06 7937.05 1404.32 833112 1.18197e+06 8.15387e+06 3.07457e+07 31738 377
82906 20240321.2 87877.2 0.801621 27754.2 2.30851e+07 5533.71 8.59996e+07 17172.3 13799.2 1.88908e+07 13962 1.05021e+07 15288.3 1.46964e+07 52970.8 40672.6 60757.5 4392.6 20462.7 20745.2 1355.5 1.25993e+07 17430.2 17175.9 6799.37 1.67936e+07 6906.2 6.30784e+06 11543 5790.33 1.67936e+07 5465.42 1.67936e+07 3983.52 1.67936e+07 42157.6 1.05977e+06 1.17412e+06 7531.67 1400.02 836529 1.18229e+06 8.15368e+06 3.25902e+07 29270 386
82925 20240321.7 79485.1 0.807056 27420.1 2.30851e+07 5646.99 8.59996e+07 17368.7 13895 1.88908e+07 14012.6 1.05021e+07 15451.8 1.46964e+07 53475.8 56637 62746 4439.9 21040.8 21736.3 1376.3 1.25993e+07 17694.8 17398 6896.06 1.88908e+07 7094.7 6.30784e+06 11628.1 5751.92 1.67936e+07 5715.65 1.67936e+07 3995.22 1.67936e+07 45300.9 1.05086e+06 1.14718e+06 8069.03 1407.16 831410 1.17717e+06 8.13044e+06 3.0809e+07 32455 379
82996 20240322.3 79428.1 0.803997 27423.4 2.30851e+07 5569.26 8.59996e+07 17355.5 13890.2 1.88908e+07 14049.6 1.05021e+07 15467.8 1.46964e+07 53050.4 56308.8 62950.9 4446 20891.9 21857.9 1372.1 1.25993e+07 17952 17419.6 6884.86 1.88908e+07 7030.1 6.30784e+06 11656.7 5801.3 1.67936e+07 5456.3 1.67936e+07 3990.73 1.67936e+07 43140.2 1.04493e+06 1.11832e+06 8234.47 1400.61 835988 1.17669e+06 8.1458e+06 3.07868e+07 31479 377
83004 20240322.5 89907 0.808055 27756.3 2.30851e+07 5565.83 8.59996e+07 17299.9 13932.7 1.88908e+07 13952 1.05021e+07 15426.3 1.46964e+07 52868.8 55992.6 62180.5 4432.5 20709.2 21069 1361.3 1.25993e+07 17629.6 17616.8 6830.62 1.88908e+07 6879.1 6.30784e+06 11600.9 5801.54 1.67936e+07 5464.86 1.67936e+07 3984.08 1.67936e+07 42890.9 1.0618e+06 1.05664e+06 8153.94 1399.29 835816 1.1854e+06 8.16642e+06 3.10656e+07 30745 366
83028 20240322.11 67943.8 0.786739 27692 2.30851e+07 5528.39 8.59996e+07 17295.9 13900.8 1.88908e+07 13977.4 1.05021e+07 15498.5 1.46964e+07 53368.8 56110.7 62452.1 4426.2 21072 21721.7 1363.7 1.25993e+07 17573.9 17149 6797.9 1.88908e+07 6885.5 6.30784e+06 11633.8 5756.57 1.67936e+07 5440.95 1.67936e+07 3952.9 1.67936e+07 45247.5 1.01989e+06 1.16131e+06 7870.69 1403.37 826657 1.18227e+06 8.17001e+06 3.10609e+07 29497 374
83075 20240325.9 92049.2 0.777781 27592.1 2.51822e+07 5598.84 8.59996e+07 17111.8 13848.8 1.88908e+07 13996.7 1.05021e+07 15392.6 1.46964e+07 50328.8 54004.7 59968.3 4279.8 17295.7 21003.1 1356.8 1.25993e+07 17407.6 17504.3 6850.45 1.88908e+07 6933.6 6.30784e+06 11543.9 5771.89 1.67936e+07 5426.77 1.67936e+07 3782.41 1.67936e+07 44061.4 1.01698e+06 1.14469e+06 7576.94 1399.04 834313 1.18306e+06 8.15381e+06 3.15952e+07 30222 374
83097 20240325.17 79563.9 0.811724 27737.4 2.30851e+07 5551.44 8.59996e+07 17148.4 13866 1.88908e+07 13969.6 1.05021e+07 15283.2 1.25993e+07 52877.7 56718.3 62257.9 4459.3 21024.6 20727.5 1359.4 1.05021e+07 17652.1 17131.4 6803.62 1.88908e+07 6892.7 6.30784e+06 11757.9 5791.32 1.67936e+07 5465.92 1.67936e+07 3972.37 1.67936e+07 40610.5 1.05831e+06 1.1084e+06 7883.06 1398.86 841684 1.17933e+06 8.12434e+06 3.08415e+07 29938 377
83108 20240325.20 76019.9 0.816276 27653.5 2.51822e+07 5004.39 8.59996e+07 17273.3 13796.4 1.88908e+07 13646.8 1.05021e+07 14919.6 1.46964e+07 53403.3 57407.9 62082.9 4470.1 21064.6 21071.3 1356.4 1.25993e+07 17750.5 17316.2 6715.53 1.88908e+07 6823.7 6.30784e+06 11737.3 5513.68 1.67936e+07 5485.08 1.67936e+07 3838.74 1.67936e+07 43047 1.01667e+06 1.17925e+06 7419.23 1385.31 839891 1.18654e+06 8.15416e+06 3.23544e+07 31523 385
83126 20240325.25 75704.7 0.822261 27807.5 2.51822e+07 5510.05 8.59996e+07 17339.6 13821.2 1.88908e+07 13906 1.05021e+07 15175.2 1.46964e+07 53128.6 56578 61178.5 4405.7 20673 21759.5 1369.4 1.25993e+07 17593.2 17552.9 6786.31 1.88908e+07 6998.3 6.30784e+06 11803.5 5793.2 1.67936e+07 5441.74 1.67936e+07 3990.44 1.67936e+07 44709.3 1.02617e+06 1.16986e+06 7822.5 1402.59 828441 1.17895e+06 8.14146e+06 3.06771e+07 31345 377
83135 20240326.3 68065.1 0.807021 27562.6 2.51822e+07 5604.57 8.59996e+07 17387.7 13953.9 1.88908e+07 14040.3 1.05021e+07 15484.7 1.46964e+07 53118.8 56485.7 62135.6 4475.7 20800.9 21086.8 1377.6 1.05021e+07 17740.8 17202.2 6818.62 1.88908e+07 7019.5 6.30784e+06 11743.1 5803.7 1.67936e+07 5474.38 1.67936e+07 3971.4 1.67936e+07 39803.3 1.06225e+06 1.11136e+06 8134.52 1398.76 836262 1.18343e+06 8.15504e+06 3.08267e+07 32521 381
83145 20240326.6 84123.6 0.818053 27819.1 2.30851e+07 5542.68 8.59996e+07 17364.7 13980 1.88908e+07 13946 1.05021e+07 15420.4 1.46964e+07 53100.8 57093.3 61505.5 4458 21220.5 21785.5 1370.9 1.25993e+07 17392.6 17245.8 6825.64 1.88908e+07 6977.6 6.30784e+06 11592.3 5766.33 1.67936e+07 5466.25 1.67936e+07 3983.93 1.67936e+07 43404.8 1.04362e+06 1.20106e+06 8158.85 1405.66 830580 1.18191e+06 8.14e+06 3.08257e+07 32948 386
83161 20240326.10 72771 0.800191 27469.5 2.51822e+07 5624.66 8.59996e+07 17118.5 13984.8 1.88908e+07 13965.2 1.05021e+07 15438.1 1.46964e+07 50053.7 55306.1 58491.6 4390.9 20680 21083.3 1359.3 1.25993e+07 17338 17595.4 6816.39 1.88908e+07 6890.9 6.30784e+06 10381.2 5811.54 1.67936e+07 5436.84 1.67936e+07 3986.87 1.67936e+07 44328.3 1.00685e+06 1.14666e+06 8073.19 1400.87 825189 1.17774e+06 8.14917e+06 3.08675e+07 32746 373
83176 20240326.15 77379.2 0.80644 26788.9 2.51822e+07 5623.61 8.59996e+07 17353.9 13983 1.88908e+07 13998.6 1.05021e+07 15342.1 1.46964e+07 52708.7 55809.8 60335.2 4409.6 20970.2 21573.1 1355 1.25993e+07 17500.2 17488.8 6791.92 1.88908e+07 6909.2 6.30784e+06 11668.6 5801.77 1.67936e+07 5441.88 1.67936e+07 3980.3 1.67936e+07 45258.5 1.02041e+06 1.1443e+06 7901.72 1402.31 830151 1.18376e+06 8.15306e+06 3.08717e+07 30798 377
83199 20240326.22 73578.8 0.803466 27809.5 2.51822e+07 5497.03 8.59996e+07 17377.9 13883.2 1.67936e+07 13882.3 1.05021e+07 15335.1 1.25993e+07 52933.2 54977.4 60660.2 4420.9 21158 22072.6 1340.5 1.25993e+07 17485.9 16999.3 6896.2 1.88908e+07 6787.3 6.30784e+06 11526.7 5762.56 1.67936e+07 5421.69 1.67936e+07 3980.18 1.67936e+07 45287.7 1.02249e+06 1.15835e+06 8023.63 1401.56 832515 1.17816e+06 8.17261e+06 3.0797e+07 31222 380

mku-tlai

build_id build_number Commit latency factor tpcc_sgx_cft^ tpcc_sgx_cft_mem ls_sgx_cft^ ls_sgx_cft_mem pi_ls_sgx_cft^ pi_ls_sgx_cft_mem pi_basic_sgx_cft^ pi_basic_sgx_cft_mem pi_basic_mt_virtual_cft^ pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem ls_jwt_sgx_cft^ ls_jwt_sgx_cft_mem pi_ls_jwt_sgx_cft^ pi_ls_jwt_sgx_cft_mem ls_js_sgx_cft^ ls_js_sgx_cft_mem ls_full_js_sgx_cft^ ls_full_js_sgx_cft_mem ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem hist_sgx_cft^ KV ser (/s)^ KV deser (/s)^ KV snap ser (/s)^ KV snap deser (/s)^ RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^ tpcc_virtual_cft^ ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ pi_basic_js_virtual_cft^ ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_js_virtual_cft^ pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^ tlc_sim_traces tlc_sim_levelmean
83212 20240326.26 0.832407 5578.58 8.59996e+07 13828.3 1.88908e+07 13933.8 1.05021e+07 15172.1 1.46964e+07 97775.4 1370.9 1.25993e+07 6831.36 1.88908e+07 6833.7 6.30784e+06 5797.11 1.67936e+07 5470.55 1.67936e+07 3970.69 1.67936e+07 47165.7 1.06485e+06 1.18497e+06 7877.29 1401.67 837158 1.18112e+06 8.15553e+06 3.09001e+07 17205 53359 55808.9 61465.6 4435.8 20986.8 21887.1 17254.8 27568.6 2.51822e+07 17339.1 10011.2 31672 371
83226 20240326.30 0.830085 5634.72 8.59996e+07 13916.6 1.88908e+07 14000.1 1.05021e+07 15545 1.25993e+07 81704.8 1370.9 1.25993e+07 6867.91 1.88908e+07 6998.3 6.30784e+06 5799.79 1.67936e+07 5445.37 1.67936e+07 4005.98 1.67936e+07 40363.6 1.02617e+06 1.13636e+06 7866.49 1403.34 825120 1.17933e+06 8.15543e+06 3.12424e+07 17257.7 53177.2 55976.3 61267.6 4471.7 21105.4 21796.9 17415.4 27740.8 2.51822e+07 17023.2 11625.6 31332 371

images

@achamayou
Copy link
Member

achamayou commented Mar 26, 2024

The script seems to run but the upload to SARIF fails: https://github.com/microsoft/CCF/actions/runs/8442480667/job/23123973469

    message: 'Resource not accessible by integration',
    documentation_url: 'https://docs.github.com/rest'

It sounds like github/codeql-action#2117, but the repo is definitely public, so perhaps not?

@github-advanced-security
Copy link

This pull request sets up GitHub code scanning for this repository. Once the scans have completed and the checks have passed, the analysis results for this pull request branch will appear on this overview. Once you merge this pull request, the 'Security' tab will show more code scanning analysis results (for example, for the default branch). Depending on your configuration and choice of analysis tool, future pull requests will be annotated with code scanning analysis results. For more information about GitHub code scanning, check out the documentation.

@@ -20,7 +20,8 @@
SerialiseCoverageConstraint ==
LET interval == 500000
IN IF TLCGet("distinct") % interval = 0
THEN Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
THEN /\ Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])

Check warning

Code scanning / genaiscript

TLAi-linter Warning

The Serialize function in line 23 is used with options that suggest the creation and appending of data to the CoverageFilename. This is consistent with the comment in line 19 that states the file should be created if it does not exist and that data should be appended.
@@ -20,7 +20,8 @@
SerialiseCoverageConstraint ==
LET interval == 500000
IN IF TLCGet("distinct") % interval = 0
THEN Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
THEN /\ Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
/\ PrintT("Writing stats to file: " \o CoverageFilename)

Check notice

Code scanning / genaiscript

TLAi-linter

The `PrintT` statement in line 24 is consistent with the action described in the comment in line 19, as it logs the action of writing stats to the coverage file.
@@ -20,7 +20,8 @@
SerialiseCoverageConstraint ==
LET interval == 500000
IN IF TLCGet("distinct") % interval = 0
THEN Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
THEN /\ Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])

Check failure

Code scanning / genaiscript

TLAi-linter Error

The Serialize operator's options in line 23 include "WRITE", "CREATE", "APPEND", which are not standard TLA+ operators or strings and may not be understood by the TLA+ toolset without custom definitions or extensions.
@lemmy lemmy marked this pull request as ready for review March 27, 2024 00:10
@lemmy lemmy requested a review from a team March 27, 2024 00:10
@lemmy lemmy merged commit 67dd047 into main Mar 27, 2024
25 of 35 checks passed
@lemmy lemmy deleted the mku-tlai branch March 27, 2024 00:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
tla TLA+ specifications
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants