From 55630a5a89b98ad185e6ec813e97e9e9a52fea13 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Wed, 1 Nov 2023 15:14:09 +0000 Subject: [PATCH 01/22] experimenting with a stats postcondition --- tla/consensus/MCccfraft.cfg | 2 ++ tla/consensus/MCccfraft.tla | 9 +++++++-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index 09c7508056c0..009635ba0b13 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -76,3 +76,5 @@ INVARIANTS MatchIndexLowerBoundNextIndexInv CommitCommittableIndices CommittableIndicesAreKnownSignaturesInv + +POSTCONDITION PrintStats diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index d55776707c7b..ea543a43fe0e 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -1,5 +1,5 @@ ---------- MODULE MCccfraft ---------- -EXTENDS ccfraft, TLC +EXTENDS ccfraft, TLC, Json CONSTANTS NodeOne, NodeTwo, NodeThree @@ -53,7 +53,7 @@ MCTimeout(i) == /\ CCF!Timeout(i) \* Limit on client requests -RequestLimit == 3 +RequestLimit == 1 \* Limit number of requests (new entries) that can be made MCClientRequest(i) == @@ -136,4 +136,9 @@ AllReconfigurationsCommitted == DebugAllReconfigurationsReachableInv == ~AllReconfigurationsCommitted +PrintStats == + /\ PrintT(TLCGet("stats")) + /\ PrintT(ToJson(TLCGet("stats"))) + /\ JsonSerialize("/workspaces/CCF/tla/stats.json",TLCGet("stats")) + =================================== \ No newline at end of file From 23f10a25c9aa0c7356e3703bb06283456aa4e0c3 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Wed, 1 Nov 2023 15:27:12 +0000 Subject: [PATCH 02/22] moving stats filename --- tla/consensus/MCccfraft.cfg | 1 + tla/consensus/MCccfraft.tla | 7 +++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index 009635ba0b13..ca68f9d6326e 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -6,6 +6,7 @@ CONSTANTS MaxTermLimit = 1 MaxCommitsNotified = 0 + StatsFilename = "MCccfraft_stats.json" Timeout <- MCTimeout Send <- MCSend diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index ea543a43fe0e..7f9a8cf48eec 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -17,6 +17,9 @@ ASSUME MaxTermLimit \in Nat CONSTANT MaxCommitsNotified ASSUME MaxCommitsNotified \in Nat +CONSTANT StatsFilename +ASSUME StatsFilename \in STRING + ToServers == UNION Range(Configurations) @@ -53,7 +56,7 @@ MCTimeout(i) == /\ CCF!Timeout(i) \* Limit on client requests -RequestLimit == 1 +RequestLimit == 3 \* Limit number of requests (new entries) that can be made MCClientRequest(i) == @@ -139,6 +142,6 @@ DebugAllReconfigurationsReachableInv == PrintStats == /\ PrintT(TLCGet("stats")) /\ PrintT(ToJson(TLCGet("stats"))) - /\ JsonSerialize("/workspaces/CCF/tla/stats.json",TLCGet("stats")) + /\ JsonSerialize(StatsFilename, TLCGet("stats")) =================================== \ No newline at end of file From 2bb940af989d14abcd3f190469549b634867d2bc Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Wed, 1 Nov 2023 16:00:19 +0000 Subject: [PATCH 03/22] jsonserialize expects a sequence --- tla/consensus/MCccfraft.tla | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index 7f9a8cf48eec..4a97d0eeed02 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -56,7 +56,7 @@ MCTimeout(i) == /\ CCF!Timeout(i) \* Limit on client requests -RequestLimit == 3 +RequestLimit == 1 \* Limit number of requests (new entries) that can be made MCClientRequest(i) == @@ -140,8 +140,6 @@ DebugAllReconfigurationsReachableInv == ~AllReconfigurationsCommitted PrintStats == - /\ PrintT(TLCGet("stats")) - /\ PrintT(ToJson(TLCGet("stats"))) - /\ JsonSerialize(StatsFilename, TLCGet("stats")) + ndJsonSerialize(StatsFilename, <>) =================================== \ No newline at end of file From 0507d0fe2d735761d6c3bec7c1d0e0dc6985f651 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Wed, 1 Nov 2023 17:19:19 +0000 Subject: [PATCH 04/22] undo requestlimit change --- tla/consensus/MCccfraft.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index 4a97d0eeed02..1e0fd3be292d 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -56,7 +56,7 @@ MCTimeout(i) == /\ CCF!Timeout(i) \* Limit on client requests -RequestLimit == 1 +RequestLimit == 3 \* Limit number of requests (new entries) that can be made MCClientRequest(i) == From 6f0225767cc446b7ed5559d246d5d72ef02776b0 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Wed, 1 Nov 2023 17:25:57 +0000 Subject: [PATCH 05/22] tidying up json file stats --- tla/.gitignore | 3 ++- tla/consensus/MCccfraft.cfg | 2 +- tla/consensus/MCccfraft.tla | 2 +- tla/consensus/MCccfraftAtomicReconfig.cfg | 1 + tla/consensus/MCccfraftWithReconfig.cfg | 1 + 5 files changed, 6 insertions(+), 3 deletions(-) diff --git a/tla/.gitignore b/tla/.gitignore index e2bf06556ae6..181d5587e4f9 100644 --- a/tla/.gitignore +++ b/tla/.gitignore @@ -11,4 +11,5 @@ tools/ .DS_Store *.dot *TTrace*.tla -*TTrace*.bin \ No newline at end of file +*TTrace*.bin +*_stats.json \ No newline at end of file diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index ca68f9d6326e..6f7df6388f56 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -78,4 +78,4 @@ INVARIANTS CommitCommittableIndices CommittableIndicesAreKnownSignaturesInv -POSTCONDITION PrintStats +POSTCONDITION StatsFile diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index 1e0fd3be292d..1f879d0b9899 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -139,7 +139,7 @@ AllReconfigurationsCommitted == DebugAllReconfigurationsReachableInv == ~AllReconfigurationsCommitted -PrintStats == +StatsFile == ndJsonSerialize(StatsFilename, <>) =================================== \ No newline at end of file diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg index 0805ce3b785f..5814878b265e 100644 --- a/tla/consensus/MCccfraftAtomicReconfig.cfg +++ b/tla/consensus/MCccfraftAtomicReconfig.cfg @@ -6,6 +6,7 @@ CONSTANTS MaxTermLimit = 4 MaxCommitsNotified = 2 + StatsFilename = "MCccfraftAtomicReconfig_stats.json" Timeout <- MCTimeout Send <- MCSend diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg index 7075daee6fbf..13682894208a 100644 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ b/tla/consensus/MCccfraftWithReconfig.cfg @@ -6,6 +6,7 @@ CONSTANTS MaxTermLimit = 3 MaxCommitsNotified = 2 + StatsFilename = "MCccfraftWithReconfig_stats.json" Timeout <- MCTimeout Send <- MCSend From eef132ef82a8c131cbd44ffcae1299d81532308c Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Wed, 1 Nov 2023 19:53:41 +0000 Subject: [PATCH 06/22] tidying up --- tla/consensus/MCccfraft.cfg | 8 +++++--- tla/consensus/MCccfraft.tla | 11 +++++++---- tla/consensus/MCccfraftAtomicReconfig.cfg | 6 +++++- tla/consensus/MCccfraftWithReconfig.cfg | 6 +++++- 4 files changed, 22 insertions(+), 9 deletions(-) diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index f8cb16fffbd4..5602cd0ed89d 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -6,8 +6,9 @@ CONSTANTS MaxTermLimit = 1 MaxCommitsNotified = 0 - StatsFilename = "MCccfraft_stats.json" RequestLimit = 3 + + StatsFilename = "MCccfraft_stats.json" Timeout <- MCTimeout Send <- MCSend @@ -51,6 +52,9 @@ VIEW View CHECK_DEADLOCK FALSE +POSTCONDITION + WriteStatsFile + PROPERTIES CommittedLogAppendOnlyProp MonotonicTermProp @@ -78,5 +82,3 @@ INVARIANTS MatchIndexLowerBoundNextIndexInv CommitCommittableIndices CommittableIndicesAreKnownSignaturesInv - -POSTCONDITION StatsFile diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index bd9fc1c70897..97f250a8fcf4 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -17,13 +17,14 @@ ASSUME MaxTermLimit \in Nat CONSTANT MaxCommitsNotified ASSUME MaxCommitsNotified \in Nat -CONSTANT StatsFilename -ASSUME StatsFilename \in STRING - \* Limit on client requests CONSTANT RequestLimit ASSUME RequestLimit \in Nat +\* Filename to write TLC stats to +CONSTANT StatsFilename +ASSUME StatsFilename \in STRING + ToServers == UNION Range(Configurations) @@ -141,7 +142,9 @@ AllReconfigurationsCommitted == DebugAllReconfigurationsReachableInv == ~AllReconfigurationsCommitted -StatsFile == +\* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format +\* Specify WriteStatsFile as a postcondition to write the stats file at the end of model checking +WriteStatsFile == ndJsonSerialize(StatsFilename, <>) =================================== \ No newline at end of file diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg index 73f1df795e52..914b0e160935 100644 --- a/tla/consensus/MCccfraftAtomicReconfig.cfg +++ b/tla/consensus/MCccfraftAtomicReconfig.cfg @@ -6,8 +6,9 @@ CONSTANTS MaxTermLimit = 4 MaxCommitsNotified = 2 - StatsFilename = "MCccfraftAtomicReconfig_stats.json" RequestLimit = 3 + + StatsFilename = "MCccfraftAtomicReconfig_stats.json" Timeout <- MCTimeout Send <- MCSend @@ -51,6 +52,9 @@ VIEW View CHECK_DEADLOCK FALSE +POSTCONDITION + WriteStatsFile + PROPERTIES CommittedLogAppendOnlyProp MonotonicTermProp diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg index 8df96ff1f760..db2f1b600bf0 100644 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ b/tla/consensus/MCccfraftWithReconfig.cfg @@ -6,8 +6,9 @@ CONSTANTS MaxTermLimit = 3 MaxCommitsNotified = 2 - StatsFilename = "MCccfraftWithReconfig_stats.json" RequestLimit = 3 + + StatsFilename = "MCccfraftWithReconfig_stats.json" Timeout <- MCTimeout Send <- MCSend @@ -51,6 +52,9 @@ VIEW View CHECK_DEADLOCK FALSE +POSTCONDITION + WriteStatsFile + PROPERTIES CommittedLogAppendOnlyProp MonotonicTermProp From b514e5a77f4888088438ebcd0d0c03e7a952d71b Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Thu, 2 Nov 2023 13:01:37 +0000 Subject: [PATCH 07/22] print statement for stats file --- tla/consensus/MCccfraft.tla | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index 97f250a8fcf4..803c54eb98af 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -145,6 +145,7 @@ DebugAllReconfigurationsReachableInv == \* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format \* Specify WriteStatsFile as a postcondition to write the stats file at the end of model checking WriteStatsFile == - ndJsonSerialize(StatsFilename, <>) + /\ PrintT("Writing stats to file: " \o StatsFilename) + /\ ndJsonSerialize(StatsFilename, <>) =================================== \ No newline at end of file From 2f39151cbdfddde2c358be794fa01caa96112ac5 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Thu, 2 Nov 2023 13:52:52 +0000 Subject: [PATCH 08/22] starting script to upload --- tests/upload_tlc_stats.py | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tests/upload_tlc_stats.py diff --git a/tests/upload_tlc_stats.py b/tests/upload_tlc_stats.py new file mode 100644 index 000000000000..1b4173956748 --- /dev/null +++ b/tests/upload_tlc_stats.py @@ -0,0 +1,37 @@ +# Copyright (c) Microsoft Corporation. All rights reserved. +# Licensed under the Apache 2.0 License. + +import json +import os +import argparse + +from loguru import logger as LOG + + +def run(filename): + if os.path.exists(filename): + with open(filename) as f: + data = json.load(f) + duration_sec = data["duration"] + dstates = data["distinct"] + LOG.info( + "Uploading metrics - duration: {}, distinct states: {}", + duration_sec, + dstates, + ) + # TODO: upload metrics here + + else: + LOG.warning(f"Could not find file {filename}: skipping metrics upload") + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description="Upload TLC stats to cimetrics.") + + parser.add_argument( + "filename", + help="TLC stats JSON file to upload", + ) + + args = parser.parse_args() + run(args.filename) From f13758d9106e1599a5dc5ce286192b6a99988a10 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Thu, 2 Nov 2023 14:27:58 +0000 Subject: [PATCH 09/22] starting action for upload --- .github/workflows/tlaplus.yml | 6 ++++++ tests/upload_tlc_stats.py | 5 ++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index aa81023a858e..34bca823431e 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -38,6 +38,12 @@ jobs: cd tla/ ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json + - name: Uploading TLC stats to cimetrics + run: | + cd tests + pip3 install -r requirements.txt + python3 upload_tlc_stats.py ../tla/MCccfraftWithReconfig.json + - name: Upload traces in TLA and JSON format uses: actions/upload-artifact@v3 if: ${{ failure() }} diff --git a/tests/upload_tlc_stats.py b/tests/upload_tlc_stats.py index 1b4173956748..332a5b171946 100644 --- a/tests/upload_tlc_stats.py +++ b/tests/upload_tlc_stats.py @@ -4,6 +4,7 @@ import json import os import argparse +import cimetrics.upload from loguru import logger as LOG @@ -19,7 +20,9 @@ def run(filename): duration_sec, dstates, ) - # TODO: upload metrics here + with cimetrics.upload.metrics(complete=False) as metrics: + metrics.put("TLC Duration (s)", duration_sec) + metrics.put("TLC Distinct States", dstates) else: LOG.warning(f"Could not find file {filename}: skipping metrics upload") From e4ecc7f56ef445946d9c76debb1eb2f26d2002ce Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Thu, 2 Nov 2023 19:36:36 +0000 Subject: [PATCH 10/22] adding test label --- tests/upload_tlc_stats.py | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/tests/upload_tlc_stats.py b/tests/upload_tlc_stats.py index 332a5b171946..f85ac7dc51e2 100644 --- a/tests/upload_tlc_stats.py +++ b/tests/upload_tlc_stats.py @@ -9,20 +9,21 @@ from loguru import logger as LOG -def run(filename): +def run(test_label, filename): if os.path.exists(filename): with open(filename) as f: data = json.load(f) duration_sec = data["duration"] dstates = data["distinct"] LOG.info( - "Uploading metrics - duration: {}, distinct states: {}", + "Uploading metrics for {} - duration: {}, distinct states: {}", + test_label, duration_sec, dstates, ) with cimetrics.upload.metrics(complete=False) as metrics: - metrics.put("TLC Duration (s)", duration_sec) - metrics.put("TLC Distinct States", dstates) + metrics.put(f"tlc_{test_label}_duration_s", duration_sec) + metrics.put(f"tlc_{test_label}_states", dstates) else: LOG.warning(f"Could not find file {filename}: skipping metrics upload") @@ -31,10 +32,15 @@ def run(filename): if __name__ == "__main__": parser = argparse.ArgumentParser(description="Upload TLC stats to cimetrics.") + parser.add_argument( + "test_label", + help="test name to upload metrics under", + ) + parser.add_argument( "filename", help="TLC stats JSON file to upload", ) args = parser.parse_args() - run(args.filename) + run(args.test_label, args.filename) From c04ed2f400072058f9c55832e90f64c29e9fe4f5 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Thu, 2 Nov 2023 20:19:56 +0000 Subject: [PATCH 11/22] using stats file with consistency spec as well --- tla/StatsFile.tla | 14 ++++++++++++++ tla/consensus/MCccfraft.tla | 12 ++---------- tla/consistency/MCMultiNodeReads.cfg | 7 ++++++- tla/consistency/MCMultiNodeReads.tla | 2 +- 4 files changed, 23 insertions(+), 12 deletions(-) create mode 100644 tla/StatsFile.tla diff --git a/tla/StatsFile.tla b/tla/StatsFile.tla new file mode 100644 index 000000000000..8fd576267984 --- /dev/null +++ b/tla/StatsFile.tla @@ -0,0 +1,14 @@ +---- MODULE StatsFile---- +EXTENDS TLC, Json, Sequences + +\* Filename to write TLC stats to +CONSTANT StatsFilename +ASSUME StatsFilename \in STRING + +\* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format +\* Specify WriteStatsFile as a postcondition to write the stats file at the end of model checking +WriteStatsFile == + /\ PrintT("Writing stats to file: " \o StatsFilename) + /\ ndJsonSerialize(StatsFilename, <>) + +==== \ No newline at end of file diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla index 803c54eb98af..a1890a759340 100644 --- a/tla/consensus/MCccfraft.tla +++ b/tla/consensus/MCccfraft.tla @@ -1,5 +1,5 @@ ---------- MODULE MCccfraft ---------- -EXTENDS ccfraft, TLC, Json +EXTENDS ccfraft, StatsFile CONSTANTS NodeOne, NodeTwo, NodeThree @@ -21,10 +21,6 @@ ASSUME MaxCommitsNotified \in Nat CONSTANT RequestLimit ASSUME RequestLimit \in Nat -\* Filename to write TLC stats to -CONSTANT StatsFilename -ASSUME StatsFilename \in STRING - ToServers == UNION Range(Configurations) @@ -142,10 +138,6 @@ AllReconfigurationsCommitted == DebugAllReconfigurationsReachableInv == ~AllReconfigurationsCommitted -\* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format -\* Specify WriteStatsFile as a postcondition to write the stats file at the end of model checking -WriteStatsFile == - /\ PrintT("Writing stats to file: " \o StatsFilename) - /\ ndJsonSerialize(StatsFilename, <>) + =================================== \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReads.cfg b/tla/consistency/MCMultiNodeReads.cfg index d7550de52e54..4cf35c970535 100644 --- a/tla/consistency/MCMultiNodeReads.cfg +++ b/tla/consistency/MCMultiNodeReads.cfg @@ -4,6 +4,8 @@ CONSTANTS HistoryLimit = 6 ViewLimit = 3 + StatsFilename = "MCMultiNodeReads_stats.json" + RwTxRequest = RwTxRequest RwTxResponse = RwTxResponse RoTxRequest = RoTxRequest @@ -28,4 +30,7 @@ INVARIANTS AtMostOnceObservedInv CHECK_DEADLOCK - FALSE \ No newline at end of file + FALSE + +POSTCONDITION + WriteStatsFile \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReads.tla b/tla/consistency/MCMultiNodeReads.tla index 68f414d8fb0e..e371602f4612 100644 --- a/tla/consistency/MCMultiNodeReads.tla +++ b/tla/consistency/MCMultiNodeReads.tla @@ -1,7 +1,7 @@ ---- MODULE MCMultiNodeReads ---- \* Bounded version of MultiNodeReads -EXTENDS MCSingleNodeReads, MCMultiNode +EXTENDS MCSingleNodeReads, MCMultiNode, StatsFile MCNextMultiNodeReadsAction == \/ MCNextMultiNodeAction From ce7f5f20d56f4d339834205b9744e5651f2e7ed4 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 11:32:47 +0000 Subject: [PATCH 12/22] rollback consistency changes --- tla/consistency/MCMultiNodeReads.cfg | 7 +------ tla/consistency/MCMultiNodeReads.tla | 2 +- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/tla/consistency/MCMultiNodeReads.cfg b/tla/consistency/MCMultiNodeReads.cfg index 4cf35c970535..d7550de52e54 100644 --- a/tla/consistency/MCMultiNodeReads.cfg +++ b/tla/consistency/MCMultiNodeReads.cfg @@ -4,8 +4,6 @@ CONSTANTS HistoryLimit = 6 ViewLimit = 3 - StatsFilename = "MCMultiNodeReads_stats.json" - RwTxRequest = RwTxRequest RwTxResponse = RwTxResponse RoTxRequest = RoTxRequest @@ -30,7 +28,4 @@ INVARIANTS AtMostOnceObservedInv CHECK_DEADLOCK - FALSE - -POSTCONDITION - WriteStatsFile \ No newline at end of file + FALSE \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReads.tla b/tla/consistency/MCMultiNodeReads.tla index e371602f4612..f63a30fd3360 100644 --- a/tla/consistency/MCMultiNodeReads.tla +++ b/tla/consistency/MCMultiNodeReads.tla @@ -1,7 +1,7 @@ ---- MODULE MCMultiNodeReads ---- \* Bounded version of MultiNodeReads -EXTENDS MCSingleNodeReads, MCMultiNode, StatsFile +EXTENDS MCSingleNodeReads, MCMultiNodegit s MCNextMultiNodeReadsAction == \/ MCNextMultiNodeAction From 775d5d73b8a9c0fe8004f67e29362ecfd46609e9 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 11:33:29 +0000 Subject: [PATCH 13/22] rollback consistency changes --- tla/consistency/MCMultiNodeReads.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tla/consistency/MCMultiNodeReads.tla b/tla/consistency/MCMultiNodeReads.tla index f63a30fd3360..68f414d8fb0e 100644 --- a/tla/consistency/MCMultiNodeReads.tla +++ b/tla/consistency/MCMultiNodeReads.tla @@ -1,7 +1,7 @@ ---- MODULE MCMultiNodeReads ---- \* Bounded version of MultiNodeReads -EXTENDS MCSingleNodeReads, MCMultiNodegit s +EXTENDS MCSingleNodeReads, MCMultiNode MCNextMultiNodeReadsAction == \/ MCNextMultiNodeAction From a106bc016e3c1e77d8ef0095e37091e86e77a390 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 11:38:08 +0000 Subject: [PATCH 14/22] rollback edits to .gitignore before merge with ado migration --- .github/workflows/tlaplus.yml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index 34bca823431e..aa81023a858e 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -38,12 +38,6 @@ jobs: cd tla/ ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json - - name: Uploading TLC stats to cimetrics - run: | - cd tests - pip3 install -r requirements.txt - python3 upload_tlc_stats.py ../tla/MCccfraftWithReconfig.json - - name: Upload traces in TLA and JSON format uses: actions/upload-artifact@v3 if: ${{ failure() }} From b14d78ec441baa05c2f432adb83e1069038be92b Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 13:27:37 +0000 Subject: [PATCH 15/22] trying cimetrics with ado --- .azure-pipelines-templates/model_checking.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml index b8e70d712be1..8be3a29eb644 100644 --- a/.azure-pipelines-templates/model_checking.yml +++ b/.azure-pipelines-templates/model_checking.yml @@ -31,6 +31,12 @@ jobs: workingDirectory: tla displayName: MCccfraftWithReconfig.cfg + - script: | + pip3 install -r requirements.txt + python3 upload_tlc_stats.py ../tla/MCccfraft.json + workingDirectory: tests + displayName: Uploading TLC stats to cimetrics + - task: PublishPipelineArtifact@1 inputs: artifactName: "Model Checking Traces" From 3365e23182deed5e22b8e5dc81c840e3e076db6d Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 13:35:15 +0000 Subject: [PATCH 16/22] adding test label --- .azure-pipelines-templates/model_checking.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml index 8be3a29eb644..ba48573b16c7 100644 --- a/.azure-pipelines-templates/model_checking.yml +++ b/.azure-pipelines-templates/model_checking.yml @@ -33,7 +33,7 @@ jobs: - script: | pip3 install -r requirements.txt - python3 upload_tlc_stats.py ../tla/MCccfraft.json + python3 upload_tlc_stats.py 3node_fixed ../tla/MCccfraft.json workingDirectory: tests displayName: Uploading TLC stats to cimetrics From e1e3cc4acd46d510acc432c2efd4507b89bde4ff Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 13:46:19 +0000 Subject: [PATCH 17/22] adding new category for to cimetrics for tlc --- metrics.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/metrics.yml b/metrics.yml index d7834b71c03d..fe243e962460 100644 --- a/metrics.yml +++ b/metrics.yml @@ -10,4 +10,5 @@ monitoring_span: 150 groups: "SGX": ".*_sgx_.*" "Virtual": ".*_virtual_.*" + "TLC": "tlc_.*" "Others": ".*" From 8f30c52bcfce9c344d2cc646837e1cdf34ae892e Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 13:52:14 +0000 Subject: [PATCH 18/22] giving the new cimetric across to the mongo connection --- .azure-pipelines-templates/model_checking.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml index ba48573b16c7..727b8669ed72 100644 --- a/.azure-pipelines-templates/model_checking.yml +++ b/.azure-pipelines-templates/model_checking.yml @@ -34,6 +34,8 @@ jobs: - script: | pip3 install -r requirements.txt python3 upload_tlc_stats.py 3node_fixed ../tla/MCccfraft.json + env: + METRICS_MONGO_CONNECTION: $(METRICS_MONGO_CONNECTION) workingDirectory: tests displayName: Uploading TLC stats to cimetrics From e1d8297c2f4e9f1c5e7e73c363f31fb08e2d3389 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 14:50:22 +0000 Subject: [PATCH 19/22] test run --- .azure-pipelines-templates/model_checking.yml | 14 +++++++------- tla/consensus/MCccfraftWithReconfig.cfg | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml index 727b8669ed72..ebb06bc8768c 100644 --- a/.azure-pipelines-templates/model_checking.yml +++ b/.azure-pipelines-templates/model_checking.yml @@ -23,16 +23,16 @@ jobs: workingDirectory: tla displayName: MCccfraft.cfg - - script: ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json - workingDirectory: tla - displayName: MCccfraftAtomicReconfig.cfg + # - script: ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json + # workingDirectory: tla + # displayName: MCccfraftAtomicReconfig.cfg - - script: ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json - workingDirectory: tla - displayName: MCccfraftWithReconfig.cfg + # - script: ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json + # workingDirectory: tla + # displayName: MCccfraftWithReconfig.cfg - script: | - pip3 install -r requirements.txt + pip install -r requirements.txt python3 upload_tlc_stats.py 3node_fixed ../tla/MCccfraft.json env: METRICS_MONGO_CONNECTION: $(METRICS_MONGO_CONNECTION) diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg index db2f1b600bf0..f6890893c8b0 100644 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ b/tla/consensus/MCccfraftWithReconfig.cfg @@ -6,7 +6,7 @@ CONSTANTS MaxTermLimit = 3 MaxCommitsNotified = 2 - RequestLimit = 3 + RequestLimit = 2 StatsFilename = "MCccfraftWithReconfig_stats.json" From 195f9afa338b010f19b39507595d7f4f8ac20b7c Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Tue, 7 Nov 2023 17:45:55 +0000 Subject: [PATCH 20/22] Update .azure-pipelines-templates/model_checking.yml --- .azure-pipelines-templates/model_checking.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml index ebb06bc8768c..eabafaeee2e9 100644 --- a/.azure-pipelines-templates/model_checking.yml +++ b/.azure-pipelines-templates/model_checking.yml @@ -32,7 +32,10 @@ jobs: # displayName: MCccfraftWithReconfig.cfg - script: | - pip install -r requirements.txt + set -ex + python3.8 -m venv env + source env/bin/activate + python -m pip install -r requirements.txt python3 upload_tlc_stats.py 3node_fixed ../tla/MCccfraft.json env: METRICS_MONGO_CONNECTION: $(METRICS_MONGO_CONNECTION) From e194afb227af85b598e22b2268d9fb4b786f30f5 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Tue, 7 Nov 2023 20:59:55 +0000 Subject: [PATCH 21/22] Update .azure-pipelines-templates/model_checking.yml --- .azure-pipelines-templates/model_checking.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml index eabafaeee2e9..711bfa0bece1 100644 --- a/.azure-pipelines-templates/model_checking.yml +++ b/.azure-pipelines-templates/model_checking.yml @@ -36,7 +36,8 @@ jobs: python3.8 -m venv env source env/bin/activate python -m pip install -r requirements.txt - python3 upload_tlc_stats.py 3node_fixed ../tla/MCccfraft.json + ls ../tla/*.json + python3 upload_tlc_stats.py 3node_fixed ../tla/MCccfraft_stats.json env: METRICS_MONGO_CONNECTION: $(METRICS_MONGO_CONNECTION) workingDirectory: tests From 715d1870843712595bd8f1beed5f7ee87605c48a Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 7 Nov 2023 21:31:34 +0000 Subject: [PATCH 22/22] restoring the other mc jobs --- .azure-pipelines-templates/model_checking.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml index 711bfa0bece1..c9d130610447 100644 --- a/.azure-pipelines-templates/model_checking.yml +++ b/.azure-pipelines-templates/model_checking.yml @@ -23,13 +23,13 @@ jobs: workingDirectory: tla displayName: MCccfraft.cfg - # - script: ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json - # workingDirectory: tla - # displayName: MCccfraftAtomicReconfig.cfg + - script: ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json + workingDirectory: tla + displayName: MCccfraftAtomicReconfig.cfg - # - script: ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json - # workingDirectory: tla - # displayName: MCccfraftWithReconfig.cfg + - script: ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json + workingDirectory: tla + displayName: MCccfraftWithReconfig.cfg - script: | set -ex