tarantool · Serpentian · Mar 26, 2025 · Apr 1, 2025 · Mar 31, 2025 · Apr 4, 2025
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -852,6 +852,7 @@ set(TARANTOOL_BIN $<TARGET_FILE:tarantool>)
 
 add_subdirectory(extra)
 add_subdirectory(test)
+add_subdirectory(proofs/tla)
 if (CMAKE_BUILD_TYPE STREQUAL "Debug")
     message(AUTHOR_WARNING "Benchmarks are available only in release build")
 else ()

diff --git a/proofs/tla/CMakeLists.txt b/proofs/tla/CMakeLists.txt
@@ -0,0 +1,47 @@
+find_program(TLC tlc)
+if (NOT EXISTS ${TLC})
+  message(WARNING "TLC is required for running TLA+ tests")
+  return()
+endif()
+
+set(TEST_SUITE_NAME "tla")
+
+message(STATUS "Add test suite ${TEST_SUITE_NAME}")
+
+list(APPEND TLA_LIBRARIES
+  ${PROJECT_SOURCE_DIR}/proofs/tla/src/modules
+  ${PROJECT_SOURCE_DIR}/proofs/tla/src/
+)
+list(JOIN TLA_LIBRARIES ":" TLA_LIBRARIES_STR)
+
+file(GLOB_RECURSE tests
+  ${CMAKE_CURRENT_SOURCE_DIR}/test/*.tla
+)
+
+# Remove files that match *_TTrace_*.tla. These are remainings of the runs.
+foreach(test ${tests})
+  if(test MATCHES ".*_TTrace_.*\\.tla$")
+    list(REMOVE_ITEM tests ${test})
+  endif()
+endforeach()
+
+foreach(test_path ${tests})
+  get_filename_component(test_name ${test_path} NAME)
+  # FIXME: By default, GLOB lists directories.
+  # Directories are omitted in the result if LIST_DIRECTORIES
+  # is set to false. New in version CMake 3.3.
+  if(${test_name} STREQUAL ${TEST_SUITE_NAME})
+    continue()
+  endif()
+  set(test_title "test/${TEST_SUITE_NAME}/${test_name}")
+  get_filename_component(test_dir "${test_path}" DIRECTORY)
+  get_filename_component(test_name "${test_path}" NAME_WLE)
+  add_test(NAME ${test_title}
+           COMMAND ${TLC} -workers auto ${test_name}
+           WORKING_DIRECTORY ${test_dir}
+  )
+  set_tests_properties(${test_title} PROPERTIES
+    ENVIRONMENT "JAVA_OPTS=-DTLA-Library=${TLA_LIBRARIES_STR}"
+    LABELS "${TEST_SUITE_NAME};regression;"
+  )
+endforeach()
diff --git a/proofs/tla/src/definitions.tla b/proofs/tla/src/definitions.tla
@@ -0,0 +1,74 @@
+/*
+ * Copyright 2010-2025, Tarantool AUTHORS, please see AUTHORS file.
+ *
+ * Redistribution and use in source and binary forms, with or
+ * without modification, are permitted provided that the following
+ * conditions are met:
+ *
+ * 1. Redistributions of source code must retain the above
+ *    copyright notice, this list of conditions and the
+ *    following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above
+ *    copyright notice, this list of conditions and the following
+ *    disclaimer in the documentation and/or other materials
+ *    provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY <COPYRIGHT HOLDER> ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL
+ * <COPYRIGHT HOLDER> OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT,
+ * INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
+ * BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF
+ * THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ */
+
+------------------------------ MODULE definitions ------------------------------
+
+\* See raft's state variable.
+Follower == "FOLLOWER"
+Candidate == "CANDIDATE"
+Leader == "LEADER"
+
+\* XrowEntry types.
+DmlType == "INSERT"
+PromoteType == "PROMOTE"
+ConfirmType == "CONFIRM"
+RollbackType == "ROLLBACK"
+RaftType == "RAFT"
+OkType == "OK"
+NopType == "NOP"
+
+\* Group IDs of the XrowEntry.
+DefaultGroup == "DEFAULT"
+LocalGroup == "LOCAL"
+
+\* Flags of the XrowEntry:
+\* - wait_sync - true for any transaction, that would enter the limbo.
+\* - wait_ack - true for a synchronous transaction.
+DefaultFlags == [wait_sync |-> FALSE, wait_ack |-> FALSE, force_async |-> FALSE]
+SyncFlags == [wait_sync |-> TRUE, wait_ack |-> TRUE, force_async |-> FALSE]
+ForceAsyncFlags == [wait_sync |-> FALSE, wait_ack |-> FALSE, force_async |-> TRUE]
+
+\* Type of cbus messages to Tx thread.
+TxWalType == "WAL"
+TxRelayType == "RELAY"
+TxApplierType == "APPLIER"
+
+\* See msgs variable for description.
+RelaySource == 1
+ApplierSource == 2
+
+\* Error codes.
+SplitBrainError == "SPLIT_BRAIN"
+
+\* Reserved value
+Nil == "NIL"
+
+===============================================================================
diff --git a/proofs/tla/src/modules/applier.tla b/proofs/tla/src/modules/applier.tla
@@ -0,0 +1,196 @@
+/*
+ * Copyright 2010-2025, Tarantool AUTHORS, please see AUTHORS file.
+ *
+ * Redistribution and use in source and binary forms, with or
+ * without modification, are permitted provided that the following
+ * conditions are met:
+ *
+ * 1. Redistributions of source code must retain the above
+ *    copyright notice, this list of conditions and the
+ *    following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above
+ *    copyright notice, this list of conditions and the following
+ *    disclaimer in the documentation and/or other materials
+ *    provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY <COPYRIGHT HOLDER> ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL
+ * <COPYRIGHT HOLDER> OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT,
+ * INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
+ * BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF
+ * THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ */
+
+-------------------------------- MODULE applier --------------------------------
+
+EXTENDS Integers, Sequences, FiniteSets
+
+--------------------------------------------------------------------------------
+\* Declaration
+--------------------------------------------------------------------------------
+
+CONSTANTS
+    Servers,        \* A nonempty set of server identifiers.
+    SplitBrainCheck \* Whether SplitBrain errors should be raised.
+
+ASSUME Cardinality(Servers) > 0
+ASSUME SplitBrainCheck \in {TRUE, FALSE}
+
+VARIABLES
+    msgs,
+    \* Applier implementation.
+    applierAckMsg, \* Whether applier needs to send acks.
+    applierVclock, \* Implementation of the replicaset.applier.vclock
+    \* Tx implementation (see box module).
+    txApplierQueue
+
+applierVars == <<applierAckMsg, applierVclock>>
+
+\* Txn substitution.
+CONSTANTS MaxClientRequests
+VARIABLES tId, clientCtr, walQueue
+LOCAL txnVarsSub == <<tId, clientCtr, walQueue>>
+
+\* Raft substitution.
+CONSTANTS ElectionQuorum, MaxRaftTerm
+VARIABLES state, term, volatileTerm, vote, volatileVote, leader, votesReceived,
+          isBroadcastScheduled, candidateVclock, vclock,
+          relayRaftMsg
+LOCAL raftVarsSub == <<state, term, volatileTerm, vote, volatileVote, leader,
+                       votesReceived, isBroadcastScheduled,
+                       candidateVclock, vclock, relayRaftMsg>>
+
+\* Limbo substitution.
+VARIABLES limbo, limboVclock, limboOwner, limboPromoteGreatestTerm,
+          limboPromoteTermMap, limboConfirmedLsn, limboVolatileConfirmedLsn,
+          limboConfirmedVclock, limboAckCount, limboSynchroMsg,
+          limboPromoteLatch, error, relayLastAck
+LOCAL limboVarsSub == <<limbo, limboVclock, limboOwner,
+                        limboPromoteGreatestTerm, limboPromoteTermMap,
+                        limboConfirmedLsn, limboVolatileConfirmedLsn,
+                        limboConfirmedVclock, limboAckCount, limboSynchroMsg,
+                        limboPromoteLatch, error, relayLastAck>>
+
+--------------------------------------------------------------------------------
+\* Imports
+--------------------------------------------------------------------------------
+
+LOCAL INSTANCE txn
+LOCAL INSTANCE raft
+LOCAL INSTANCE limbo
+LOCAL INSTANCE utils
+
+--------------------------------------------------------------------------------
+\* Implementation
+--------------------------------------------------------------------------------
+
+ApplierInit ==
+    /\ applierAckMsg = [i \in Servers |-> [j \in Servers |-> EmptyGeneralMsg]]
+    /\ applierVclock = [i \in Servers |-> [j \in Servers |-> 0]]
+
+\* Implementation of the applier_thread_writer_f
+ApplierWrite(i, j) ==
+    /\ applierAckMsg[i][j].is_ready = TRUE
+    /\ Send(msgs, i, j, ApplierSource, applierAckMsg[i][j].body)
+    /\ LET newMsg == [applierAckMsg[i][j] EXCEPT !.is_ready = FALSE]
+       IN applierAckMsg' = [applierAckMsg EXCEPT ![i][j] = newMsg]
+    /\ UNCHANGED
+        \* Without {msgs, applierAckMsg}
+        <<applierVclock, txApplierQueue>>
+
+ApplierRead(i, j) ==
+    /\ Len(msgs[j][i][RelaySource]) > 0
+    /\ LET entry == Head(msgs[j][i][RelaySource])
+           newQueue == Append(txApplierQueue[i], TxMsg(TxApplierType, entry))
+       IN /\ txApplierQueue' = [txApplierQueue EXCEPT ![i] = newQueue]
+          /\ msgs' = [msgs EXCEPT ![j][i][RelaySource] =
+                          Tail(msgs[j][i][RelaySource])]
+          /\ UNCHANGED
+                \* Without {msgs, txApplierQueue}
+                <<applierAckMsg, applierVclock>>
+
+ApplierProcess(i, j) ==
+    /\ \/ ApplierWrite(i, j)
+       \/ ApplierRead(i, j)
+    /\ UNCHANGED <<msgs, txnVarsSub, raftVarsSub, limboVarsSub, txApplierQueue>>
+
+ApplierSynchroIsSplitBrain(i, entry) ==
+    /\ SplitBrainCheck = TRUE
+    /\ limboPromoteTermMap[entry.replica_id] # limboPromoteGreatestTerm[i]
+    /\ entry.type = DmlType
+
+\* Part of applier_synchro_filter_tx, raise Split Brain error.
+ApplierSynchroRaiseSplitBrainIfNeeded(i, entry) ==
+    IF ApplierSynchroIsSplitBrain(i, entry)
+    THEN error' = [error EXCEPT ![i] = SplitBrainError]
+    ELSE UNCHANGED <<error>>
+
+\* Part of applier_synchro_filter_tx, NOPify entries.
+ApplierSynchroNopifyTx(i, entry) ==
+    LET skipNopify == /\ limboPromoteTermMap[entry.replica_id] =
+                            limboPromoteGreatestTerm[i]
+                      /\ \/ entry.type = PromoteType
+                         \/ /\ entry.type = ConfirmType
+                            /\ entry.body.lsn >
+                                limboConfirmedVclock[i][entry.replica_id]
+    IN IF skipNopify THEN entry
+       ELSE [entry EXCEPT !.type = NopType, !.body = <<>>]
+
+ApplierNotInSynchroWrite(i) ==
+    ~LimboIsInRollback(i, limboSynchroMsg, limboPromoteLatch)
+
+ApplierApplyTx(i, entry) ==
+    /\ ApplierSynchroRaiseSplitBrainIfNeeded(i, entry)
+    /\ IF /\ ~ApplierSynchroIsSplitBrain(i, entry)
+          /\ entry.lsn > applierVclock[i][entry.replica_id]
+       THEN LET newEntry == ApplierSynchroNopifyTx(i, entry)
+            IN /\ applierVclock = [applierVclock EXCEPT
+                                   ![i][entry.replica_id] = newEntry.lsn]
+               /\ IF \/ newEntry.type = DmlType
+                     \/ newEntry.type = NopType
+                  THEN /\ TxnDo(i, newEntry)
+                  ELSE /\ LimboScheduleWrite(i, newEntry)
+                       /\ UNCHANGED <<>>
+       ELSE UNCHANGED <<applierVclock>>
+    /\ UNCHANGED
+        \* Without {error, applierVclock, TxnDo: {wal, walQueue, limbo, tId},
+        \*          LimboScheduleWrite: {limboSynchroMsg, {tId, walQueue, error,
+        \*          limbo, limboSynchroMsg, limboVolatileConfirmedLsn,
+        \*          limboPromoteLatch}}}
+        <
8A04
<msgs, raftVars,
+          vclock, txApplierQueue, limboVclock, limboOwner,
+          limboPromoteGreatestTerm, limboPromoteTermMap, limboConfirmedLsn,
+          limboConfirmedVclock, limboAckCount, limboSynchroMsg>>
+
+\* Implementation of the applier_process_batch.
+TxOnApplierReceive(i, entry) ==
+    \/ /\ entry.lsn # -1 \* DmlType, PromoteType, ConfirmType
+       /\ ApplierApplyTx(i, entry)
+    \/ /\ entry.type = RaftType
+       /\ RaftProcessMsg(i, entry)
+
+ApplierSignalAck(i, j, ackVclock) ==
+    LET entry == XrowEntry(OkType, i, DefaultGroup, DefaultFlags, [
+        vclock |-> ackVclock,
+        term |-> term[i]
+    ])
+    IN applierAckMsg = [applierAckMsg EXCEPT ![i][j] = GeneralMsg(entry)]
+
+\* Implementation of the applier_on_wal_write. Sends acks.
+ApplierSignalAckIfNeeded(i, entry, ackVclock) ==
+    /\ IF entry.replica_id # i
+       THEN ApplierSignalAck(i, entry.replica_id, ackVclock)
+       ELSE UNCHANGED <<applierAckMsg>>
+    /\ UNCHANGED <<relayLastAck, relayRaftMsg, applierVclock>>
+
+ApplierNext(servers) == \E i, j \in servers: ApplierProcess(i, j)
+
+================================================================================