zookeeper trace verification by tla+

Signed-off-by: Niu Zhi <[email protected]>

README.md

@@ -0,0 +1,22 @@
+
+
+
+<p align="left">
+  <a href="https://lamport.azurewebsites.net/tla/">
+    <img src="https://lamport.azurewebsites.net/tla/splash_small.png"" alt="https://lamport.azurewebsites.net/tla/"><br/>
+  </a>
+</p>
+<p align="center">
+  <a href="https://zookeeper.apache.org/">
+    <img src="https://zookeeper.apache.org/images/zookeeper_small.gif"" alt="https://zookeeper.apache.org/"><br/>
+  </a>
+</p>
+
+<p align="left">                                                                                                          
+本仓库为使用Trace运行态模型实现对Zookeeper集群中数据一致性、状态一致性以及其选举阶段、数据同步阶段、广播阶段
+需要满足的属性进行形式化验证。<br/>
+1.TraceVerification为规约验证需要的自定义TLC算子，规约代码<br/>
+2.zookeeper-release-3.7.0为zookeeper插桩后的集群代码<br/>
+3.论文链接:https://dl.acm.org/doi/10.1145/3558819.3558822
+
+</p>

TraceVerification/BS.tla

@@ -0,0 +1,126 @@
+--------------------------------- MODULE BS ---------------------------------
+EXTENDS FiniteSets, Sequences, Naturals, Integers, TLC, Broadcast,Broadcast2,Reals  
+
+\* Sequence to Set
+RECURSIVE Seq2Set(_)
+Seq2Set(S) ==
+    IF S = <<>> THEN {}
+    ELSE
+        LET i == Head(S)
+        IN {i} \cup Seq2Set(Tail(S))
+
+
+
+VARIABLES broadCastSeq,offset,broadCastCollection
+vars == <<broadCastSeq,offset,broadCastCollection>>
+
+
+
+
+
+Init == /\ offset = 1
+        /\ broadCastSeq = <<>>
+        /\ broadCastCollection = {}
+
+Trace == broadcastparser("./broadcast.log")
+Trace2 == broadcastparser2("./broadcast.log")
+IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b  
+SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)                                       
+
+\*获取leader节点
+selectLeaderNode(S) == CHOOSE temp \in S : 
+                                        /\ temp.action = "LeaderLaunchProposal" 
+
+\*节点向数据库提交的事务
+selectNodeCommitTranslation(S) == { temp \in S:
+                                            /\ temp.action = "Request2DataTree"
+                                   }                                           
+
+\*获取Follower节点
+selectFollowerNode(S) == { temp \in S:
+                                      /\ temp.action = "FollowerSendAckToLeader"}  
+
+
+\*选择接受到的proposal
+selectReceivedProposal(S) ==  { temp \in S:
+                                      /\ temp.action = "ReceivedProposal"} 
+\*判断节点提交的事务是否与发起的写请求一致
+decideWriteRequestTranslationConsistency(writeRequestCollection,NodeCommitTranslationCollection,nodeCount,Request2DataTreeCount)==
+                                \A commitTranslation \in NodeCommitTranslationCollection:
+                                /\ commitTranslation.sessionid = writeRequestCollection.sessionid
+                                /\ commitTranslation.type = writeRequestCollection.type
+                                /\ commitTranslation.cxid = writeRequestCollection.cxid
+                                /\ commitTranslation.zxidHigh = writeRequestCollection.zxidHigh
+                                /\ commitTranslation.zxidLow = writeRequestCollection.zxidLow
+                                /\ commitTranslation.txntype = writeRequestCollection.txntype
+                                /\ nodeCount = Request2DataTreeCount
+\*判断proposal接受发送数据一致性
+decideProposalConsistency(SendProposal,ReceivedProposal) ==
+                              \A RP \in ReceivedProposal:
+                               /\ RP.sessionid = SendProposal.sessionid
+                               /\ RP.type = SendProposal.type
+                               /\ RP.cxid = SendProposal.cxid
+                               /\ RP.zxidHigh = SendProposal.zxidHigh
+                               /\ RP.zxidLow = SendProposal.zxidLow
+
+
+
+\*事务提交全局顺序验证
+SelectNodeByMyId(myId_,S) == CHOOSE x \in S : x.myId = myId_ 
+
+
+decideOrder(zxidHigh_1,zxidLow_1,zxidHigh_2,zxidLow_2) == 
+                                                       IF (zxidHigh_1 < zxidHigh_2) 
+                                                       THEN
+                                                        /\  TRUE
+                                                       ELSE
+                                                        /\  IF (zxidHigh_1 = zxidHigh_2) 
+                                                            THEN
+                                                             /\  IF (zxidLow_1 < zxidLow_2) 
+                                                                 THEN
+                                                                  /\  TRUE
+                                                                 ELSE
+                                                                  /\   FALSE
+                                                            ELSE
+                                                             /\   FALSE
+
+globaOrderVerification(S1,S2) ==
+                                /\\A temp \in S1:
+                                   \A temp_2 \in S2:
+                                     /\ IF ((temp.myId = temp_2.myId)) 
+                                        THEN
+                                         /\ decideOrder(temp.zxidHigh,temp.zxidLow,temp_2.zxidHigh,temp_2.zxidLow)
+
+                                        ELSE
+                                         /\ TRUE
+
+broadcast == /\ offset <= Len(Trace)
+             /\ offset' = offset + 1
+             /\ broadCastSeq' = Trace[offset]
+             /\ broadCastCollection' = Seq2Set(broadCastSeq')
+             /\ Assert(decideWriteRequestTranslationConsistency(selectLeaderNode(broadCastCollection'), selectNodeCommitTranslation(broadCastCollection'), Len(SetToSeq(selectFollowerNode(broadCastCollection'))) +1 ,  Len(SetToSeq(selectNodeCommitTranslation(broadCastCollection'))))=TRUE ,
+                       "WriteTranslationConsistency")
+             /\ Assert(decideProposalConsistency(selectLeaderNode(broadCastCollection'),selectReceivedProposal(broadCastCollection')) =TRUE , "Proposal consitency")   
+             /\ IF ((offset +1) <= Len(Trace2)) 
+                THEN
+                  /\ globaOrderVerification(Trace2[offset],Trace2[offset+1])
+                ELSE
+                  /\ TRUE
+
+
+
+
+term == /\ offset > Len(Trace)
+        /\ UNCHANGED vars
+
+Next == \/ broadcast
+        \/ term
+
+Spec == Init /\ [][Next]_vars  
+
+
+
+=============================================================================
+\* Modification History
+\* Last modified Thu Apr 07 20:41:27 CST 2022 by niuzhi
+\* Created Tue Mar 29 15:20:35 CST 2022 by niuzhi

TraceVerification/Broadcast.cfg

@@ -0,0 +1,4 @@
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* Generated on Wed Mar 09 21:40:05 CST 2022

TraceVerification/Broadcast.java

@@ -0,0 +1,62 @@
+import tlc2.value.impl.*;
+import util.UniqueString;
+
+import java.io.*;
+import java.util.*;
+import java.util.regex.Pattern;
+
+
+public class Broadcast {
+	// @TLAPlusOperator(identifier = "broadcastparser", module = "Broadcast")
+	public static Value broadcastparser(final StringValue absolutePath) throws IOException {
+		// read the log file at [absolutePath]
+		BufferedReader br = new BufferedReader(new FileReader(absolutePath.val.toString()));
+		// initialize array for all parsed records
+		List<TupleValue> result = new ArrayList<>();
+		boolean flag = false;
+		try {
+			List<RecordValue> rcdSeq = new ArrayList<>();
+			String line = br.readLine();
+			while (line != null && line.length() > 0) {
+				String[] lnarr = line.split(",");
+				if (Integer.parseInt(lnarr[1].split(":")[1]) == 0) {
+					flag = true;
+
+				}else if (Integer.parseInt(lnarr[1].split(":")[1]) == 9999) {
+					flag = false;
+				}else {
+					if (flag) {
+						// initialize arrays for field values [fields] and [values]
+						List<UniqueString> fields = new ArrayList<>();
+						List<Value> values = new ArrayList<>();
+						for (int i = 0; i < lnarr.length; i++) {
+							parsePair(lnarr[i].split(":"), fields, values);
+						}
+						rcdSeq.add(new RecordValue(fields.toArray(new UniqueString[0]), values.toArray(new Value[0]), true));
+					}
+				}
+				if (!flag) {
+					result.add(new TupleValue(rcdSeq.toArray(new Value[0])));
+					rcdSeq.clear();
+				}
+				line = br.readLine();
+			}
+		} finally {
+			br.close();
+		}
+		// return the aggregated sequence of records
+		//return new TupleValue(rcdSeq.toArray(new Value[0]));
+		return new TupleValue(result.toArray(new Value[0]));
+	}
+
+	private static void parsePair(String[] pair, List<UniqueString> fields, List<Value> values) {
+		fields.add(UniqueString.uniqueStringOf(pair[0]));
+		if (Pattern.compile("[0-9]*").matcher(pair[1]).matches()) {
+			values.add(IntValue.gen(Integer.parseInt(pair[1])));
+		}else {
+			values.add(new StringValue(pair[1]));
+		}
+
+	}
+
+}

TraceVerification/Broadcast.tla

@@ -0,0 +1,10 @@
+---- MODULE Broadcast ----
+
+EXTENDS Integers, Sequences, TLC
+
+\* parses the log to a TLA+ sequence of TLA+ records
+broadcastparser(path) == CHOOSE x \in Seq([state:Int,myId:Int,action:STRING,sessionid:STRING,type:STRING,cxid:STRING,zxid:STRING,txntype:STRING,reqpath:STRING]):TRUE
+========================================
+\* Modification History
+\* Last modified Thu Apr 07 20:41:27 CST 2022 by niuzhi
+\* Created Tue Mar 29 15:20:35 CST 2022 by niuzhi

TraceVerification/Broadcast2.java

@@ -0,0 +1,62 @@
+import tlc2.value.impl.*;
+import util.UniqueString;
+
+import java.io.*;
+import java.util.*;
+import java.util.regex.Pattern;
+
+
+public class Broadcast2 {
+	// @TLAPlusOperator(identifier = "broadcastparser2", module = "Broadcast2")
+	public static Value broadcastparser2(final StringValue absolutePath) throws IOException {
+		// read the log file at [absolutePath]
+		BufferedReader br = new BufferedReader(new FileReader(absolutePath.val.toString()));
+		// initialize array for all parsed records
+		List<Value> result = new ArrayList<>();
+		boolean flag = false;
+		try {
+			List<RecordValue> rcdSeq = new ArrayList<>();
+			String line = br.readLine();
+			while (line != null) {
+				String[] lnarr = line.split(",");
+				if (Integer.parseInt(lnarr[1].split(":")[1]) == 0) {
+					flag = true;
+
+				}else if (Integer.parseInt(lnarr[1].split(":")[1]) == 9999) {
+					flag = false;
+				}else {
+					if (flag) {
+						// initialize arrays for field values [fields] and [values]
+						List<UniqueString> fields = new ArrayList<>();
+						List<Value> values = new ArrayList<>();
+						for (int i = 0; i < lnarr.length; i++) {
+							parsePair(lnarr[i].split(":"), fields, values);
+						}
+						rcdSeq.add(new RecordValue(fields.toArray(new UniqueString[0]), values.toArray(new Value[0]), true));
+					}
+				}
+				if (!flag) {
+					result.add(new SetEnumValue(rcdSeq.toArray(new Value[0]),true));
+					rcdSeq.clear();
+				}
+				line = br.readLine();
+			}
+		} finally {
+			br.close();
+		}
+		// return the aggregated sequence of records
+		//return new TupleValue(rcdSeq.toArray(new Value[0]));
+		return new TupleValue(result.toArray(new Value[0]));
+	}
+
+	private static void parsePair(String[] pair, List<UniqueString> fields, List<Value> values) {
+		fields.add(UniqueString.uniqueStringOf(pair[0]));
+		if (Pattern.compile("[0-9]*").matcher(pair[1]).matches()) {
+			values.add(IntValue.gen(Integer.parseInt(pair[1])));
+		}else {
+			values.add(new StringValue(pair[1]));
+		}
+
+	}
+
+}

TraceVerification/Broadcast2.tla

@@ -0,0 +1,10 @@
+---- MODULE Broadcast2 ----
+
+EXTENDS Integers, Sequences, TLC
+
+\* parses the log to a TLA+ sequence of TLA+ records
+broadcastparser2(path) == CHOOSE x \in Seq([state:Int,myId:Int,action:STRING,sessionid:STRING,type:STRING,cxid:STRING,zxidHigh:Int,zxidLow:Int,txntype:STRING,reqpath:STRING]):TRUE
+========================================
+\* Modification History
+\* Last modified Thu Apr 07 20:41:27 CST 2022 by niuzhi
+\* Created Tue Mar 29 15:20:35 CST 2022 by niuzhi

TraceVerification/ExternalSeqRecordParser2.java

@@ -0,0 +1,52 @@
+import tlc2.value.impl.*;
+import util.UniqueString;
+
+import java.io.*;
+import java.util.*;
+
+
+public class ExternalSeqRecordParser2 {
+	// @TLAPlusOperator(identifier = "ExSeqRcdParser2", module = "ExternalSeqRecordParser2")
+	public static Value ExSeqRcdParser2(final StringValue absolutePath) throws IOException {
+		// read the log file at [absolutePath]
+		BufferedReader br = new BufferedReader(new FileReader(absolutePath.val.toString()));
+		// initialize array for all parsed records
+		List<RecordValue> rcdSeq = new ArrayList<>();
+		try {
+			String line = br.readLine();
+			while (line != null) {
+				// initialize arrays for field values [fields] and [values]
+				List<UniqueString> fields = new ArrayList<>();
+				List<Value> values = new ArrayList<>();
+				// split string on seperator into array of filed and value
+				String[] lnarr = line.split(",");
+				// parse each entry of [lnarr] as a field-value pair
+				for (int i = 0; i < lnarr.length; i++) {
+					parsePair(lnarr[i].split(":"), fields, values);
+				}
+
+				//leader:3,follower:2,followerSendEpochToLeader:1,leaderReceivedEpochFromFollower:1,leaderCalculaterNewEpoch:2,followerReceivedNewEpochFromLeader:2,leaderSyncDataZxid:10000006,followerSyncDataZxid:10000006
+
+				// add record to the sequence
+				rcdSeq.add(new RecordValue(fields.toArray(new UniqueString[0]), values.toArray(new Value[0]), true));
+				line = br.readLine();
+			}
+		} finally {
+			br.close();
+		}
+		// return the aggregated sequence of records
+		return new TupleValue(rcdSeq.toArray(new Value[0]));
+	}
+
+	private static void parsePair(String[] pair, List<UniqueString> fields, List<Value> values) {
+		fields.add(UniqueString.uniqueStringOf(pair[0]));
+
+		if (pair[1].contains("0x")) {
+			values.add(new StringValue(pair[1]));
+		}else {
+			values.add(IntValue.gen(Integer.parseInt(pair[1])));
+		}
+
+	}	
+
+}

TraceVerification/ExternalSeqRecordParser2.tla

@@ -0,0 +1,11 @@
+---- MODULE ExternalSeqRecordParser2 ----
+
+EXTENDS Integers, Sequences, TLC
+
+\* parses the log to a TLA+ sequence of TLA+ records
+ExSeqRcdParser2(path) == CHOOSE x \in Seq([leader:Int,follower:Int,followerSendEpochToLeader:Int,leaderReceivedEpochFromFollower:Int,leaderCalculaterNewEpoch:Int,followerReceivedNewEpochFromLeader:Int,leaderSyncDataZxid:STRING,followerSyncDataZxid:STRING]):TRUE
+
+========================================
+\* Modification History
+\* Last modified Thu Apr 07 20:41:27 CST 2022 by niuzhi
+\* Created Tue Mar 29 15:20:35 CST 2022 by niuzhi