diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index c5faa059dc14..ebbe90fe0656 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -10,8 +10,8 @@ on: workflow_dispatch: jobs: - model-checking: - name: Model Checking + model-checking-consensus: + name: Model Checking - Consensus runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] container: image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15 @@ -42,8 +42,8 @@ jobs: tla/*.trace.tla tla/*.json - simulation: - name: Simulation + simulation-consensus: + name: Simulation - Consensus runs-on: ubuntu-latest steps: @@ -63,3 +63,100 @@ jobs: path: | tla/*.trace.tla tla/*.json + + model-checking-consistency: + name: Model Checking - Consistency + runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] + container: + image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15 + + steps: + - uses: actions/checkout@v3 + - run: | + sudo apt update + sudo apt install -y default-jre + python3 ./tla/install_deps.py + + - name: consistency/MCSingleNode.cfg + run: | + cd tla/ + ./tlc.sh -workers auto consistency/MCSingleNode.tla -dumpTrace json MCSingleNode.json + + - name: consistency/MCSingleNodeReads.cfg + run: | + cd tla/ + ./tlc.sh -workers auto consistency/MCSingleNodeReads.tla -dumpTrace json MCSingleNodeReads.json + + - name: consistency/MCMultiNode.cfg + run: | + cd tla/ + ./tlc.sh -workers auto consistency/MCMultiNode.tla -dumpTrace json MCMultiNode.json + + - name: consistency/MCMultiNodeReads.cfg + run: | + cd tla/ + ./tlc.sh -workers auto consistency/MCMultiNodeReads.tla -dumpTrace json MCMultiNodeReads.json + + - name: consistency/MCMultiNodeReadsAlt.cfg + run: | + cd tla/ + ./tlc.sh -workers auto consistency/MCMultiNodeReadsAlt.tla -dumpTrace json MCMultiNodeReadsAlt.json + + - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox. + uses: actions/upload-artifact@v3 + if: ${{ failure() }} + with: + name: tlc + path: | + tla/consistency/*_TTrace_*.tla + tla/*.json + + counterexamples-consistency: + name: Counterexamples - Consistency + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v3 + - run: python3 ./tla/install_deps.py + + - name: consistency/MCSingleNodeCommitReachability.cfg + run: | + cd tla/ + ./tlc_debug.sh -workers auto -config consistency/MCSingleNodeCommitReachability.cfg consistency/MCSingleNodeReads.tla + + - name: consistency/MCMultiNodeCommitReachability.cfg + run: | + cd tla/ + ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeCommitReachability.cfg consistency/MCMultiNodeReads.tla + + - name: consistency/MCMultiNodeInvalidReachability.cfg + run: | + cd tla/ + ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeInvalidReachability.cfg consistency/MCMultiNodeReads.tla + + - name: consistency/MCMultiNodeReadsNotLinearizable.cfg + run: | + cd tla/ + ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeReadsNotLinearizable.cfg consistency/MCMultiNodeReads.tla + + simulation-consistency: + name: Simulation - Consistency + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v3 + - run: python3 ./tla/install_deps.py + + - name: consistency/MultiNodeReads.cfg + run: | + cd tla/ + ./tlc.sh -workers auto -simulate num=5 -depth 50 consistency/MultiNodeReads.tla -dumpTrace json MultiNodeReads.json + + - name: Upload traces in TLA and JSON format + uses: actions/upload-artifact@v3 + if: ${{ failure() }} + with: + name: tlc + path: | + tla/consistency/*_TTrace_*.tla + tla/*.json diff --git a/tests/infra/consortium.py b/tests/infra/consortium.py index 54574ca84f1c..65eaca91ca3d 100644 --- a/tests/infra/consortium.py +++ b/tests/infra/consortium.py @@ -522,9 +522,7 @@ def assert_service_identity(self, remote_node, service_cert_path): proposal = self.get_any_active_member().propose(remote_node, proposal_body) return self.vote_using_majority(remote_node, proposal, careful_vote) - def set_js_app_from_dir( - self, remote_node, bundle_path, disable_bytecode_cache=False - ): + def read_bundle_from_dir(self, bundle_path): if os.path.isfile(bundle_path): tmp_dir = tempfile.TemporaryDirectory(prefix="ccf") shutil.unpack_archive(bundle_path, tmp_dir.name) @@ -547,21 +545,20 @@ def set_js_app_from_dir( f"{method} {url}: module '{module_path}' not found in bundle" ) - proposal_body, careful_vote = self.make_proposal( - "set_js_app", - bundle={"metadata": metadata, "modules": modules}, - disable_bytecode_cache=disable_bytecode_cache, - ) - proposal = self.get_any_active_member().propose(remote_node, proposal_body) - # Large apps take a long time to process - wait longer than normal for commit - return self.vote_using_majority(remote_node, proposal, careful_vote, timeout=30) + return {"metadata": metadata, "modules": modules} - def set_js_app_from_json( - self, remote_node, json_path, disable_bytecode_cache=False + def set_js_app_from_dir( + self, remote_node, bundle_path, disable_bytecode_cache=False ): + bundle = self.read_bundle_from_dir(bundle_path) + return self.set_js_app_from_bundle( + remote_node, bundle, disable_bytecode_cache=disable_bytecode_cache + ) + + def set_js_app_from_bundle(self, remote_node, bundle, disable_bytecode_cache=False): proposal_body, careful_vote = self.make_proposal( "set_js_app", - bundle=slurp_json(json_path), + bundle=bundle, disable_bytecode_cache=disable_bytecode_cache, ) diff --git a/tests/js-custom-authorization/custom_authorization.py b/tests/js-custom-authorization/custom_authorization.py index 4319c14c7958..242276b5adf4 100644 --- a/tests/js-custom-authorization/custom_authorization.py +++ b/tests/js-custom-authorization/custom_authorization.py @@ -16,6 +16,7 @@ import infra.jwt_issuer import datetime import re +import uuid from http import HTTPStatus import subprocess from contextlib import contextmanager @@ -960,6 +961,12 @@ def was_cached(response): expect_much_smaller(repeat2, baseline) expect_much_smaller(repeat3, baseline) + return network + + +def test_caching_of_kv_handles(network, args): + primary, _ = network.find_nodes() + with primary.client() as c: LOG.info("Testing caching of KV handles") r = c.post("/app/increment") assert r.status_code == http.HTTPStatus.OK, r @@ -975,6 +982,33 @@ def was_cached(response): return network +def test_caching_of_app_code(network, args): + primary, backups = network.find_nodes() + LOG.info( + "Testing that interpreter reuse does not persist functions past app update" + ) + + def set_app_with_placeholder(new_val): + LOG.info(f"Replacing placeholder with {new_val}") + bundle = network.consortium.read_bundle_from_dir(args.js_app_bundle) + # Replace placeholder blindly, in the raw bundle JSON as string + s = json.dumps(bundle).replace("", new_val) + bundle = json.loads(s) + return network.consortium.set_js_app_from_bundle(primary, bundle) + + for _ in range(5): + v = str(uuid.uuid4()) + p = set_app_with_placeholder(v) + for node in [primary, *backups]: + with node.client() as c: + infra.commit.wait_for_commit(client=c, view=p.view, seqno=p.seqno) + r = c.get("/app/func_caching") + assert r.status_code == http.HTTPStatus.OK, r + assert r.body.text() == v + + return network + + def run_interpreter_reuse(args): # The js_app_bundle arg includes TS and Node dependencies, so must be built here # before deploying (and then we deploy the produces /dist folder) @@ -989,7 +1023,9 @@ def run_interpreter_reuse(args): ) as network: network.start_and_open(args) - network = test_reused_interpreter_behaviour(network, args) + network = test_reused_interpreter_behaviour(network, args) # + network = test_caching_of_kv_handles(network, args) + network = test_caching_of_app_code(network, args) if __name__ == "__main__": @@ -1035,7 +1071,7 @@ def run_interpreter_reuse(args): cr.add( "interpreter_reuse", run_interpreter_reuse, - nodes=infra.e2e_args.nodes(cr.args, 1), + nodes=infra.e2e_args.min_nodes(cr.args, f=1), js_app_bundle=os.path.join(cr.args.js_app_bundle, "js-interpreter-reuse"), ) diff --git a/tests/js-interpreter-reuse/app.json b/tests/js-interpreter-reuse/app.json index 876965b0e0b4..1980f42505b9 100644 --- a/tests/js-interpreter-reuse/app.json +++ b/tests/js-interpreter-reuse/app.json @@ -74,6 +74,19 @@ "key": "increment" } } + }, + "/func_caching": { + "get": { + "js_module": "func_caching.js", + "js_function": "func_caching", + "forwarding_required": "never", + "authn_policies": ["no_auth"], + "mode": "readonly", + "openapi": {}, + "interpreter_reuse": { + "key": "func_caching" + } + } } } } diff --git a/tests/js-interpreter-reuse/src/func_caching.js b/tests/js-interpreter-reuse/src/func_caching.js new file mode 100644 index 000000000000..d651c72dc75d --- /dev/null +++ b/tests/js-interpreter-reuse/src/func_caching.js @@ -0,0 +1,6 @@ +export function func_caching(request) { + const s = ""; + console.log(`Executing with s: ${s}`); + + return { body: s }; +} diff --git a/tests/js-interpreter-reuse/src/rollup_entry.ts b/tests/js-interpreter-reuse/src/rollup_entry.ts index 6fd965ce851f..51a953f5a733 100644 --- a/tests/js-interpreter-reuse/src/rollup_entry.ts +++ b/tests/js-interpreter-reuse/src/rollup_entry.ts @@ -1,3 +1,4 @@ export * from "./cache.js"; +export * from "./func_caching.js"; export * from "./di_sample"; export * from "./global_handle"; diff --git a/tests/js-modules/modules.py b/tests/js-modules/modules.py index 7ab53dbaa39d..c9114ba369b2 100644 --- a/tests/js-modules/modules.py +++ b/tests/js-modules/modules.py @@ -483,7 +483,8 @@ def test_npm_app(network, args): bundle_path = os.path.join( app_dir, "dist", "bundle.json" ) # Produced by build step of test npm-app - network.consortium.set_js_app_from_json(primary, bundle_path) + bundle = infra.consortium.slurp_json(bundle_path) + network.consortium.set_js_app_from_bundle(primary, bundle) LOG.info("Calling npm app endpoints") with primary.client("user0") as c: @@ -1211,7 +1212,8 @@ def test_js_execution_time(network, args): bundle_path = os.path.join( app_dir, "dist", "bundle.json" ) # Produced by build step of test npm-app in the previous test_npm_app - network.consortium.set_js_app_from_json(primary, bundle_path) + bundle = infra.consortium.slurp_json(bundle_path) + network.consortium.set_js_app_from_bundle(primary, bundle) LOG.info("Store JWT signing keys") jwt_key_priv_pem, _ = infra.crypto.generate_rsa_keypair(2048) diff --git a/tla/consistency/ExternalHistory.tla b/tla/consistency/ExternalHistory.tla new file mode 100644 index 000000000000..c977514b56c6 --- /dev/null +++ b/tla/consistency/ExternalHistory.tla @@ -0,0 +1,125 @@ +---- MODULE ExternalHistory ---- +\* Defines the notion of a externally observable client history and its associated properties. +\* The history differs for traditional client histories, as clients receive responses to +\* transactions before they have been committed. + +EXTENDS Naturals, Sequences, SequencesExt, FiniteSets, FiniteSetsExt + +\* Event types recorded in the history +\* Note that transaction status requests are not modelled to reduce state space +\* Currently only read-write (Rw) transactions and read-only (Ro) transactions are modelled +\* Both transaction types are modelled as forward-always transactions +\* This could be extended to support more types of read-only transactions +CONSTANTS RwTxRequest, RwTxResponse, RoTxRequest, RoTxResponse, TxStatusReceived + + +\* Transaction statuses +\* This model does not include the unknown and pending status to reduce state space +CONSTANTS CommittedStatus, InvalidStatus +TxStatuses == { + CommittedStatus, + InvalidStatus + } + +\* Views start at 1, 0 is used a null value +Views == Nat + +\* Sequence numbers start at 1, 0 is used a null value +SeqNums == Nat + +\* TxIDs consist of a view and sequence number and thus start at (1,1) +TxIDs == Views \X SeqNums + +\* This models uses a dummy application where read-write transactions +\* append an integer to a list and then reads the list +\* Read-only transactions simply read the list +Txs == Nat + +\* History of events visible to clients +VARIABLES history + +HistoryTypeOK == + \A i \in DOMAIN history: + \/ /\ history[i].type \in {RwTxRequest, RoTxRequest} + /\ history[i].tx \in Txs + \/ /\ history[i].type \in {RwTxResponse, RoTxResponse} + /\ history[i].tx \in Txs + /\ history[i].observed \in Seq(Txs) + /\ history[i].tx_id \in TxIDs + \/ /\ history[i].type = TxStatusReceived + /\ history[i].tx_id \in TxIDs + /\ history[i].status \in TxStatuses + +\* History is append-only +\* Like HistoryTypeOK, this property should always hold +HistoryMonoProp == + [][IsPrefix(history, history')]_history + +\* Indexes into history for events where a committed status is received +CommittedEventIndexes == + {i \in DOMAIN history: + /\ history[i].type = TxStatusReceived + /\ history[i].status = CommittedStatus + } + +\* Transaction IDs which received committed status messages +CommittedTxIDs == + {history[i].tx_id: i \in CommittedEventIndexes} + +InvalidEventIndexes == + {i \in DOMAIN history: + /\ history[i].type = TxStatusReceived + /\ history[i].status = InvalidStatus + } + +\* Transaction IDs which received invalid status messages +InvalidTxIDs == + {history[i].tx_id: i \in InvalidEventIndexes} + +\* Highest commit sequence number +CommitSeqNum == + Max({i[2]: i \in CommittedTxIDs} \cup {0}) + +RwTxResponseEventIndexes == + {x \in DOMAIN history : history[x].type = RwTxResponse} + +RoTxResponseEventIndexes == + {x \in DOMAIN history : history[x].type = RoTxResponse} + +TxResponseEventIndexes == + RwTxResponseEventIndexes \union RoTxResponseEventIndexes + + +\* Note these index are the events where the transaction was responded to +RwTxResponseCommittedEventIndexes == + {x \in DOMAIN history : + /\ history[x].type = RwTxResponse + /\ history[x].tx_id \in CommittedTxIDs} + +RwTxRequestCommittedEventIndexes == + {x \in DOMAIN history : + /\ history[x].type = RwTxRequest + /\ \E y \in RwTxResponseCommittedEventIndexes: + history[y].tx = history[x].tx} + +\* Note these index are the events where the transaction was responded to +RoTxResponseCommittedEventIndexes == + {x \in DOMAIN history : + /\ history[x].type = RoTxResponse + /\ history[x].tx_id \in CommittedTxIDs} + +RoTxRequestCommittedEventIndexes == + {x \in DOMAIN history : + /\ history[x].type = RoTxRequest + /\ \E y \in RoTxResponseCommittedEventIndexes: + history[y].tx = history[x].tx} + +TxStatusReceivedEventIndexes == + {x \in DOMAIN history : history[x].type = TxStatusReceived} + +RoTxRequestedCommittedEventIndexes == + {x \in DOMAIN history : + /\ history[x].type = RoTxRequest + /\ history[x].tx_id \in CommittedTxIDs} + +==== \ No newline at end of file diff --git a/tla/consistency/ExternalHistoryInvars.tla b/tla/consistency/ExternalHistoryInvars.tla new file mode 100644 index 000000000000..146fd2818043 --- /dev/null +++ b/tla/consistency/ExternalHistoryInvars.tla @@ -0,0 +1,225 @@ +---- MODULE ExternalHistoryInvars ---- + +EXTENDS ExternalHistory + +\* Read-write transaction responses always follow an associated request +AllRwReceivedIsFirstSentInv == + \A i \in DOMAIN history : + history[i].type = RwTxResponse + => \E j \in DOMAIN history : + /\ j < i + /\ history[j].type = RwTxRequest + /\ history[j].tx = history[i].tx + +\* Read-only transaction responses always follow an associated request +\* TODO: extend this to handle the fact that separate reads might get the same transaction ID +AllRoReceivedIsFirstSentInv == + \A i \in DOMAIN history : + history[i].type = RoTxResponse + => \E j \in DOMAIN history : + /\ j < i + /\ history[j].type = RoTxRequest + /\ history[j].tx = history[i].tx + +\* All responses must have an associated request earlier in the history (except tx status) +AllReceivedIsFirstSentInv == + /\ AllRwReceivedIsFirstSentInv + /\ AllRoReceivedIsFirstSentInv + +\* Transaction IDs uniquely identify read-write transactions +\* Note that it does not hold for read-only transactions +UniqueTxsInv == + \A i, j \in DOMAIN history: + /\ history[i].type = RwTxResponse + /\ history[j].type = RwTxResponse + /\ history[i].tx_id = history[j].tx_id + => history[i].tx = history[j].tx + +\* All transactions with the same ID observe the same transactions +SameObservationsInv == + \A i, j \in DOMAIN history: + /\ history[i].type \in {RwTxResponse, RoTxResponse} + /\ history[j].type \in {RwTxResponse, RoTxResponse} + /\ history[i].tx_id = history[j].tx_id + => history[i].observed = history[j].observed + +\* Transaction requested are unique +UniqueTxRequestsInv == + \A i, j \in DOMAIN history: + /\ history[i].type \in {RwTxRequest, RoTxRequest} + /\ history[j].type \in {RwTxRequest, RoTxRequest} + /\ i # j + => history[i].tx # history[j].tx + + +\* Each transaction has a unique transaction ID +UniqueTxIdsInv == + \A i, j \in {x \in DOMAIN history : history[x].type \in {RwTxResponse, RoTxResponse}} : + history[i].tx = history[j].tx + => history[i].tx_id = history[j].tx_id + +\* Sequence numbers uniquely identify read-write transactions +\* This invariant does not hold unless there is only a single CCF node +UniqueSeqNumsInv == + \A i, j \in {x \in DOMAIN history : history[x].type = RwTxResponse} : + history[i].tx_id[2] = history[j].tx_id[2] + => history[i].tx = history[j].tx + +\* Committed transactions have unique sequence numbers +\* This is a weaker version of UniqueSeqNumsInv +\* This always holds (except during DR) +UniqueSeqNumsCommittedInv == + \A i,j \in RwTxResponseCommittedEventIndexes: + \* Same sequences numbers implies same transaction + /\ history[i].tx_id[2] = history[j].tx_id[2] + => history[i].tx = history[j].tx + +\* A transaction status cannot be both committed and invalid +CommittedOrInvalidInv == + CommittedTxIDs \intersect InvalidTxIDs = {} + +\* If a transaction is committed then so are all others from the same term with smaller seqnums +\* These transactions cannot be invalid +OnceCommittedPrevCommittedInv == + \A i, j \in TxStatusReceivedEventIndexes: + /\ history[i].status = CommittedStatus + /\ history[i].tx_id[1] = history[j].tx_id[1] + /\ history[j].tx_id[2] <= history[i].tx_id[2] + => history[j].status = CommittedStatus + +\* If a transaction is invalid then so are all others from the same term with greater seqnums +OnceInvalidNextInvalidInv == + \A i, j \in TxStatusReceivedEventIndexes: + /\ history[i].status = InvalidStatus + /\ history[i].tx_id[1] = history[j].tx_id[1] + /\ history[j].tx_id[2] >= history[i].tx_id[2] + => history[j].status = InvalidStatus + +\* The following is strengthened variant of CommittedOrInvalidInv +CommittedOrInvalidStrongInv == + /\ OnceCommittedPrevCommittedInv + /\ OnceInvalidNextInvalidInv + + +\* Responses never observe transactions that have not been requested +OnlyObserveSentRequestsInv == + \A i \in {x \in DOMAIN history : history[x].type \in {RoTxResponse, RwTxResponse}} : + ToSet(history[i].observed) \subseteq + {history[j].tx : j \in {k \in DOMAIN history : + /\ k < i + /\ history[k].type = RwTxRequest}} + +\* All responses never observe the same request more than once +AtMostOnceObservedInv == + \A i \in DOMAIN history : + history[i].type \in {RoTxResponse, RwTxResponse} + => \A seqnum_x, seqnum_y \in DOMAIN history[i].observed: + seqnum_x # seqnum_y + => history[i].observed[seqnum_x] # history[i].observed[seqnum_y] + + +\* All committed read-write txs observe all previously committed txs (wrt to real-time) +\* Note that this requires committed txs to be observed from their response, +\* not just from when the client learns they were committed +AllCommittedObservedInv == + \A i \in RwTxResponseCommittedEventIndexes : + \A j \in RwTxRequestCommittedEventIndexes : + \A k \in RwTxResponseCommittedEventIndexes : + /\ history[k].tx = history[j].tx + /\ i < j + => Contains(history[k].observed, history[i].tx) + +\* All committed read-only txs observe all previously committed txs (wrt to real-time) +\* Note that this requires committed txs to be observed from their response, +\* not just from when the client learns they were committed +\* This does not hold for CCF services with multiple nodes +AllCommittedObservedRoInv == + \A i \in RwTxResponseCommittedEventIndexes : + \A j \in RoTxRequestCommittedEventIndexes : + \A k \in RoTxResponseCommittedEventIndexes : + /\ history[k].tx = history[j].tx + /\ i < j + => Contains(history[k].observed, history[i].tx) + +\* Invalid requests are not observed by any other requests +\* This is vacuously true for single node CCF services and does not hold for multi node services +InvalidNotObservedInv == + \A i, j, k \in DOMAIN history: + /\ history[i].type = RwTxResponse + /\ history[j].type = TxStatusReceived + /\ history[j].status = InvalidStatus + /\ history[k].type = RwTxResponse + /\ i # k + => history[i].tx \notin ToSet(history[k].observed) + + +\* A weaker variant of InvalidNotObservedInv which states that invalid requests are +\* not observed by committed requests +InvalidNotObservedByCommittedInv == + \A i, j, k, l \in DOMAIN history: + /\ history[i].type = RwTxResponse + /\ history[j].type = TxStatusReceived + /\ history[j].status = InvalidStatus + /\ history[k].type = RwTxResponse + /\ history[l].type = TxStatusReceived + /\ history[l].type = CommittedStatus + /\ history[k].tx_id = history[l] + /\ i # k + => history[i].tx \notin ToSet(history[k].observed) + +\* A history is serializable if there exists an execution sequence which is consistent +\* with client observations. This property completely ignores the order of events. +\* If any request observes A before B then every request must observe A before B +\* In this model, every request execution observes itself +\* This invariant ignores transaction IDs and whether transactions are committed +\* This invariant only holds for a single node CCF service +\* TODO: Fix this definition (and related) as I am not quite happy with them +RwSerializableInv == + \A i,j \in DOMAIN history: + /\ history[i].type = RwTxResponse + /\ history[j].type = RwTxResponse + => \/ IsPrefix(history[i].observed, history[j].observed) + \/ IsPrefix(history[j].observed, history[i].observed) + +\* A weaker version of RwSerializableInv which only considers committed requests +\* If any committed request observes A before B then every committed request must observe A before B +CommittedRwSerializableInv == + \A i,j,k,l \in DOMAIN history: + \* Event k is the committed status received for the transaction in event i + /\ history[i].type = RwTxResponse + /\ history[k].type = TxStatusReceived + /\ history[k].status = CommittedStatus + /\ history[i].tx_id = history[k].tx_id + \* Event l is the committed status received for the transaction in event j + /\ history[j].type = RwTxResponse + /\ history[l].type = TxStatusReceived + /\ history[l].status = CommittedStatus + /\ history[j].tx_id = history[l].tx_id + => \/ IsPrefix(history[i].observed, history[j].observed) + \/ IsPrefix(history[j].observed, history[i].observed) + +\* Linearizability for read-write transactions +\* Or equivalently, strict serializability as we are modeling a single object system +\* Refer to "Linearizability: A Correctness Condition for Concurrent Objects" +CommittedRwLinearizableInv == + /\ CommittedRwSerializableInv + /\ AllCommittedObservedInv + /\ AtMostOnceObservedInv + +\*Debugging invariants to check that specific states are reachable + +SomeCommittedTxDebugInv == + Cardinality(CommittedTxIDs) = 0 + +SomeInvalidTxDebugInv == + Cardinality(InvalidTxIDs) = 0 + +\* Two different transactions are committed +MultiCommittedTxDebugInv == + Cardinality(CommittedTxIDs) <= 1 + +\* Two different invalid transactions +MultiInvalidTxDebugInv == + Cardinality(InvalidTxIDs) <= 1 + +==== \ No newline at end of file diff --git a/tla/consistency/MCMultiNode.cfg b/tla/consistency/MCMultiNode.cfg new file mode 100644 index 000000000000..2f0f2852f8f7 --- /dev/null +++ b/tla/consistency/MCMultiNode.cfg @@ -0,0 +1,31 @@ +SPECIFICATION MCSpecMultiNode + +CONSTANTS + HistoryLimit = 6 + ViewLimit = 3 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + AllReceivedIsFirstSentInv + AllCommittedObservedInv + OnlyObserveSentRequestsInv + UniqueTxsInv + SameObservationsInv + UniqueTxIdsInv + UniqueTxRequestsInv + UniqueSeqNumsCommittedInv + CommittedOrInvalidStrongInv + CommittedRwSerializableInv + InvalidNotObservedByCommittedInv + AtMostOnceObservedInv + +CHECK_DEADLOCK + FALSE \ No newline at end of file diff --git a/tla/consistency/MCMultiNode.tla b/tla/consistency/MCMultiNode.tla new file mode 100644 index 000000000000..e9d26fcad1c4 --- /dev/null +++ b/tla/consistency/MCMultiNode.tla @@ -0,0 +1,27 @@ +---- MODULE MCMultiNode ---- +\* Bounded version of MultiNode + +EXTENDS MultiNode, MCSingleNode + +\* Upper bound on the number of possible view changes +CONSTANT ViewLimit + +MCTruncateLedgerAction == + \* check ViewLimit will not be exceed before truncating the ledger + /\ Len(ledgerBranches) < ViewLimit + /\ TruncateLedgerAction + +MCStatusInvalidResponseAction == + /\ Len(history) < HistoryLimit + /\ StatusInvalidResponseAction + +MCNextMultiNodeAction == + \/ MCNextSingleNodeAction + \/ MCTruncateLedgerAction + \/ MCStatusInvalidResponseAction + + +MCSpecMultiNode == Init /\ [][MCNextMultiNodeAction]_vars + + +==== \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeCommitReachability.cfg b/tla/consistency/MCMultiNodeCommitReachability.cfg new file mode 100644 index 000000000000..c6b58096506c --- /dev/null +++ b/tla/consistency/MCMultiNodeCommitReachability.cfg @@ -0,0 +1,22 @@ +SPECIFICATION MCSpecMultiNodeReads + + +CONSTANTS + HistoryLimit = 6 + ViewLimit = 1 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + MultiCommittedTxDebugInv + +CHECK_DEADLOCK + FALSE + \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeInvalidReachability.cfg b/tla/consistency/MCMultiNodeInvalidReachability.cfg new file mode 100644 index 000000000000..2c1f6ef12dbd --- /dev/null +++ b/tla/consistency/MCMultiNodeInvalidReachability.cfg @@ -0,0 +1,21 @@ +SPECIFICATION MCSpecMultiNodeReads + + +CONSTANTS + HistoryLimit = 7 + ViewLimit = 2 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + SomeInvalidTxDebugInv + +CHECK_DEADLOCK + FALSE \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReads.cfg b/tla/consistency/MCMultiNodeReads.cfg new file mode 100644 index 000000000000..d7550de52e54 --- /dev/null +++ b/tla/consistency/MCMultiNodeReads.cfg @@ -0,0 +1,31 @@ +SPECIFICATION MCSpecMultiNodeReads + +CONSTANTS + HistoryLimit = 6 + ViewLimit = 3 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + AllReceivedIsFirstSentInv + AllCommittedObservedInv + OnlyObserveSentRequestsInv + UniqueTxsInv + SameObservationsInv + UniqueTxIdsInv + UniqueTxRequestsInv + UniqueSeqNumsCommittedInv + CommittedOrInvalidStrongInv + CommittedRwSerializableInv + InvalidNotObservedByCommittedInv + AtMostOnceObservedInv + +CHECK_DEADLOCK + FALSE \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReads.tla b/tla/consistency/MCMultiNodeReads.tla new file mode 100644 index 000000000000..68f414d8fb0e --- /dev/null +++ b/tla/consistency/MCMultiNodeReads.tla @@ -0,0 +1,13 @@ +---- MODULE MCMultiNodeReads ---- +\* Bounded version of MultiNodeReads + +EXTENDS MCSingleNodeReads, MCMultiNode + +MCNextMultiNodeReadsAction == + \/ MCNextMultiNodeAction + \/ MCRoTxRequestAction + \/ MCRoTxResponseAction + +MCSpecMultiNodeReads == Init /\ [][MCNextMultiNodeReadsAction]_vars + +==== \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReadsAlt.cfg b/tla/consistency/MCMultiNodeReadsAlt.cfg new file mode 100644 index 000000000000..a56f36604922 --- /dev/null +++ b/tla/consistency/MCMultiNodeReadsAlt.cfg @@ -0,0 +1,31 @@ +SPECIFICATION MCSpecMultiNodeReadsAlt + +CONSTANTS + HistoryLimit = 11 + ViewLimit = 3 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + AllReceivedIsFirstSentInv + AllCommittedObservedInv + OnlyObserveSentRequestsInv + UniqueTxsInv + SameObservationsInv + UniqueTxIdsInv + UniqueTxRequestsInv + UniqueSeqNumsCommittedInv + CommittedOrInvalidStrongInv + CommittedRwSerializableInv + InvalidNotObservedByCommittedInv + AtMostOnceObservedInv + +CHECK_DEADLOCK + FALSE \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReadsAlt.tla b/tla/consistency/MCMultiNodeReadsAlt.tla new file mode 100644 index 000000000000..b9be2b6ed443 --- /dev/null +++ b/tla/consistency/MCMultiNodeReadsAlt.tla @@ -0,0 +1,24 @@ +---- MODULE MCMultiNodeReadsAlt ---- +\* MCMultiNodeReads with a different initial state + +EXTENDS MCMultiNodeReads + +\* Alternative initial state with two transactions already committed +InitAlt == + /\ ledgerBranches = << + <<[view |-> 1, tx |-> 0]>>, + <<[view |-> 1, tx |-> 0], [view |-> 2, tx |-> 1]>> + >> + /\ history = << + [type |-> RwTxRequest, tx |-> 0], + [type |-> RwTxRequest, tx |-> 1], + [type |-> RwTxResponse, tx_id |-> <<1, 1>>, tx |-> 0, observed |-> <<0>>], + [type |-> RwTxResponse, tx_id |-> <<2, 2>>, tx |-> 1, observed |-> <<0, 1>>], + [type |-> TxStatusReceived, status |-> CommittedStatus, tx_id |-> <<1, 1>>], + [type |-> TxStatusReceived, status |-> CommittedStatus, tx_id |-> <<2, 2>>] + >> + +MCSpecMultiNodeReadsAlt == InitAlt /\ [][MCNextMultiNodeReadsAction]_vars + + +==== \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReadsNotLinearizable.cfg b/tla/consistency/MCMultiNodeReadsNotLinearizable.cfg new file mode 100644 index 000000000000..372867a8281c --- /dev/null +++ b/tla/consistency/MCMultiNodeReadsNotLinearizable.cfg @@ -0,0 +1,22 @@ +SPECIFICATION MCSpecMultiNodeReads + + +CONSTANTS + HistoryLimit = 8 + ViewLimit = 2 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + AllCommittedObservedRoInv + +CHECK_DEADLOCK + FALSE + \ No newline at end of file diff --git a/tla/consistency/MCSingleNode.cfg b/tla/consistency/MCSingleNode.cfg new file mode 100644 index 000000000000..195a9bb207d1 --- /dev/null +++ b/tla/consistency/MCSingleNode.cfg @@ -0,0 +1,30 @@ +SPECIFICATION MCSpecSingleNode + +CONSTANTS + HistoryLimit = 7 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + AllReceivedIsFirstSentInv + AllCommittedObservedInv + OnlyObserveSentRequestsInv + UniqueTxsInv + UniqueTxIdsInv + UniqueSeqNumsInv + CommittedOrInvalidStrongInv + RwSerializableInv + CommittedRwSerializableInv + InvalidNotObservedInv + InvalidNotObservedByCommittedInv + AtMostOnceObservedInv + +CHECK_DEADLOCK + FALSE diff --git a/tla/consistency/MCSingleNode.tla b/tla/consistency/MCSingleNode.tla new file mode 100644 index 000000000000..49d09f40048d --- /dev/null +++ b/tla/consistency/MCSingleNode.tla @@ -0,0 +1,31 @@ +---- MODULE MCSingleNode ---- +\* Bounded version of SingleNode + +EXTENDS SingleNode + +CONSTANT HistoryLimit + +MCRwTxRequestAction == + /\ Len(history) < HistoryLimit + /\ RwTxRequestAction + +MCRwTxExecuteAction == + RwTxExecuteAction + +MCRwTxResponseAction == + /\ Len(history) < HistoryLimit + /\ RwTxResponseAction + +MCStatusCommittedResponseAction == + /\ Len(history) < HistoryLimit + /\ StatusCommittedResponseAction + +MCNextSingleNodeAction == + \/ MCRwTxRequestAction + \/ MCRwTxExecuteAction + \/ MCRwTxResponseAction + \/ MCStatusCommittedResponseAction + +MCSpecSingleNode == Init /\ [][MCNextSingleNodeAction]_vars + +==== \ No newline at end of file diff --git a/tla/consistency/MCSingleNodeCommitReachability.cfg b/tla/consistency/MCSingleNodeCommitReachability.cfg new file mode 100644 index 000000000000..28aaaf77289d --- /dev/null +++ b/tla/consistency/MCSingleNodeCommitReachability.cfg @@ -0,0 +1,20 @@ +SPECIFICATION MCSpecSingleNode + + +CONSTANTS + HistoryLimit = 3 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + SomeCommittedTxDebugInv + +CHECK_DEADLOCK + FALSE \ No newline at end of file diff --git a/tla/consistency/MCSingleNodeReads.cfg b/tla/consistency/MCSingleNodeReads.cfg new file mode 100644 index 000000000000..34fcd669c40a --- /dev/null +++ b/tla/consistency/MCSingleNodeReads.cfg @@ -0,0 +1,31 @@ +SPECIFICATION MCSpecSingleNodeReads + +CONSTANTS + HistoryLimit = 7 + + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + AllReceivedIsFirstSentInv + AllCommittedObservedInv + OnlyObserveSentRequestsInv + UniqueTxsInv + UniqueTxIdsInv + UniqueSeqNumsInv + CommittedOrInvalidStrongInv + RwSerializableInv + CommittedRwSerializableInv + InvalidNotObservedInv + InvalidNotObservedByCommittedInv + AtMostOnceObservedInv + AllCommittedObservedRoInv + +CHECK_DEADLOCK + FALSE \ No newline at end of file diff --git a/tla/consistency/MCSingleNodeReads.tla b/tla/consistency/MCSingleNodeReads.tla new file mode 100644 index 000000000000..f242da88f747 --- /dev/null +++ b/tla/consistency/MCSingleNodeReads.tla @@ -0,0 +1,21 @@ +---- MODULE MCSingleNodeReads ---- +\* Bounded version of SingleNodeReads + +EXTENDS SingleNodeReads, MCSingleNode + +MCRoTxRequestAction == + /\ Len(history) < HistoryLimit + /\ RoTxRequestAction + +MCRoTxResponseAction == + /\ Len(history) < HistoryLimit + /\ RoTxResponseAction + +MCNextSingleNodeReadsAction == + \/ MCNextSingleNodeAction + \/ MCRoTxRequestAction + \/ MCRoTxResponseAction + +MCSpecSingleNodeReads == Init /\ [][MCNextSingleNodeReadsAction]_vars + +==== \ No newline at end of file diff --git a/tla/consistency/MultiNode.tla b/tla/consistency/MultiNode.tla new file mode 100644 index 000000000000..08d95525839f --- /dev/null +++ b/tla/consistency/MultiNode.tla @@ -0,0 +1,49 @@ +---- MODULE MultiNode ---- +\* This specification extends SingleNode to model a multi-node CCF service + +EXTENDS SingleNode + +\* The set of views where the corresponding terms have all committed log entries +ViewWithAllCommitted == + {view \in DOMAIN ledgerBranches: + /\ Len(ledgerBranches[view]) >= CommitSeqNum + /\ \/ CommitSeqNum = 0 + \/ <> \in CommittedTxIDs } + +\* Simulates leader election by rolling back some number of uncommitted transactions and updating view +TruncateLedgerAction == + /\ \E view \in ViewWithAllCommitted: + /\ \E i \in (CommitSeqNum + 1)..Len(ledgerBranches[view]) : + /\ ledgerBranches' = Append(ledgerBranches, SubSeq(ledgerBranches[view], 1, i)) + /\ UNCHANGED history + +\* Sends status invalid message +StatusInvalidResponseAction == + /\ \E i \in DOMAIN history : + /\ history[i].type = RwTxResponse + \* either commit has passed seqnum but committed another transaction + /\ \/ /\ CommitSeqNum >= history[i].tx_id[2] + /\ Len(ledgerBranches[Len(ledgerBranches)]) >= history[i].tx_id[2] + /\ ledgerBranches[Len(ledgerBranches)][history[i].tx_id[2]].view # history[i].tx_id[1] + \* or commit hasn't reached seqnum but never will as current seqnum is higher + \/ /\ CommitSeqNum > 0 + /\ CommitSeqNum < history[i].tx_id[2] + /\ ledgerBranches[Len(ledgerBranches)][CommitSeqNum].view > history[i].tx_id[1] + \* Reply + /\ history' = Append( + history,[ + type |-> TxStatusReceived, + tx_id |-> history[i].tx_id, + status |-> InvalidStatus] + ) + /\ UNCHANGED ledgerBranches + +NextMultiNodeAction == + \/ NextSingleNodeAction + \/ TruncateLedgerAction + \/ StatusInvalidResponseAction + + +SpecMultiNode == Init /\ [][NextMultiNodeAction]_vars + +==== \ No newline at end of file diff --git a/tla/consistency/MultiNodeReads.cfg b/tla/consistency/MultiNodeReads.cfg new file mode 100644 index 000000000000..015b5e3d6a80 --- /dev/null +++ b/tla/consistency/MultiNodeReads.cfg @@ -0,0 +1,29 @@ +SPECIFICATION SpecMultiNodeReads + +CONSTANTS + RwTxRequest = RwTxRequest + RwTxResponse = RwTxResponse + RoTxRequest = RoTxRequest + RoTxResponse = RoTxResponse + TxStatusReceived = TxStatusReceived + + CommittedStatus = CommittedStatus + InvalidStatus = InvalidStatus + +INVARIANTS + TypeOK + AllReceivedIsFirstSentInv + AllCommittedObservedInv + OnlyObserveSentRequestsInv + UniqueTxsInv + SameObservationsInv + UniqueTxIdsInv + UniqueTxRequestsInv + UniqueSeqNumsCommittedInv + CommittedOrInvalidStrongInv + CommittedRwSerializableInv + InvalidNotObservedByCommittedInv + AtMostOnceObservedInv + +CHECK_DEADLOCK + FALSE \ No newline at end of file diff --git a/tla/consistency/MultiNodeReads.tla b/tla/consistency/MultiNodeReads.tla new file mode 100644 index 000000000000..75dafaeb779f --- /dev/null +++ b/tla/consistency/MultiNodeReads.tla @@ -0,0 +1,13 @@ +---- MODULE MultiNodeReads ---- +\* This specification extends MultiNode to add read-only transactions + +EXTENDS SingleNodeReads, MultiNode + +NextMultiNodeReadsAction == + \/ NextMultiNodeAction + \/ RoTxRequestAction + \/ RoTxResponseAction + +SpecMultiNodeReads == Init /\ [][NextMultiNodeReadsAction]_vars + +==== \ No newline at end of file diff --git a/tla/consistency/SingleNode.tla b/tla/consistency/SingleNode.tla new file mode 100644 index 000000000000..a9480321eed0 --- /dev/null +++ b/tla/consistency/SingleNode.tla @@ -0,0 +1,115 @@ +---- MODULE SingleNode ---- +\* A lightweight specification to define the externally visible behaviour of CCF +\* This specification has been inspired by https://github.com/tlaplus/azure-cosmos-tla +\* Where possible, naming should be consistent with https://microsoft.github.io/CCF/main/index.html +\* SingleNode considers a single node CCF service, so no view changes + +EXTENDS ExternalHistoryInvars, TLC + + +\* Abstract ledgers that contains only client transactions (no signatures) +\* Indexed by view, each ledger is the ledger associated with leader of that view +\* In practice, the ledger of every CCF node is one of these or a prefix for one of these +\* This could be switched to a tree which can represent forks more elegantly +VARIABLES ledgerBranches + +LedgerTypeOK == + \A view \in DOMAIN ledgerBranches: + \A seqnum \in DOMAIN ledgerBranches[view]: + \* Each ledger entry is tuple containing a view and tx + \* The ledger entry index is the sequence number + /\ ledgerBranches[view][seqnum].view \in Views + /\ ledgerBranches[view][seqnum].tx \in Txs + +\* In this abstract version of CCF's consensus layer, each ledger is append-only +LedgersMonoProp == + [][\A view \in DOMAIN ledgerBranches: IsPrefix(ledgerBranches[view], ledgerBranches[view]')]_ledgerBranches + +vars == << history, ledgerBranches >> + +TypeOK == + /\ HistoryTypeOK + /\ LedgerTypeOK + +Init == + /\ history = <<>> + /\ ledgerBranches = [ x \in {1} |-> <<>>] + +IndexOfLastRequested == + SelectLastInSeq(history, LAMBDA e : e.type \in {RwTxRequest, RoTxRequest}) + +NextRequestId == + IF IndexOfLastRequested = 0 THEN 0 ELSE history[IndexOfLastRequested].tx+1 + +\* Submit new read-write transaction +\* This could be extended to add a notion of session and then check for session consistency +RwTxRequestAction == + /\ history' = Append( + history, + [type |-> RwTxRequest, tx |-> NextRequestId] + ) + /\ UNCHANGED ledgerBranches + +\* Execute a read-write transaction +RwTxExecuteAction == + /\ \E i \in DOMAIN history : + /\ history[i].type = RwTxRequest + \* Check transaction has not already been added to a ledger + /\ \A view \in DOMAIN ledgerBranches: + {seqnum \in DOMAIN ledgerBranches[view]: + history[i].tx = ledgerBranches[view][seqnum].tx} = {} + \* Note that a transaction can be added to any ledger, simulating the fact + \* that it can be picked up by the current leader or any former leader + /\ \E view \in DOMAIN ledgerBranches: + ledgerBranches' = [ledgerBranches EXCEPT ![view] = + Append(@,[view |-> view, tx |-> history[i].tx])] + /\ UNCHANGED history + +\* Response to a read-write transaction +RwTxResponseAction == + /\ \E i \in DOMAIN history : + \* Check request has been received and executed but not yet responded to + /\ history[i].type = RwTxRequest + /\ {j \in DOMAIN history: + /\ j > i + /\ history[j].type = RwTxResponse + /\ history[j].tx = history[i].tx} = {} + /\ \E view \in DOMAIN ledgerBranches: + /\ \E seqnum \in DOMAIN ledgerBranches[view]: + /\ history[i].tx = ledgerBranches[view][seqnum].tx + /\ history' = Append( + history,[ + type |-> RwTxResponse, + tx |-> history[i].tx, + observed |-> [x \in 1..seqnum |-> ledgerBranches[view][x].tx], + tx_id |-> <>] ) + /\ UNCHANGED ledgerBranches + +\* Sending a committed status message +\* Note that a request could only be committed if it's in the highest view's ledger +StatusCommittedResponseAction == + /\ \E i \in DOMAIN history : + /\ history[i].type = RwTxResponse + /\ Len(ledgerBranches[Len(ledgerBranches)]) >= history[i].tx_id[2] + /\ ledgerBranches[Len(ledgerBranches)][history[i].tx_id[2]].view = history[i].tx_id[1] + \* Reply + /\ history' = Append( + history,[ + type |-> TxStatusReceived, + tx_id |-> history[i].tx_id, + status |-> CommittedStatus] + ) + /\ UNCHANGED ledgerBranches + +\* A CCF service with a single node will never have a view change +\* so the log will never be rolled back and thus transaction IDs cannot be invalid +NextSingleNodeAction == + \/ RwTxRequestAction + \/ RwTxExecuteAction + \/ RwTxResponseAction + \/ StatusCommittedResponseAction + + +SpecSingleNode == Init /\ [][NextSingleNodeAction]_vars + +==== \ No newline at end of file diff --git a/tla/consistency/SingleNodeReads.tla b/tla/consistency/SingleNodeReads.tla new file mode 100644 index 000000000000..9e92b90f2c6e --- /dev/null +++ b/tla/consistency/SingleNodeReads.tla @@ -0,0 +1,42 @@ +---- MODULE SingleNodeReads ---- +\* Expanding SingleNode to add read-only transactions + +EXTENDS SingleNode + +\* Submit new read-only transaction +RoTxRequestAction == + /\ history' = Append( + history, + [type |-> RoTxRequest, tx |-> NextRequestId] + ) + /\ UNCHANGED ledgerBranches + +\* Response to a read-only transaction request +\* Assumes read-only transactions are always forwarded +\* TODO: Separate execution and response +RoTxResponseAction == + /\ \E i \in DOMAIN history : + \* Check request has been received but not yet responded to + /\ history[i].type = RoTxRequest + /\ {j \in DOMAIN history: + /\ j > i + /\ history[j].type = RoTxResponse + /\ history[j].tx = history[i].tx} = {} + /\ \E view \in DOMAIN ledgerBranches: + /\ Len(ledgerBranches[view]) > 0 + /\ history' = Append( + history,[ + type |-> RoTxResponse, + tx |-> history[i].tx, + observed |-> [seqnum \in DOMAIN ledgerBranches[view] |-> ledgerBranches[view][seqnum].tx], + tx_id |-> <>] ) + /\ UNCHANGED ledgerBranches + +NextSingleNodeReadsAction == + \/ NextSingleNodeAction + \/ RoTxRequestAction + \/ RoTxResponseAction + +SpecSingleNodeReads == Init /\ [][NextSingleNodeReadsAction]_vars + +==== \ No newline at end of file diff --git a/tla/tlc_debug.sh b/tla/tlc_debug.sh new file mode 100755 index 000000000000..e58c6aa12126 --- /dev/null +++ b/tla/tlc_debug.sh @@ -0,0 +1,23 @@ +#!/bin/bash +# Copyright (c) Microsoft Corporation. All rights reserved. +# Licensed under the Apache 2.0 License. + +# When finding a counterexample is the expected outcome from TLC +# The debug invariant(s) should be the only invariant(s), otherwise +# this script might falsely return without errors + +./tlc.sh "$@" +status=$? + +# TLC safety violation returns error code 12 +# https://github.com/tlaplus/tlaplus/blob/a41cbafc66b1dd225156aaca38ad35ec330f4ae9/tlatools/org.lamport.tlatools/src/tlc2/output/EC.java#L350 + +if [ $status -eq 12 ]; then + echo "Counterexample found as expected." + exit 0 +elif [ $status -eq 0 ]; then + echo "Counterexample expected but not found." >&2 + exit 1 + else + exit $status +fi \ No newline at end of file