commit 8484b521803938e06f38ce64e14b125bdfd9f60a
from: Sergey Bronnikov <estetus@gmail.com>
via: Sergey Bronnikov <sergeyb@tarantool.org>
date: Tue Jan 09 11:16:19 2024 UTC

spin: initial version of 2pc model

commit - /dev/null
commit + 8484b521803938e06f38ce64e14b125bdfd9f60a
blob - /dev/null
blob + 707b3bc4892bd92e01a4755fb1425f3527f523fb (mode 644)
--- /dev/null
+++ spin/2pc.pml
@@ -0,0 +1,69 @@
+/*
+ * Two-phase commit (2PC) is a very simple and elegant protocol
+ * that ensures the atomic commitment of distributed transactions.
+ */
+
+/* A number of processes. */
+#ifndef NPROC
+#define NPROC 3
+#endif /* NPROC */
+
+mtype = {
+	ABORT,
+	COMMIT,
+	START,
+	UNDEFINED
+};
+
+/* A channel with messages produced by resource manager. */
+chan Mchan = [0] of {mtype};
+
+/* A channel with messages produced by processes. */
+chan Pchan = [0] of {mtype};
+
+/* By default global decision is undefined. */
+mtype CommonDecision = UNDEFINED;
+
+proctype manager() {
+	byte count = 0;
+	do
+	:: (count < NPROC) -> Mchan ! START; count++;
+	:: (count == NPROC) -> break;
+	od;
+
+	CommonDecision = COMMIT;
+	mtype vote;
+	do
+	:: (count < 2 * NPROC) -> Pchan ? vote; count++;
+	   if
+	   :: (vote == ABORT) -> CommonDecision = ABORT;
+	   :: (vote == COMMIT) -> skip;
+	   fi
+	:: (count == 2 * NPROC) -> break;
+	od;
+
+	do
+	:: (count < 3 * NPROC) -> Mchan ! CommonDecision; count++;
+	:: (count == 3 * NPROC) -> break;
+	od;
+}
+
+proctype proc(byte proc_id) {
+	mtype proc_decision = UNDEFINED;
+	Mchan ? START ->
+	if
+	:: Pchan ! ABORT; Mchan ? proc_decision; proc_decision = ABORT;
+	:: Pchan ! COMMIT; Mchan ? proc_decision
+	fi;
+	assert(proc_decision == CommonDecision)
+}
+
+init {
+	byte started_procs = 0;
+	do
+	:: (started_procs < NPROC) -> run proc(started_procs); started_procs++;
+	:: (started_procs == NPROC) -> break;
+	od;
+
+	run manager();
+}